FreePlane.thy

theory FreePlane
  imports Chapter2 (* Jordan_Normal_Form.Matrix *)
(* Need to somehow import AFP first; see https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-February/msg00129.html*)

begin
text \<open>\begin{hartshorne}
Example (A non-Desarguesian projective plane). Let $\pi_0$ be four points and no lines. 
Let $\Pi$ be the free projective plane generated by $\pi_0.$ Note, as a Corollary of the previous
proposition, that $\Pi$ is infinite, and so every line contains infinitely many points. Thus 
it is possible to choose $O,A,B,C,$ no three collinear, $A'$ on $OA,$ $B'$ on $OB,$ $C'$ on $OC,$ such 
that they form 7 distinct points and $A', B', C'$ are not collinear. Then construct
\begin{align*}
P &= AB \cdot A'B'\\
Q &= AC \cdot A'C'\\ 
R &= BC \cdot B'C'.
\end{align*}

Check that all $10$ points are distinct. If Desargues’ Theorem is true in $\Pi,$ then $P,Q,R$ 
lie on a 
line, hence these $10$ points and $10$ lines form a confined configuration, which 
must lie in $\pi_0,$ and that's a contradiction, 
 since $\pi_0$ has only four points.
\end{hartshorne}\<close>

text \<open>\spike
Modeling the free projective plane on a set of points is quite a pain in the neck. Hatshorne can 
be glib, for instance, saying that if $l$ and $m$ don't intersect at level $n$, then we add a 
new point called $l \cdot m$ at level $n+1$, but we need some actual representation of $l \cdot m$, 
and when we try to construct once, we recognize that it must be ``the same'' as $m \cdot l$. So 
we place an order on lines, and only construct the intersection of $l$ and $m$ when $l < m$; we
do the same for the line joining points $P $ and $Q$, which must be the same as the line joining
$Q$ and $P$. 

The natural solution, in both cases, would be to use a constructor ``Join {P,Q}'', but it turns 
out that I could not make ``Join fpoint set'' be a legal constructor description, and parenthesizing 
was of no use either. Another possibility would be to define all possible (unordered) joins/meets,
and then build an equivalence relation and take quotients, but that seemed grim as well. 

I've ignored lines that occur in the initial
configuration, as free projective planes appear only once more in the book, and it didn't seem 
worth making this definition even more complex just to handle that one additional mention.

I've really constructed only the free projective plane on four points (defined in the 
type "basepoint"), but this can clearly be extended to more points as needed. 

There's one more divergence from the text: I'm really defining \emph{two} mutually recursive sets: 
$\Pi_n$, the set of points in the $n$th version of the projective plane, and $\Lambda_n$, the set of 
lines. My $\Pi_n$ is Hartshorne's $\pi_{2n}$; my $\Pi_n$, together with $\Lambda_n$ as the set of lines,
is Hartshorne's $\pi{2n+1}$. This has the advantage that each of these sequences of things has a 
single natural-number index, rather than one being indexed by evens and one being indexed by odds; 
this sets them up for a (mutual) induction of some sort. 
\done\<close>
locale free_projective_plane_data =
    fixes meets :: "'point \<Rightarrow> 'line \<Rightarrow> bool"
begin
datatype basepoint = AA | BB | CC | DD

(* I need an order on basepoints to start an inductive definition of order on pairs of points,
and pairs of lines, etc. *)

fun lt:: "basepoint \<Rightarrow> basepoint \<Rightarrow> bool" where
    "lt AA BB = True"
  | "lt AA CC = True"
  | "lt AA DD = True"
  | "lt BB CC = True"
  | "lt BB DD = True"
  | "lt CC DD = True"
  | "lt U V = False"


lemma "antisymp lt" 
  by (smt antisympI free_projective_plane_data.lt.elims(2) free_projective_plane_data.lt.simps(15) free_projective_plane_data.lt.simps(7))

