diff options
| -rw-r--r-- | EqualProps.thy | 12 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 4 | ||||
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | ex/Methods.thy | 29 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 10 |
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 @@ -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 |