diff options
| -rw-r--r-- | Equal.thy | 12 | ||||
| -rw-r--r-- | EqualProps.thy | 78 | ||||
| -rw-r--r-- | Nat.thy | 1 | ||||
| -rw-r--r-- | Prod.thy | 22 | ||||
| -rw-r--r-- | Proj.thy | 19 | ||||
| -rw-r--r-- | Sum.thy | 2 | ||||
| -rw-r--r-- | scratch.thy | 49 |
7 files changed, 105 insertions, 78 deletions
@@ -15,7 +15,7 @@ section \<open>Constants and syntax\<close> axiomatization Equal :: "[Term, Term, Term] \<Rightarrow> Term" and refl :: "Term \<Rightarrow> Term" and - indEqual :: "[Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)") + indEqual :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)") syntax "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) @@ -35,16 +35,16 @@ and Equal_elim: "\<lbrakk> \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x); - a: A; - b: A; + x: A; + y: A; p: a =\<^sub>A b - \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)" + \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(p) : C(x)(y)(p)" and Equal_comp: "\<lbrakk> \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x); a: A - \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(a)(refl(a)) \<equiv> f(a)" + \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(refl(a)) \<equiv> f(a)" text "Admissible inference rules for equality type formation:" (* @@ -56,7 +56,7 @@ and Equal_form_cond3: "a =\<^sub>A b: U(i) \<Longrightarrow> 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 \<open>Symmetry / Path inverse\<close> -definition inv :: "[Term, Term] \<Rightarrow> (Term \<Rightarrow> Term)" ("(1inv[_,/ _])") - where "inv[x,y] \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) x y p" +axiomatization inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) + where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>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\<inverse>: y =\<^sub>A x" unfolding inv_def -proof +proof (rule Equal_elim[where ?x=x and ?y=y]) \<comment> \<open>Path induction\<close> show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) .. show "\<And>x. x: A \<Longrightarrow> 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)) \<equiv> refl(a)" +lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" unfolding inv_def proof show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. @@ -38,24 +38,66 @@ qed (fact assms) section \<open>Transitivity / Path composition\<close> -text "``Raw'' composition function, of type \<open>\<Prod>x,y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close>." +text " + Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. +" + +axiomatization rcompose :: Term where + rcompose_def: "rcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" + -definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") - where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:(x =\<^sub>A y). indEqual[A] - (\<lambda>x y _. \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z) - (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p) - x y p" +lemma rcompose_type: + assumes "A: U(i)" + shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" +unfolding rcompose_def +proof + show "\<And>x. x: A \<Longrightarrow> + \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + proof + show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow> + \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + proof + { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z" + proof (rule Equal_elim[where ?x=x and ?y=y]) + show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" + proof + show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" + by (rule Prod_form Equal_form assms | assumption)+ + qed (rule assms) + + show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z" + proof + show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> 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 "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms) + show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. + qed (fact asm)+ } + show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms) + qed + qed (rule assms) + qed (rule asm)+ } + show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> 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] \<Rightarrow> [Term, Term] \<Rightarrow> Term" ("(1compose[ _,/ _,/ _])") - where "compose[x,y,z] \<equiv> \<lambda>p." +axiomatization compose :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where + compose_comp: "\<lbrakk> + A: U(i); + x: A; y: A; z: A; + p: x =\<^sub>A y; q: y =\<^sub>A z + \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> 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 \<rightarrow> y =\<^sub>A z \<rightarrow> 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) \<equiv> refl(a)" @@ -43,6 +43,7 @@ and \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> 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 @@ -14,23 +14,19 @@ section \<open>Constants and syntax\<close> axiomatization Prod :: "[Term, Typefam] \<Rightarrow> Term" and - lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and - appl :: "[Term, Term] \<Rightarrow> Term" ("(1_`_)" [61, 60] 60) + lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 30) and + appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) - "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(1\<^bold>\<lambda>_:_./ _)" 30) "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30) - "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3%%_:_./ _)" 30) text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>." translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)" - "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)" "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)" - "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)" text "Nondependent functions are a special case." @@ -43,21 +39,20 @@ section \<open>Type rules\<close> axiomatization where Prod_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)" and - Prod_intro: "\<lbrakk>A: U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x): \<Prod>x:A. B(x)" + Prod_intro: "\<lbrakk>A: U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)" and Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)" and - Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. 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:A. (f`x) \<equiv> f" + Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f" text " Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>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 \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>. + In addition to the usual type rules, it is a meta-theorem that whenever \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>. 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: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" and Prod_form_cond2: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> 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 @@ -13,21 +13,23 @@ theory Proj begin -abbreviation fst :: "Term \<Rightarrow> Term" where "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)" -abbreviation snd :: "Term \<Rightarrow> Term" where "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)" +axiomatization fst :: "Term \<Rightarrow> Term" where fst_def: "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)" +axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)" text "Typing judgments and computation rules for the dependent and non-dependent projection functions." lemma fst_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>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 \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a" +unfolding fst_def proof show "\<And>x. x: A \<Longrightarrow> x: A" . qed (rule assms)+ @@ -35,25 +37,27 @@ qed (rule assms)+ lemma snd_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)" +unfolding snd_def proof show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" proof - have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type) - with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_forms) + with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_wellform) qed fix x y assume asm: "x: A" "y: B(x)" show "y: B(fst <x,y>)" proof (subst fst_comp) - show "A: U(i)" using assms(1) by (rule Sum_forms) - show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_forms) + show "A: U(i)" using assms(1) by (rule Sum_wellform) + show "\<And>x. x: A \<Longrightarrow> 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 \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b" +unfolding snd_def proof show "\<And>x y. y: B(x) \<Longrightarrow> 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 @@ -60,7 +60,7 @@ and Sum_form_cond2: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> 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 "\<nat>: U(O)" .. -qed - lemma - assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)" + assumes "\<Sum>x:A. B(x): U(i)" "<a,b>: \<Sum>x:A. B(x)" shows "a : A" -proof (rule Sum_form_conds) +proof +oops -abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)" +abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat>(\<lambda>n c. n) 0 n" schematic_goal "?a: (pred`0) =\<^sub>\<nat> 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 : \<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> 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 : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n" |