lemma "transp lt"
  by (smt free_projective_plane_data.basepoint.exhaust lt.simps(2,3,5,10,12,13) transpI)

datatype fpoint = Basepoint nat basepoint | Intersect nat fline fline and
fline =  Join nat fpoint fpoint | Extend nat fline (* | Baseline nat baseline;  removed to simplify *)

text \<open>\spike
To clarify the typedefs above: the "nat" in each item is its "level" (in Hartshorne's terminology),
although I guess it's Hartshorne's level divided by two. And while this "level" can be any
natural number, we're actually going to build a final set of points, point_set, that contains
only certain special fpoints. For instance, Basepoints will only be included if their level is 0
(and all such Basepoints will be included). Intersect i k l will only be included if one of 
k and l has level i-1, and if k and l don't intersect at level i-1,m and if k is "before" l in some
ordering that I'll define. 

What about lines? Well, Join i P Q will only be included if at least one of P and Q has level i-1, 
and P is before Q in a soon-to-be-defined ordering, AND if there's no line at level i-1 containing
both P and Q. The only slightly tricky one is "Extend i k". For that, k must already be an 
fline at level i-1, but the semantics of Extend i k is that it contains all points of k (i.e., points 
P such that "nmeets (i-1) P k") AND contains any level-i point P of the form Intersect i k m or 
Intersect i m k. 
\done\<close>

(* "less than" rules for points and lines. *)
fun plt:: "fpoint  \<Rightarrow> fpoint \<Rightarrow> bool" 
     and llt:: "fline \<Rightarrow> fline \<Rightarrow> bool" 
where
    "plt (Basepoint n P) (Basepoint k Q) = (lt P Q)"
  | "plt (Basepoint n P) (Intersect i l m) = True"
  | "plt (Intersect i l m) (Basepoint n P)  = False"
  | "plt (Intersect i l m) (Intersect j n p)  
        = ((i < j) \<or> 
           ((i = j) \<and> (llt l n)) \<or>
           ((i = j) \<and> (l = n) \<and> (llt m p)))" 
  | "llt (Join i P Q)(Join j R S) = ((i < j) \<or> 
                                     ((i = j) \<and> (plt P  R)) \<or>
                                     ((i = j) \<and> (P = R) \<and> (plt Q  S)))"
  | "llt (Join i P Q) (Extend j m) = (i \<le> j)"
  | "llt (Extend j m) (Join i P Q)  = (j < i)"
  | "llt (Extend i l) (Extend j m) = ((i < j) \<or>
                                       (i = j) \<and> (llt l m))" 

