Basic compute method

5 files changed, 45 insertions, 12 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index 9b43345..2a13ed2 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -96,7 +96,7 @@ lemma reqcompose_comp:
   assumes "A: U(i)" and "a: A"
   shows "reqcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)"
 unfolding reqcompose_def
-proof (subst comp)
+proof compute
   { fix x assume 1: "x: A"
   show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
   proof
@@ -120,7 +120,7 @@ proof (subst comp)
   qed (rule assms) }
 
   show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)"
-  proof (subst comp)
+  proof compute
     { fix y assume 1: "y: A"
     show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)"
       proof
@@ -141,7 +141,7 @@ proof (subst comp)
       qed (simple lems: assms 1) }
     
     show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)"
-    proof (subst comp)
+    proof compute
       { fix p assume 1: "p: a =\<^sub>A a"
       show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A a \<rightarrow> a =\<^sub>A z"
       proof (rule Equal_elim[where ?x=a and ?y=a])
@@ -158,7 +158,7 @@ proof (subst comp)
       qed (simple lems: assms 1) }
       
       show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)"
-      proof (subst comp)
+      proof compute
         { fix u assume 1: "u: A"
         show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z"
         proof
@@ -171,7 +171,7 @@ proof (subst comp)
         qed fact }
         
         show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)"
-        proof (subst comp)
+        proof compute
           { fix a assume 1: "a: A"
           show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
           proof
@@ -180,7 +180,7 @@ proof (subst comp)
           qed (simple lems: assms 1) }
           
           show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)"
-          proof (subst comp)
+          proof compute
             show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
             by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms)
             show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)"
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index d7f0821..d3aed66 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -60,5 +60,9 @@ ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
 ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
 ML_file "~~/src/Tools/eqsubst.ML"
 
+text "Perform basic single-step computations:"
+
+method compute uses lems = (subst comp lems)
+
 
 end
\ No newline at end of file
diff --git a/Prod.thy b/Prod.thy
index 59c6cc3..496bf3e 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -43,7 +43,7 @@ and
 and
   Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)"
 and
-  Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)"
+  Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)"
 and
   Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f"
 
diff --git a/ex/Methods.thy b/ex/Methods.thy
index 699d620..871964f 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -10,6 +10,8 @@ theory Methods
 begin
 
 
+text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules."
+
 lemma
   assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)"
   shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)"
@@ -45,4 +47,31 @@ apply (rule Sum_intro)
 apply assumption+
 done
 
+
+text "
+  Function application.
+  The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types.
+"
+
+lemma
+  assumes "A: U(i)" "a: A"
+  shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
+proof compute
+  show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by simple
+qed (simple lems: assms)
+
+
+lemma
+  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)"
+  shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
+proof compute
+  show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (simple lems: assms)
+
+  show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>"
+  proof compute
+    show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (simple lems: assms)
+  qed fact
+qed fact
+
+
 end
\ No newline at end of file
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index 48d762c..ef6673c 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -33,8 +33,8 @@ text "
 "
 
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
-apply (subst comp)
-prefer 4 apply (subst comp)
+apply compute
+prefer 4 apply compute
 prefer 3 apply (rule Nat_rules)
 apply (rule Nat_rules | assumption)+
 done
@@ -51,7 +51,7 @@ lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simpl
 lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
 proof (simple lems: pred_type)
   have *: "pred`0 \<equiv> 0" unfolding pred_def
-  proof (subst comp)
+  proof compute
     show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple
     show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
     proof (rule Nat_comps)
@@ -63,10 +63,10 @@ proof (simple lems: pred_type)
   show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n"
   unfolding pred_def proof
     show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) n n)`succ(n)) =\<^sub>\<nat> n"
-    proof (subst comp)
+    proof compute
       show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple
       show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) (succ n) (succ n) =\<^sub>\<nat> n"
-      proof (subst comp)
+      proof compute
         show "\<nat>: U(O)" ..
       qed simple
     qed rule