Basic compute method

2 files changed, 34 insertions, 5 deletions

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