(* Basepoints: the only "stage" (the 'nat' data) allowed is 0. For all flines, the 'nat' data is
  1 or more (now that I've gotten rid of Baselines)  *)
(* Use "s" for "stage" (i.e., the index in the construction process). I'll use i and j similarly *)

(* define a rule for when, at stage s, a particular point and line "meet". So (nmeets s) takes
points and lines at stage s and tells whether or not they meet.

Note that points whose stage is greater than s cannot meet a line at stage s. 
On the other hand, a new point at stage s may be joined to a basepoint (stage 0 !) by a 
new line at stage s, so lines at stage s may meet any point whose stage is s or less.  

Finally, we have to define "stage s meeting" for *all* imaginable points and lines,
even if many will never be relevant (basepoints at level 3, for instance). 
*)

(* Reminder of the type-defs:
datatype fpoint = Basepoint nat basepoint | Intersect nat fline fline and
fline =  Join nat fpoint fpoint | Extend nat fline (* | Baseline nat baseline removed to simplify *)
*)

fun nmeets :: "nat  \<Rightarrow> fpoint  \<Rightarrow> fline \<Rightarrow> bool" where
    "nmeets s (Basepoint i X) (Join j (Intersect ii u v)  (Intersect jj y z))  = False" 
  | "nmeets s (Basepoint i X) (Join j (Basepoint u Y)  (Intersect jj y z))  = ((i = 0) \<and> (u = 0) \<and> (X = Y))" 
  | "nmeets s (Basepoint i X) (Join j (Intersect ii u v)(Basepoint x Y) )  = ((i = 0) \<and> (x = 0) \<and> (X = Y))" 
  | "nmeets s (Basepoint i X) (Join j (Basepoint u Z) (Basepoint v Y) )  = ((i = 0) \<and> ((u = 0) \<and> (X = Y)) \<or> 
                                                                                      ((v = 0) \<and> (X = Z)))" 
  | "nmeets s (Basepoint i X) (Extend j l)  = ((i = 0) \<and> ((nmeets (s-1) (Basepoint i X) l)))" 
  
  | "nmeets s (Intersect i k l) (Extend j m)  = ((i = j) \<and> ((k = m) \<or> (l = m)))" 
  | "nmeets s (Intersect i l m) (Join j P Q)  = ((i = j) \<and> 
                                                 ((P = (Intersect i l m)) \<or> (Q = (Intersect i l m))))"
  
fun is_config :: " 'point set  \<Rightarrow> 'line set  \<Rightarrow> ('point   \<Rightarrow> 'line  \<Rightarrow> bool) \<Rightarrow> bool" where
  "is_config Points Lines mmeets = (\<forall> k l P Q. (k \<in> Lines) \<and> (l \<in> Lines) \<and> (k \<noteq> l) \<and> (mmeets P k) \<and> (mmeets P l) 
   \<and> mmeets Q k \<and> mmeets Q l \<longrightarrow> P = Q)"

datatype lline = LLine "fpoint set" (* limit line *)

fun Plevel:: "fpoint\<Rightarrow>nat" where
  "Plevel (Basepoint n x) = n " |
  "Plevel (Intersect n k l) = n"

fun Llevel:: "fline \<Rightarrow> nat" where
  "Llevel (Join n k l) = n" |
  "Llevel (Extend n l) = n"


text \<open>\spike 
Now we'd like to build 
(1) a set, PS, of points for the free projective plane (namely, the union of all the reasonable
points, i.e., basepoints or lines of the form Inter (l, m) where l is "less than" m, and they don't already
have points in common) and
(2) a set of lines, LS, (using the type lline), where a line in our geometry is actually a point set (imagine 
that!) whose intersection with SOME level is a line at that level, and the same is true thereafter, 

Now there's an observation about lines that Hartshorne doesn't mention: suppose that some line in 
$\Pi$ (the free projective plane) intersects level $i$ in some line $k$. Then its intersection 
with level $i+1$ must contain all the points that were in $k$, and possibly a few more, i.e., 
this intersection must be exactly "Extend (i+1) k". So our line in the free projective plane not only 
meets each level in some line at that level, it meets the "same" line at every level (in the sense
that we keep extending k, etc.) And in fact these are the ONLY lines in the free projective plane. 

To capture this notion, and the description of the ith point-set (which is a superset of 
the $(i-1)$th point-set, and the description of the ith line-set (which \emph{replaces} the (i-1)th 
line-set), we need a few predicates (which will be used to construct the set of items satisfying
the predicates). 
\done\<close>

text \<open>\spike 
First, something that tests, given the (i-1)th point- and line-sets, whether some 
fpoint is in fact a "new point" that should be included in the ith point-set. For this to tbe 
the case, there need to be lines k and l at level i-1 that do not meet, and X must be the "Intersect"
point constructed from these, and k must come before l in our order to ensure we don't get duplicates
(and to ensure that k and l are distinct). 
\done\<close>



fun newPoint :: "nat  \<Rightarrow> fpoint set\<Rightarrow> fline set \<Rightarrow> fpoint \<Rightarrow> bool" where
 "newPoint i pts lines X = (\<exists>k l . (k \<in> lines) \<and> (l \<in> lines) \<and>
                            (X = Intersect i k l) \<and> 
                            (llt k l) \<and> 
                            (\<forall> P \<in> pts . \<not>(nmeets i P l \<and> nmeets i P k)))"

