theory Question4
imports Complex_Main
begin
  datatype a2pt = A2Point "real" "real"
  datatype a2ln = A2Ordinary "real" "real" 
                | A2Vertical "real"
  text "Ordinary m b represents the line y = mx+b; Vertical xo is the line x = xo "

  fun a2meets :: "a2pt \<Rightarrow> a2ln \<Rightarrow> bool" where
    "a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
    "a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"

  lemma A2_a1: "P \<noteq> Q \<Longrightarrow> \<exists>! l . a2meets P l \<and> a2meets Q l"
  proof -
    assume P_ne_Q: "P \<noteq> Q"
    show "\<exists>! l . a2meets P l \<and> a2meets Q l"
    proof (cases P, cases Q)
      fix px py qx qy
      assume P: "P = A2Point px py"
      assume Q: "Q = A2Point qx qy"
      show "\<exists>! l . a2meets P l \<and> a2meets Q l"
      proof (cases "px = qx")
        assume eq: "px = qx"
        show "\<exists>!l. a2meets P l \<and> a2meets Q l"
        proof
          show "a2meets P (A2Vertical px) \<and> a2meets Q (A2Vertical px)"
            using P Q eq by simp
          show "\<And>l. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical px"
          proof -
            fix l
            show "a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical px"
            proof (cases l)
              show "\<And>m b. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Ordinary m b \<Longrightarrow> l = A2Vertical px"
                using P Q P_ne_Q eq by simp
              show "\<And>x. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Vertical x \<Longrightarrow> l = A2Vertical px"
                using P by simp
            qed
          qed
        qed
        next
        assume neq: "px \<noteq> qx"
        show "\<exists>!l. a2meets P l \<and> a2meets Q l"
        proof
          let ?m = "(qy - py)/(qx - px)"
          let ?b = "py - ?m * px"
          have *: "py = ?m * px + ?b \<and> qy = ?m * qx + ?b"
          proof -
            have "?m * qx - ?m * px + py = ?m * (qx - px) + py"
              by argo
            also have "... = qy - py + py"
              using neq by simp
            also have "... = qy"
              by simp
            finally show ?thesis by simp
          qed
          show "a2meets P (A2Ordinary ?m ?b) \<and> a2meets Q (A2Ordinary ?m ?b)"
            using * P Q by simp
          show "\<And>l. a2meets P l \<and> a2meets Q l \<Longrightarrow> l = A2Ordinary ?m (py - ?m * px)"
          proof -
            fix l
            assume l: "a2meets P l \<and> a2meets Q l"
            show "l = A2Ordinary ?m (py - ?m * px)"
            proof (cases l)
              case (A2Ordinary m b)
              assume 1: "l = A2Ordinary m b"
              have "py = m * px + b \<and> qy = m * qx + b"
                using P Q l 1 by simp
              hence "m = ?m \<and> b = ?b"
                using neq by (smt "*" crossproduct_noteq)  (* Found with sledgehammer *)
              thus "l = A2Ordinary ?m ?b"
                using 1 by simp
            next
              case (A2Vertical x)
              assume 1: "l = A2Vertical x"
              then show "l = A2Ordinary ?m ?b"
                (*
                 * This is false, something of the form A2Vertical cannot equal
                 * something of the form A2Ordinary (the datatype is freely generated
                 * by its constructors).
                 *
                 * So uniqueness fails because if l = A2Vertical x with x = px and x = qx
                 * then a2meets P l and a2meets Q l according to your definition.
                 *)
                sorry
            qed
          qed
        qed
      qed
    qed
  qed

end