Rewrote methods: wellformed now two lines, uses named theorems. New, more powerful derive method. Used these to rewrite proofs.

6 files changed, 117 insertions, 121 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index b691133..10d3b17 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -18,6 +18,7 @@ section \<open>Symmetry / Path inverse\<close>
 definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
   where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) x y p"
 
+
 lemma inv_type:
   assumes "p : x =\<^sub>A y"
   shows "inv[A,x,y]`p : y =\<^sub>A x"
@@ -64,45 +65,32 @@ section \<open>Transitivity / Path composition\<close>
 text "``Raw'' composition function, of type \<open>\<Prod>x,y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close>."
 
 definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
-  where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A]
+  where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:(x =\<^sub>A y). indEqual[A]
     (\<lambda>x y _. \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)
-    (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:x =\<^sub>A z. indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p)
+    (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p)
     x y p"
 
 text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>."
 
 abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
-  where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. rcompose[A]`x`y`p`z`q"
+  where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:(x =\<^sub>A y). \<^bold>\<lambda>q:(y =\<^sub>A z). rcompose[A]`x`y`p`z`q"
+
+
+lemma compose_type:
+  assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z"
+  shows "compose[A,x,y,z]`p`q : x =\<^sub>A z"
+
+sorry
 
 
 lemma compose_comp:
   assumes "a : A"
   shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
 
