From 257561ff4036d0eb5b51e649f2590b61e08d6fc5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 15 Aug 2018 12:42:52 +0200 Subject: Basic compute method --- EqualProps.thy | 12 ++++++------ HoTT_Methods.thy | 4 ++++ Prod.thy | 2 +- ex/Methods.thy | 29 +++++++++++++++++++++++++++++ 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) \ refl(a)" unfolding reqcompose_def -proof (subst comp) +proof compute { fix x assume 1: "x: A" show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" proof @@ -120,7 +120,7 @@ proof (subst comp) qed (rule assms) } show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \ refl(a)" - proof (subst comp) + proof compute { fix y assume 1: "y: A" show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: a =\<^sub>A y \ (\z:A. y =\<^sub>A z \ a =\<^sub>A z)" proof @@ -141,7 +141,7 @@ proof (subst comp) qed (simple lems: assms 1) } show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" - proof (subst comp) + proof compute { fix p assume 1: "p: a =\<^sub>A a" show "ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p: \z:A. a =\<^sub>A a \ 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>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" - proof (subst comp) + proof compute { fix u assume 1: "u: A" show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A u\ u =\<^sub>A z" proof @@ -171,7 +171,7 @@ proof (subst comp) qed fact } show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" - proof (subst comp) + proof compute { fix a assume 1: "a: A" show "\<^bold>\q. ind\<^sub>= refl q: a =\<^sub>A a \ a =\<^sub>A a" proof @@ -180,7 +180,7 @@ proof (subst comp) qed (simple lems: assms 1) } show "(\<^bold>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" - proof (subst comp) + proof compute show "\p. p: a =\<^sub>A a \ 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)) \ 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: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_comp: "\a: A; \x. x: A \ b(x): B(x)\ \ (\<^bold>\x. b(x))`a \ b(a)" and Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ 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 \ U(i)" "\x. x : A \ C x: B x \ U(i)" shows "\x:A. \y:B x. \z:C x y. \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>\x. )`a \ " +proof compute + show "\x. x: A \ : A \ \" by simple +qed (simple lems: assms) + + +lemma + assumes "A: U(i)" "B: A \ U(i)" "a: A" "b: B(a)" + shows "(\<^bold>\x y. )`a`b \ " +proof compute + show "\x. x: A \ \<^bold>\y. : \y:B(x). \x:A. B(x)" by (simple lems: assms) + + show "(\<^bold>\b. )`b \ " + proof compute + show "\b. b: B(a) \ : \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 \ 0" and "\n. n: \ \ (?p`(succ n)) \ 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: \ \ \" unfolding pred_def by simpl lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" proof (simple lems: pred_type) have *: "pred`0 \ 0" unfolding pred_def - proof (subst comp) + proof compute show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple show "ind\<^sub>\ (\a b. a) 0 0 \ 0" proof (rule Nat_comps) @@ -63,10 +63,10 @@ proof (simple lems: pred_type) show "\<^bold>\n. refl(n): \n:\. (pred`(succ(n))) =\<^sub>\ n" unfolding pred_def proof show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) n n)`succ(n)) =\<^sub>\ n" - proof (subst comp) + proof compute show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) (succ n) (succ n) =\<^sub>\ n" - proof (subst comp) + proof compute show "\: U(O)" .. qed simple qed rule -- cgit v1.2.3