text \<open>\spike 
Same kind of things for lines:
\done\<close>

fun newLine :: "nat  \<Rightarrow> fpoint set\<Rightarrow> fline set \<Rightarrow> fline \<Rightarrow> bool" where
 "newLine i pts lines k = (\<exists>P Q . (P \<in> pts) \<and> (Q \<in> pts) \<and>
                            (k = Join i P Q) \<and> 
                            (plt P Q) \<and> 
                            (\<forall> m \<in> lines . \<not>(nmeets (i-1) P m \<and> nmeets (i-1) Q m)))"
text \<open>\spike 
Which "extended" lines should be included in the ith line-set? Extensions of lines that
were in the $i-1$th line-set!
\done\<close>

fun extendedLine :: "nat  \<Rightarrow> fpoint set\<Rightarrow> fline set \<Rightarrow> fline \<Rightarrow> bool" where
 "extendedLine i pts lines k = (\<exists>l . (l \<in> lines)  \<and>
                            (k = Extend i l))" 

text \<open>\spike 
And now we're ready to define the ith point-set and line-set:
\done\<close>


fun Pi:: "nat  \<Rightarrow> fpoint set" 
     and Lambda:: "nat \<Rightarrow> fline set" 
where
  "Pi 0 = {Basepoint 0 AA, Basepoint 0 BB, Basepoint 0 CC, Basepoint 0 DD }"
  | "Pi (Suc n) = Pi(n) \<union> Collect (newPoint (Suc n) (Pi n) (Lambda n)) " 
  | "Lambda 0 = {}"
  | "Lambda (Suc n) = Collect (newLine (Suc n) (Pi n) (Lambda n)) \<union> Collect (extendedLine (Suc n) (Pi n) (Lambda n))"


text \<open>\spike 
A line k "extends" a line n if they're equal, or if there's a chain of "Extends" constructors
leading from one to the other. So a Join fline never extends any line except itself. 
\done\<close>
fun extends:: "fline \<Rightarrow> fline \<Rightarrow> bool" where
 "extends (Join i P Q) (Extend j n)  = False"  |
 "extends (Join i P Q) (Join j R S)  = ( (i = j) \<and> (P = R) \<and> (Q = S))" |
 "extends (Extend i n) (Join j R S)  = ( ((Join j R S) \<in> Lambda(j)) \<and> ((Extend i n) \<in> Lambda(i)) \<and>
                                         (j < i) \<and> (extends n (Join j R S)))" |
 "extends (Extend i n) (Extend j m)  = ( ((Extend j m) \<in> Lambda(j)) \<and> ((Extend i n) \<in> Lambda(i)) \<and>
                                         (j < i) \<and> (extends n m))"
text \<open>\spike 
It's nice to be able to test whether an fpoint P lies on the extension of some fline. Why? Because 
we're going to take each possible "Join" fline, build the set of points that lies on it, and that 
SET will be a line in our free-projective-plane.
\done\<close>

fun lies_on_extension::"fpoint \<Rightarrow> fline \<Rightarrow> bool" where
 "lies_on_extension P (Extend j n)  = False"  |
 "lies_on_extension (Basepoint i XX) (Join j R S)  = ( (i = 0) \<and> (j = 1) \<and> ((R = Basepoint 0 XX)\<or> (S = Basepoint 0 XX)))" |
 "lies_on_extension (Intersect  i k n) (Join j R S)  = ( ((Join j R S) \<in> Lambda(j)) \<and> ((Intersect i k n ) \<in> Pi(i))
                                          \<and> ((extends k (Join j R S))\<or> (extends n (Join j R S))))" 