-proof (unfold rcompose_def)
-  have "compose[A,a,a,a]`refl(a) \<equiv> \<^bold>\<lambda>q:a =\<^sub>A a. rcompose[A]`a`a`refl(a)`a`q"
-  proof standard+ (*TODO: Set up the Simplifier to handle this proof at some point.*)
-    fix p q assume "p : a =\<^sub>A a" and "q : a =\<^sub>A a"
-    then show "rcompose[A]`a`a`p`a`q : a =\<^sub>A a"
-    proof (unfold rcompose_def)
-      have "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:x =\<^sub>A y. (indEqual[A]
-        (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z)
-        (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>q:x =\<^sub>A z. (indEqual[A] (\<lambda>x z _. x =\<^sub>A z) refl x z q))
-        x y p))`a`a`p`a`q \<equiv> ..." (*Okay really need to set up the Simplifier...*)
-oops
-
-text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
-This would likely involve something like:
-  1. Recognizing that there is a function application that can be simplified.
-  2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
-  3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
-
-lemmas Equal_simps [simp] = inv_comp compose_comp
-
-section \<open>Pretty printing\<close>
-
-abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_\<^sup>-\<^sup>1[_, _, _])" 500)
-  where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p"
-
-abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_ \<bullet>[_, _, _, _]/ _)")
-  where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q"
\ No newline at end of file
+sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close>
+
+
+lemmas Equal_simps [intro] = inv_comp compose_comp
+
+
+end
\ No newline at end of file
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 561dbe6..e5c0776 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -11,13 +11,14 @@ begin
 
 section \<open>Setup\<close>
 
-text "Set up type checking routines, proof methods etc."
+text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments."
 
+named_theorems wellform
 
 section \<open>Metalogical definitions\<close>
 
 text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
-We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ''\<open>a\<close> is a type''."
+We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''."
 
 typedecl Term
 
@@ -35,7 +36,7 @@ consts
 text "The following fact is used to make explicit the assumption of well-formed contexts."
 
 axiomatization where
-  inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U"
+  inhabited_implies_type [intro, elim, wellform]: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
@@ -47,7 +48,7 @@ type_synonym Typefam = "Term \<Rightarrow> Term"
 abbreviation (input) is_type_family :: "[Typefam, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
   where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)"
 
-text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML code, and is for the moment not really crucial."
+\<comment> \<open>There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.\<close>
 
 
 end
\ No newline at end of file
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 7886c1a..bce5123 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -3,7 +3,7 @@
     Date:   Jun 2018
 
 Method setup for the HoTT library.
-Relies on Eisbach, which for the moment lives in HOL/Eisbach.
+Relies heavily on Eisbach.
 *)
 
 theory HoTT_Methods
@@ -16,71 +16,100 @@ theory HoTT_Methods
     Sum
 begin
 
+section \<open>Method setup\<close>
 
-text "This method finds a proof of any valid typing judgment derivable from a given wellformed judgment."
+text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas."
+
+method simple uses lems = (assumption|standard|rule lems)+
+
+
+text "Find a proof of any valid typing judgment derivable from a given wellformed judgment."
 
 method wellformed uses jdgmt = (
-  match jdgmt in
-    "?a : ?A" \<Rightarrow> \<open>
-      rule HoTT_Base.inhabited_implies_type[OF jdgmt] |
-      wellformed jdgmt: HoTT_Base.inhabited_implies_type[OF jdgmt]
-      \<close> \<bar>
-    "A : U" for A \<Rightarrow> \<open>
-      match (A) in
-        "\<Prod>x:?A. ?B x" \<Rightarrow> \<open>
-          print_term "\<Pi>",
-          (rule Prod.Prod_form_cond1[OF jdgmt] |
-          rule Prod.Prod_form_cond2[OF jdgmt] |
-          catch \<open>wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-          catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close>)
-          \<close> \<bar>
-        "\<Sum>x:?A. ?B x" \<Rightarrow> \<open>
-          rule Sum.Sum_form_cond1[OF jdgmt] |
-          rule Sum.Sum_form_cond2[OF jdgmt] |
-          catch \<open>wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-          catch \<open>wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close>
-          \<close> \<bar>
-        "?a =[?A] ?b" \<Rightarrow> \<open>
-          rule Equal.Equal_form_cond1[OF jdgmt] |
-          rule Equal.Equal_form_cond2[OF jdgmt] |
-          rule Equal.Equal_form_cond3[OF jdgmt] |
-          catch \<open>wellformed jdgmt: Equal.Equal_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-          catch \<open>wellformed jdgmt: Equal.Equal_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
-          catch \<open>wellformed jdgmt: Equal.Equal_form_cond3[OF jdgmt]\<close> \<open>fail\<close>
-          \<close>
-      \<close> \<bar>
-    "PROP ?P \<Longrightarrow> PROP Q" for Q \<Rightarrow> \<open>
-      catch \<open>rule Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>rule Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>rule Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>rule Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
-      catch \<open>wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close>
-      \<close>
+  match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
+    catch \<open>rule rl[OF jdgmt]\<close> \<open>fail\<close> |
+    catch \<open>wellformed jdgmt: rl[OF jdgmt]\<close> \<open>fail\<close>
+    )\<close>
   )
 
-notepad  \<comment> \<open>Examples using \<open>wellformed\<close>\<close>
-begin
 
-assume 0: "f : \<Sum>x:A. B x"
-  have "\<Sum>x:A. B x : U" by (wellformed jdgmt: 0)
-  have "A : U" by (wellformed jdgmt: 0)
-  have "B: A \<rightarrow> U" by (wellformed jdgmt: 0)
+text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations."
+
+method derive uses lems = (
+  catch \<open>unfold lems\<close> \<open>fail\<close> |
+  catch \<open>simple lems: lems\<close> \<open>fail\<close> |
+  match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>
+  )+
+
+
+section \<open>Examples\<close>
+
+lemma
+  assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U"
+  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U"
+by (simple lems: assms)
+
+lemma
+  assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z"
+  shows
+    "A : U" and
+    "B: A \<rightarrow> U" and
+    "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and
+    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U"
+proof -
+  show "A : U" by (wellformed jdgmt: assms)
+  show "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
+  show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms)
+  show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms)
+qed
+
+
+section \<open>Experimental methods\<close>
+
+text "Playing around with ML, following CTT/CTT.thy by Larry Paulson."
+
+lemmas forms = Prod_form Sum_form Equal_form
+lemmas intros = Prod_intro Sum_intro Equal_intro
+lemmas elims = Prod_elim Sum_elim Equal_elim
+lemmas elements = intros elims
+
+ML \<open>
+(* Try solving \<open>a : A\<close> by assumption provided \<open>a\<close> is rigid *)
+fun test_assume_tac ctxt = let
+    fun is_rigid (Const(@{const_name is_of_type},_) $ a $ _) = not(is_Var (head_of a))
+      | is_rigid (Const(@{const_name is_a_type},_) $ a $ _ $ _) = not(is_Var (head_of a))
+      | is_rigid _ = false
+  in
+    SUBGOAL (fn (prem, i) =>
+      if is_rigid (Logic.strip_assums_concl prem)
+      then assume_tac ctxt i else no_tac)
+  end
+
+fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i
+
+(* Solve all subgoals \<open>A : U\<close> using formation rules. *)
+val form_net = Tactic.build_net @{thms forms};
+fun form_tac ctxt =
+  REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net));
 
-assume 1: "f : \<Prod>x:A. \<Prod>y: B x. C x y"
-  have "A : U" by (wellformed jdgmt: 1)
-  have "B: A \<rightarrow> U" by (wellformed jdgmt: 1)
-  have "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: 1)
+(* Try to prove inhabitation judgments \<open>a : A\<close> (\<open>a\<close> flexible, \<open>A\<close> rigid) by introduction rules. *)
+fun intro_tac ctxt thms =
+  let val tac =
+    filt_resolve_from_net_tac ctxt 1
+      (Tactic.build_net (thms @ @{thms forms} @ @{thms intros}))
+  in  REPEAT_FIRST (ASSUME ctxt tac)  end
 
-assume 2: "g : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z"
-  have a: "A : U" by (wellformed jdgmt: 2)
-  have b: "B: A \<rightarrow> U" by (wellformed jdgmt: 2)
-  have c: "\<And>x. x : A \<Longrightarrow> C x : B x \<rightarrow> U" by (wellformed jdgmt: 2)
-  have d: "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y : C x y \<rightarrow> U" by (wellformed jdgmt: 2)
+(*Type checking: solve \<open>a : A\<close> (\<open>a\<close> rigid, \<open>A\<close> flexible) by formation, introduction and elimination rules. *)
+fun typecheck_tac ctxt thms =
+  let val tac =
+    filt_resolve_from_net_tac ctxt 3
+      (Tactic.build_net (thms @ @{thms forms} @ @{thms elements}))
+  in  REPEAT_FIRST (ASSUME ctxt tac)  end
+\<close>
 
-end
+method_setup form = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\<close>
+method_setup intro = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intro_tac ctxt ths))\<close>
+method_setup typecheck = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typecheck_tac ctxt ths))\<close>
 
 
 end
\ No newline at end of file
diff --git a/Prod.thy b/Prod.thy
index 162b2e6..18582a8 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -59,8 +59,7 @@ This is what the additional formation rules \<open>Prod_form_cond1\<close> and \
 text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:"
 
 lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
-lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2
-lemmas Prod_simps [simp] = Prod_comp Prod_uniq
+lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2
 
 text "Nondependent functions are a special case."
 
diff --git a/Proj.thy b/Proj.thy
index c4703d7..fe80c4c 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -49,16 +49,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 lemma fst_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "fst[A,B]`p : A"
-
-proof
-  show "fst[A,B]: (\<Sum>x:A. B x) \<rightarrow> A"
-  proof (unfold fst_dep_def, standard)
-    show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
-    proof
-      show "A : U" by (wellformed jdgmt: assms)
-    qed
-  qed (wellformed jdgmt: assms)
-qed (rule assms)
+  by (derive lems: fst_dep_def assms)
 
 
 lemma fst_dep_comp:
