From 962fc96123039b53b9c6946796e909fb50ec9004 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 13 Aug 2018 10:37:20 +0200 Subject: rcompose done --- Equal.thy | 12 ++++----- EqualProps.thy | 78 ++++++++++++++++++++++++++++++++++++++++++++-------------- Nat.thy | 1 + Prod.thy | 22 ++++++----------- Proj.thy | 19 +++++++++----- Sum.thy | 2 +- scratch.thy | 49 ++++++++++++------------------------ 7 files changed, 105 insertions(+), 78 deletions(-) diff --git a/Equal.thy b/Equal.thy index d910bb8..93f623f 100644 --- a/Equal.thy +++ b/Equal.thy @@ -15,7 +15,7 @@ section \Constants and syntax\ axiomatization Equal :: "[Term, Term, Term] \ Term" and refl :: "Term \ Term" and - indEqual :: "[Term \ Term, Term, Term, Term] \ Term" ("(1ind\<^sub>=)") + indEqual :: "[Term \ Term, Term] \ Term" ("(1ind\<^sub>=)") syntax "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) @@ -35,16 +35,16 @@ and Equal_elim: "\ \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i); \x. x: A \ f(x) : C(x)(x)(refl x); - a: A; - b: A; + x: A; + y: A; p: a =\<^sub>A b - \ \ ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)" + \ \ ind\<^sub>=(f)(p) : C(x)(y)(p)" and Equal_comp: "\ \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i); \x. x: A \ f(x) : C(x)(x)(refl x); a: A - \ \ ind\<^sub>=(f)(a)(a)(refl(a)) \ f(a)" + \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" text "Admissible inference rules for equality type formation:" (* @@ -56,7 +56,7 @@ and Equal_form_cond3: "a =\<^sub>A b: U(i) \ b: A" *) lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -(*lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*) +(*lemmas Equal_wellform [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*) lemmas Equal_comps [comp] = Equal_comp diff --git a/EqualProps.thy b/EqualProps.thy index 9d23a99..d645fb6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -15,20 +15,20 @@ begin section \Symmetry / Path inverse\ -definition inv :: "[Term, Term] \ (Term \ Term)" ("(1inv[_,/ _])") - where "inv[x,y] \ \p. ind\<^sub>= (\x. refl(x)) x y p" +axiomatization inv :: "Term \ Term" ("_\" [1000] 1000) + where inv_def: "inv \ \p. ind\<^sub>= (\x. refl(x)) p" lemma inv_type: - assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): y =\<^sub>A x" + assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\: y =\<^sub>A x" unfolding inv_def -proof +proof (rule Equal_elim[where ?x=x and ?y=y]) \ \Path induction\ show "\x y. \x: A; y: A\ \ y =\<^sub>A x: U(i)" using assms(1) .. show "\x. x: A \ refl x: x =\<^sub>A x" .. qed (fact assms)+ -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \ refl(a)" +lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" unfolding inv_def proof show "\x. x: A \ refl x: x =\<^sub>A x" .. @@ -38,24 +38,66 @@ qed (fact assms) section \Transitivity / Path composition\ -text "``Raw'' composition function, of type \\x,y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\." +text " + Raw composition function, of type \\x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\ polymorphic over the type \A\. +" + +axiomatization rcompose :: Term where + rcompose_def: "rcompose \ \<^bold>\x y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= (\x. refl(x)) q) p" + -definition rcompose :: "Term \ Term" ("(1rcompose[_])") - where "rcompose[A] \ \<^bold>\x:A. \<^bold>\y:A. \<^bold>\p:(x =\<^sub>A y). indEqual[A] - (\x y _. \z:A. y =\<^sub>A z \ x =\<^sub>A z) - (\x. \<^bold>\z:A. \<^bold>\p:(x =\<^sub>A z). indEqual[A](\x z _. x =\<^sub>A z) (\x. refl(x)) x z p) - x y p" +lemma rcompose_type: + assumes "A: U(i)" + shows "rcompose: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" +unfolding rcompose_def +proof + show "\x. x: A \ + \<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" + proof + show "\x y. \x: A ; y: A\ \ + \<^bold>\p. ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" + proof + { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y" + show "ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: \z:A. y =[A] z \ x =[A] z" + proof (rule Equal_elim[where ?x=x and ?y=y]) + show "\x y. \x: A; y: A\ \ \z:A. y =\<^sub>A z \ x =\<^sub>A z: U(i)" + proof + show "\x y z. \x: A; y: A; z: A\ \ y =\<^sub>A z \ x =\<^sub>A z: U(i)" + by (rule Prod_form Equal_form assms | assumption)+ + qed (rule assms) + + show "\x. x: A \ \<^bold>\z p. ind\<^sub>= refl p: \z:A. x =\<^sub>A z \ x =\<^sub>A z" + proof + show "\x z. \x: A; z: A\ \ \<^bold>\p. ind\<^sub>= refl p: x =\<^sub>A z \ x =\<^sub>A z" + proof + { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z" + show "ind\<^sub>= refl p: x =[A] z" + proof (rule Equal_elim[where ?x=x and ?y=z]) + show "\x y. \x: A; y: A\ \ x =\<^sub>A y: U(i)" by standard (rule assms) + show "\x. x: A \ refl x: x =\<^sub>A x" .. + qed (fact asm)+ } + show "\x z. \x: A; z: A\ \ x =\<^sub>A z: U(i)" by standard (rule assms) + qed + qed (rule assms) + qed (rule asm)+ } + show "\x y. \x: A; y: A\ \ x =\<^sub>A y: U(i)" by standard (rule assms) + qed + qed (rule assms) +qed (fact assms) +corollary + assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + shows "rcompose`x`y`p`z`q: x =\<^sub>A z" + by standard+ (rule rcompose_type assms)+ -definition compose :: "[Term, Term, Term] \ [Term, Term] \ Term" ("(1compose[ _,/ _,/ _])") - where "compose[x,y,z] \ \p." +axiomatization compose :: "[Term, Term] \ Term" (infixl "\" 60) where + compose_comp: "\ + A: U(i); + x: A; y: A; z: A; + p: x =\<^sub>A y; q: y =\<^sub>A z + \ \ p \ q \ rcompose`x`y`p`z`q" -lemma compose_type: - assumes "A : U(i)" and "x : A" and "y : A" and "z : A" - shows "compose[A,x,y,z] : x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z" - unfolding rcompose_def - by (derive lems: assms) lemma compose_comp: assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" diff --git a/Nat.thy b/Nat.thy index bd2c4ca..eed9226 100644 --- a/Nat.thy +++ b/Nat.thy @@ -43,6 +43,7 @@ and \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ f a n)" lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2 +lemmas Nat_intro = Nat_intro1 Nat_intro2 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 diff --git a/Prod.thy b/Prod.thy index 5391943..76b66dd 100644 --- a/Prod.thy +++ b/Prod.thy @@ -14,23 +14,19 @@ section \Constants and syntax\ axiomatization Prod :: "[Term, Typefam] \ Term" and - lambda :: "[Term, Term \ Term] \ Term" and - appl :: "[Term, Term] \ Term" ("(1_`_)" [61, 60] 60) + lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 30) and + appl :: "[Term, Term] \ Term" (infixl "`" 60) \ \Application binds tighter than abstraction.\ syntax "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) - "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(1\<^bold>\_:_./ _)" 30) "_PROD_ASCII" :: "[idt, Term, Term] \ Term" ("(3PROD _:_./ _)" 30) - "_LAMBDA_ASCII" :: "[idt, Term, Term] \ Term" ("(3%%_:_./ _)" 30) text "The translations below bind the variable \x\ in the expressions \B\ and \b\." translations "\x:A. B" \ "CONST Prod A (\x. B)" - "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" "PROD x:A. B" \ "CONST Prod A (\x. B)" - "%%x:A. b" \ "CONST lambda A (\x. b)" text "Nondependent functions are a special case." @@ -43,21 +39,20 @@ section \Type rules\ axiomatization where Prod_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Prod_intro: "\A: U(i); \x. x: A \ b(x): B(x)\ \ \<^bold>\x:A. b(x): \x:A. B(x)" + Prod_intro: "\A: U(i); \x. x: A \ b(x): B(x)\ \ \<^bold>\x. b(x): \x:A. B(x)" and Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\a: A; \x. x: A \ b(x): B(x)\ \ (\<^bold>\x:A. 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:A. (f`x) \ f" + Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" text " Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation). " -(* text " - In addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \\x:A. B x: U(i)\ is derivable from some set of premises \, then so are \A: U(i)\ and \B: A \ U(i)\. + In addition to the usual type rules, it is a meta-theorem that whenever \\x:A. B x: U(i)\ is derivable from some set of premises \, then so are \A: U(i)\ and \B: A \ U(i)\. That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. " @@ -66,12 +61,11 @@ axiomatization where Prod_form_cond1: "(\x:A. B(x): U(i)) \ A: U(i)" and Prod_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" -*) text "Set up the standard reasoner to use the type rules:" -lemmas Prod_rules = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq -(*lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2*) +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 lemmas Prod_comps [comp] = Prod_comp Prod_uniq diff --git a/Proj.thy b/Proj.thy index b1c21c1..e90cd95 100644 --- a/Proj.thy +++ b/Proj.thy @@ -13,21 +13,23 @@ theory Proj begin -abbreviation fst :: "Term \ Term" where "fst \ \p. ind\<^sub>\(\x y. x)(p)" -abbreviation snd :: "Term \ Term" where "snd \ \p. ind\<^sub>\(\x y. y)(p)" +axiomatization fst :: "Term \ Term" where fst_def: "fst \ \p. ind\<^sub>\(\x y. x)(p)" +axiomatization snd :: "Term \ Term" where snd_def: "snd \ \p. ind\<^sub>\(\x y. y)(p)" text "Typing judgments and computation rules for the dependent and non-dependent projection functions." lemma fst_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "fst(p): A" +unfolding fst_def proof - show "A: U(i)" using assms(1) by (rule Sum_forms) + show "A: U(i)" using assms(1) by (rule Sum_wellform) qed (fact assms | assumption)+ lemma fst_comp: assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ a" +unfolding fst_def proof show "\x. x: A \ x: A" . qed (rule assms)+ @@ -35,25 +37,27 @@ qed (rule assms)+ lemma snd_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" +unfolding snd_def proof show "\p. p: \x:A. B(x) \ B(fst p): U(i)" proof - have "\p. p: \x:A. B(x) \ fst(p): A" using assms(1) by (rule fst_type) - with assms(1) show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (rule Sum_forms) + with assms(1) show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (rule Sum_wellform) qed fix x y assume asm: "x: A" "y: B(x)" show "y: B(fst )" proof (subst fst_comp) - show "A: U(i)" using assms(1) by (rule Sum_forms) - show "\x. x: A \ B(x): U(i)" using assms(1) by (rule Sum_forms) + show "A: U(i)" using assms(1) by (rule Sum_wellform) + show "\x. x: A \ B(x): U(i)" using assms(1) by (rule Sum_wellform) qed (rule asm)+ qed (fact assms) lemma snd_comp: assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ b" +unfolding snd_def proof show "\x y. y: B(x) \ y: B(x)" . show "a: A" by (fact assms) @@ -63,4 +67,7 @@ proof qed +lemmas Proj_comps [intro] = fst_comp snd_comp + + end \ No newline at end of file diff --git a/Sum.thy b/Sum.thy index eddb464..145c303 100644 --- a/Sum.thy +++ b/Sum.thy @@ -60,7 +60,7 @@ and Sum_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_forms = Sum_form Sum_form_cond1 Sum_form_cond2 +lemmas Sum_wellform [wellform] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp diff --git a/scratch.thy b/scratch.thy index 3141120..25d2ca7 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,66 +3,49 @@ theory scratch begin - -lemma "U(O): U(O)" -proof (rule inhabited_implies_type) - show "\: U(O)" .. -qed - lemma - assumes "\x:A. B(x): U(i)" "(a,b): \x:A. B(x)" + assumes "\x:A. B(x): U(i)" ": \x:A. B(x)" shows "a : A" -proof (rule Sum_form_conds) +proof +oops -abbreviation pred where "pred \ \<^bold>\n:\. ind\<^sub>\(\n c. n, 0, n)" +abbreviation pred where "pred \ \<^bold>\n. ind\<^sub>\(\n c. n) 0 n" schematic_goal "?a: (pred`0) =\<^sub>\ 0" apply (subst comp) -apply (rule Nat_form) -prefer 4 apply (subst comp) +apply (rule Nat_intro) +prefer 2 apply (subst comp) apply (rule Nat_form) apply assumption -apply (rule Nat_intro1) +apply (rule Nat_intro) apply (rule Equal_intro) -apply (rule Nat_intro1) -prefer 2 apply (rule Nat_elim) +apply (rule Nat_intro) +apply (rule Nat_elim) apply (rule Nat_form) apply assumption apply (rule Nat_intro1) apply assumption -apply (rule Nat_form) done schematic_goal "?a : \n:\. (pred`(succ n)) =\<^sub>\ n" apply (rule Prod_intro) apply (rule Nat_form) apply (subst comp) -apply (rule Nat_form) -prefer 2 apply (rule Nat_elim) +apply (rule Nat_intro) +apply assumption +prefer 2 apply (subst comp) apply (rule Nat_form) apply assumption -apply (rule Nat_intro1) +apply (rule Nat_intro) +apply assumption +apply (rule Equal_intro) apply assumption -apply (rule Nat_form) -apply (rule Nat_intro2, assumption) -apply (rule Equal_form) -apply (rule Nat_form) apply (rule Nat_elim) apply (rule Nat_form) apply assumption -apply (rule Nat_rules)+ -apply assumption+ -apply (subst comp) -apply (rule Nat_form) -prefer 2 apply (rule Nat_elim) -defer -apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+ -apply (subst Nat_comps) -apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+ -apply (rule Equal_intro) +apply (rule Nat_intro) apply assumption -apply (rule Nat_form) done schematic_goal "?a : \p:\\\. \n:\. (p`(succ n)) =\<^sub>\ n" -- cgit v1.2.3