fun line_points:: "fline \<Rightarrow> fpoint set" where
  "line_points (Join i P Q) = {P, Q}" | 
  "line_points (Extend i k) = line_points(k) \<union> {X . \<exists>l . (l \<in> Lambda(i-1) \<and>
                            (X = Intersect i k l) \<and> 
                            (llt k l) \<and> 
                            (\<forall> P \<in> Pi(i) . \<not>(nmeets i P l \<and> nmeets i P k)))} \<union> 
                                        {X . \<exists>l . (l \<in> Lambda(i-1) \<and>
                            (X = Intersect i l k) \<and> 
                            (llt l k) \<and> 
                            (\<forall> P \<in> Pi(i) . \<not>(nmeets i P l \<and> nmeets i P k)))}"

text \<open>\spike 
We'll say that a point is "a limit point" if it lies in Pi(i) for some i. So the collection of 
all limit points is exactly the point-set for the free projective plane.
\done\<close>
fun is_limit_point:: "fpoint  \<Rightarrow> bool" where
  "is_limit_point (Basepoint 0 X) = True" | 
  "is_limit_point (Intersect i p q) = ((Intersect i p q) \<in> Pi(i))" |
  "is_limit_point Z = False"


definition PS where "PS = {X. is_limit_point(X)}"

text \<open>\spike 
Now for an fline k, we'll define the "limit set of points" to be all points that lie on 
any extension of k.
\done\<close>

fun lsp:: "fline \<Rightarrow> fpoint \<Rightarrow> bool" where
  "lsp k P = lies_on_extension P k" 

text \<open>\spike 
...and then we'll actually construct that set, which (for Join flines) will
constitute a line in the free projective plane. 
\done\<close>

fun UU :: "fline \<Rightarrow> fpoint set" where
  "UU k = {P . lsp k P  }"

text \<open>\spike 
Finally, we're ready to define our "line set", a point-set-set, where each 
point-set is the limit-set-of-points for SOME Join-constructed fline:
\done\<close>

definition LS where
  "LS = {Z . \<exists>k i P Q . ((Z = UU k) \<and> (k = Join i P Q) \<and> (k \<in> Lambda i))}"

text \<open>\spike 
In the free projective plane, where each line really IS just a subset of the set
of points, it's easy to define "meets". 
\done\<close>

fun fmeets:: "fpoint  \<Rightarrow> fpoint set  \<Rightarrow> bool" where
 "fmeets P k = (P \<in> k)"