@@ -67,18 +58,10 @@ lemma fst_dep_comp:
 
 proof -
   have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
-  proof (unfold fst_dep_def, standard)
-    show "(a,b) : \<Sum>x:A. B x" using assms ..
-    show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
-    proof
-      show "A : U" by (wellformed jdgmt: assms(2))
-    qed
-  qed
+    by (derive lems: fst_dep_def assms)
   
   also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
-  proof
-    show "A : U" by (wellformed jdgmt: assms(2))
-  qed (assumption, (rule assms)+)
+    by (derive lems: assms)
   
   finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
@@ -89,12 +72,8 @@ text "In proving results about the second dependent projection function we often
 lemma lemma1:
   assumes "p : \<Sum>x:A. B x"
   shows "B (fst[A,B]`p) : U"
+  by (derive lems: assms fst_dep_def)
 
-proof -
-  have *: "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
-  have "fst[A,B]`p : A" using assms by (rule fst_dep_type)
-  then show "B (fst[A,B]`p) : U" by (rule *)
-qed
 
 lemma lemma2:
   assumes "B: A \<rightarrow> U" and "x : A" and "y : B x"
@@ -110,7 +89,7 @@ lemma snd_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "snd[A,B]`p : B (fst[A,B]`p)"
 
-proof
+proof (derive lems: assms snd_dep_def)
   show "snd[A, B] : \<Prod>p:(\<Sum>x:A. B x). B (fst[A,B]`p)"
   proof (unfold snd_dep_def, standard)
     show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)"
@@ -216,7 +195,7 @@ lemma snd_nondep_comp:
 proof -
   have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)"
   proof (unfold snd_nondep_def, standard)
-    show "(a,b) : A \<times> B" using assms ..
+    show "(a,b) : A \<times> B" by (simple conds: assms)
     show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p : B"
     proof
       show "B : U" by (wellformed jdgmt: assms(2))
diff --git a/Sum.thy b/Sum.thy
index 8f40b74..7e688a2 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -51,7 +51,7 @@ and
     \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
-lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2
+lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2
 
 \<comment> \<open>Nondependent pair\<close>
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)