(* a few lemmas, like "every basepoint is actually a point of the free pp *)
lemma basepoints_in_PS:
  fixes P and X
  assumes "P \<in> PS" 
  assumes "P = Basepoint i X" 
  shows "(i = 0) \<and> (X= AA) \<or> (X=BB) \<or> (X=CC) \<or> (X= DD)"
proof -
  have i0: "i = 0" 
  proof (rule ccontr)
    assume "i \<noteq> 0"
    have "P \<in>PS" using assms(1) by auto 
    have A:"is_limit_point P" using PS_def assms(1) by blast
    have notA: "\<not>(is_limit_point P)" 
      using \<open>i \<noteq> 0\<close> assms(2) free_projective_plane_data.is_limit_point.elims(2) by auto
    thus False using A notA by auto
  qed
  have "P = Basepoint 0 X" by (simp add: \<open>i = 0\<close> assms(2))
  have "(X= AA) \<or> (X=BB) \<or> (X=CC) \<or> (X= DD)"
    using free_projective_plane_data.basepoint.exhaust by blast
  thus ?thesis using i0 by blast
qed


text \<open>
\spike
We'd now like  to assert that \textbf{if} several things are true, namely
\begin{itemize}
\item if $U \in PS$ and $Plevel(U) = 0$, then $U = A,B,C,$ or $D$.  
\item if $k \in LS$ then $Llevel(k) > 0$.  
\item $Join (i P Q) \in LS$ implies that $P,Q \in PS, P \ne Q,  level(P) \le i, level(Q) \le i$ 
and $P$ comes before $Q$ in our lexicographic ordering.
\item $Intersect (i k m) \in PS$ implies that $k,m \in LS, k \ne m, level(k) < i, level(m) < i$, 
and $k$ comes before $m$ in our lexicographic ordering
\end{itemize}
and a couple more that say that whenever two points aren't already on a line, their ``Join'' is in 
the line-set, and the dual of this, \textbf{then} $LS$ and $PS$ cannot contain a Desargues configuration 
because it'd have to be at level zero, which only contains four points. 

Presumably we need some lemmas first, like "if P = Intersect (n k m) and level(l) < n, then NOT meets 
P l" (i.e., k and m are the only lines of level less than n that intersect P). 

But first, we really should show that this "free pp" really IS a projective plane... This proof is still 
very much under construction. With luck, everything above here really is static, and I can 
keep working on this in "FreePlane2", which is the same file, but without lots of text.
\done
\<close>


lemma fpp_a1a: 
  fixes P and Q
  assumes "P \<in> PS"
  assumes "Q \<in> PS"
  assumes "P \<noteq> Q"  
  shows "\<exists>l \<in> LS . fmeets P l \<and> fmeets Q l" 
proof -
  show ?thesis 
  proof (cases P)
    case (Basepoint i X)
    have "(i = 0) \<and> (X= AA) \<or> (X=BB) \<or> (X=CC) \<or> (X= DD)" using basepoints_in_PS Basepoint assms(1) by auto
    have Pform: "P = Basepoint 0 X"
      using Basepoint PS_def assms(1) free_projective_plane_data.is_limit_point.elims(2) by auto 
    show ?thesis
      proof (cases Q)
        case (Basepoint j Y)
        have "(j = 0) \<and> (Y= AA) \<or> (Y=BB) \<or> (Y=CC) \<or> (Y= DD)" using basepoints_in_PS Basepoint assms(2) by auto
        have Qform: "Q = Basepoint 0 Y"
          using Basepoint PS_def assms(2) free_projective_plane_data.is_limit_point.elims(2) by auto 
        then show ?thesis 
        proof -
          have "X \<noteq> Y" using assms(3) Pform Qform by simp
          show ?thesis 
          proof (cases "plt P Q")
            case True
            let ?k = "Join 1 P Q"
            let ?S = "UU ?k"
            have "fmeets P ?S" using fmeets.simps(1) UU.simps lsp.simps  by (simp add: Pform)  
            have "fmeets Q ?S" using fmeets.simps(1) UU.simps lsp.simps  by (simp add: Qform)
  (*          have "Lambda 0 = {}" try 
   "Lambda (Suc n) = Collect (newLine (Suc n) (Pi n) (Lambda n)) \<union> Collect (extendedLine (Suc n) (Pi n) (Lambda n))"
*)
            have L1a: "Lambda (1) = Collect (newLine (1) (Pi 0) (Lambda 0)) \<union> Collect (extendedLine (1) (Pi 0) (Lambda 0))" by simp
            have L1b: "Lambda (1) = Collect (newLine (1) (Pi 0) {}) \<union> Collect (extendedLine (1) (Pi 0) {})" by simp
            have p2emptyA: "\<forall> X . \<not> (extendedLine (1) (Pi 0) {} X)" by simp
            have p2emptyB: "Collect (extendedLine (1) (Pi 0) {}) = {}" using p2emptyA by simp
            have L1c: "Lambda (1) = Collect (newLine (1) (Pi 0) {}) \<union> {}" using L1b p2emptyB by blast
            have L1d: "Lambda (1) = Collect (newLine (1) (Pi 0) {})" using L1c by blast
            have k_in_Lam1: "newLine 1 (Pi 0) {} (Join 1 P Q)" unfolding newLine.simps 
              using Pform Qform True assms(1) assms(2) basepoints_in_PS by auto 
            have k_in_Lam1B: "?k \<in> Lambda 1" using k_in_Lam1 by simp
            have "?S \<in> LS" using LS_def
            proof -
              have zl1: "(Join 1 P Q) \<in> Lambda 1" using k_in_Lam1B by auto
              let ?Z = "UU ?k"
              have big: "?Z = UU ?k \<and> ?k = Join 1 P Q \<and> ?k \<in> Lambda 1" using zl1 by simp
              thus ?thesis using big LS_def by force
            qed
            have c1: "fmeets P  (UU (Join 1 P Q))" 
              using \<open>fmeets P (UU (Join 1 P Q))\<close> by blast
            have c2: "fmeets Q  (UU (Join 1 P Q))" 
              using \<open>fmeets Q (UU (Join 1 P Q))\<close> by blast
            have "(fmeets P  (UU (Join 1 P Q))) \<and> (fmeets Q  (UU (Join 1 P Q)))" using c1 c2 by auto 
            thus ?thesis 
              using \<open>UU (Join 1 P Q) \<in> LS\<close> by blast
          next
            case False
            have ineq: "plt Q P" 
              by (smt Basepoint False Pform \<open>X \<noteq> Y\<close> basepoint.simps(3) 
                    basepoint.simps(5) basepoint.simps(9) free_projective_plane_data.plt.simps(1) lt.elims(3))
            show ?thesis 
            proof-
            let ?k = "Join 1 Q P"
            let ?S = "UU ?k"
            have "fmeets P ?S" using fmeets.simps(1) UU.simps lsp.simps  by (simp add: Pform)  
            have "fmeets Q ?S" using fmeets.simps(1) UU.simps lsp.simps  by (simp add: Qform)
            have L1a: "Lambda (1) = Collect (newLine (1) (Pi 0) (Lambda 0)) \<union> Collect (extendedLine (1) (Pi 0) (Lambda 0))" by simp
            have L1b: "Lambda (1) = Collect (newLine (1) (Pi 0) {}) \<union> Collect (extendedLine (1) (Pi 0) {})" by simp
            have p2emptyA: "\<forall> X . \<not> (extendedLine (1) (Pi 0) {} X)" by simp
            have p2emptyB: "Collect (extendedLine (1) (Pi 0) {}) = {}" using p2emptyA by simp
            have L1c: "Lambda (1) = Collect (newLine (1) (Pi 0) {}) \<union> {}" using L1b p2emptyB by blast
            have L1d: "Lambda (1) = Collect (newLine (1) (Pi 0) {})" using L1c by blast
            have qp0: "Q \<in> Pi 0" 
              using Qform assms(2) basepoints_in_PS by auto
            have pp0: "P \<in> Pi 0" 
              using Pform assms(1) basepoints_in_PS by auto
            have k_in_Lam1: "newLine 1 (Pi 0) {} (Join 1 Q P)" unfolding newLine.simps using qp0 pp0 ineq try by simp
            have k_in_Lam1B: "?k \<in> Lambda 1" using k_in_Lam1 by simp
            have "?S \<in> LS" using LS_def
            proof -
              have zl1: "(Join 1 Q P) \<in> Lambda 1" using k_in_Lam1B by auto
              let ?Z = "UU ?k"
              have big: "?Z = UU ?k \<and> ?k = Join 1 Q P \<and> ?k \<in> Lambda 1" using zl1 by simp
              thus ?thesis using big LS_def by force
            qed
            thus ?thesis
              using \<open>fmeets P (UU (Join 1 Q P))\<close> \<open>fmeets Q (UU (Join 1 Q P))\<close> by blast
          qed
        qed
      qed
    next
      case (Intersect j m n)
        then show ?thesis sorry
      qed
  next
    case (Intersect i k l)
    then show ?thesis 
    proof (cases Q)
      case (Basepoint j A)
      then show ?thesis sorry
    next
      case (Intersect j m n)
      then show ?thesis sorry
    qed
  qed

theorem "projective_plane PS LS fmeets"
  sorry
end