From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 08:59:16 +0200 Subject: Go back to higher-order application notation --- Coprod.thy | 34 +++++++++++------------ Empty.thy | 4 +-- Equal.thy | 22 +++++++-------- EqualProps.thy | 85 +++++++++++++++++++++++++++++----------------------------- HoTT_Base.thy | 14 +++++----- Nat.thy | 28 +++++++++---------- Prod.thy | 22 +++++++-------- ProdProps.thy | 12 ++++----- Proj.thy | 28 +++++++++---------- Sum.thy | 24 ++++++++--------- Unit.thy | 4 +-- 11 files changed, 138 insertions(+), 139 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index 4607d1d..b87958a 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -17,40 +17,40 @@ axiomatization inr :: "Term \ Term" and indCoprod :: "[Term \ Term, Term \ Term, Term] \ Term" ("(1ind\<^sub>+)") where - Coprod_form: "\A: U(i); B: U(i)\ \ A + B: U(i)" + Coprod_form: "\A: U i; B: U i\ \ A + B: U i" and - Coprod_intro_inl: "\a: A; B: U(i)\ \ inl(a): A + B" + Coprod_intro_inl: "\a: A; B: U i\ \ inl a: A + B" and - Coprod_intro_inr: "\b: B; A: U(i)\ \ inr(b): A + B" + Coprod_intro_inr: "\b: B; A: U i\ \ inr b: A + B" and Coprod_elim: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); u: A + B - \ \ ind\<^sub>+(c)(d)(u) : C(u)" + \ \ ind\<^sub>+ c d u : C u" and Coprod_comp_inl: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); a: A - \ \ ind\<^sub>+(c)(d)(inl(a)) \ c(a)" + \ \ ind\<^sub>+ c d (inl a) \ c a" and Coprod_comp_inr: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); b: B - \ \ ind\<^sub>+(c)(d)(inr(b)) \ d(b)" + \ \ ind\<^sub>+ c d (inr b) \ d b" text "Admissible formation inference rules:" axiomatization where - Coprod_wellform1: "A + B: U(i) \ A: U(i)" + Coprod_wellform1: "A + B: U i \ A: U i" and - Coprod_wellform2: "A + B: U(i) \ B: U(i)" + Coprod_wellform2: "A + B: U i \ B: U i" text "Rule attribute declarations:" diff --git a/Empty.thy b/Empty.thy index 8f5cc8c..a42f7ff 100644 --- a/Empty.thy +++ b/Empty.thy @@ -17,9 +17,9 @@ axiomatization Empty :: Term ("\") and indEmpty :: "Term \ Term" ("(1ind\<^sub>\)") where - Empty_form: "\: U(O)" + Empty_form: "\: U O" and - Empty_elim: "\C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" + Empty_elim: "\C: \ \ U i; z: \\ \ ind\<^sub>\ z: C z" text "Rule attribute declarations:" diff --git a/Equal.thy b/Equal.thy index 772072a..7254104 100644 --- a/Equal.thy +++ b/Equal.thy @@ -27,33 +27,33 @@ translations section \Type rules\ axiomatization where - Equal_form: "\A: U(i); a: A; b: A\ \ a =\<^sub>A b : U(i)" + Equal_form: "\A: U i; a: A; b: A\ \ a =\<^sub>A b : U i" and - Equal_intro: "a : A \ refl(a): a =\<^sub>A a" + Equal_intro: "a : A \ (refl a): a =\<^sub>A a" and Equal_elim: "\ x: A; y: A; p: x =\<^sub>A y; - \x. x: A \ f(x) : C(x)(x)(refl x); - \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) - \ \ ind\<^sub>=(f)(p) : C(x)(y)(p)" + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i + \ \ ind\<^sub>= f p : C x y p" and Equal_comp: "\ a: A; - \x. x: A \ f(x) : C(x)(x)(refl x); - \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) - \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i + \ \ ind\<^sub>= f (refl a) \ f a" text "Admissible inference rules for equality type formation:" axiomatization where - Equal_wellform1: "a =\<^sub>A b: U(i) \ A: U(i)" + Equal_wellform1: "a =\<^sub>A b: U i \ A: U i" and - Equal_wellform2: "a =\<^sub>A b: U(i) \ a: A" + Equal_wellform2: "a =\<^sub>A b: U i \ a: A" and - Equal_wellform3: "a =\<^sub>A b: U(i) \ b: A" + Equal_wellform3: "a =\<^sub>A b: U i \ b: A" text "Rule attribute declarations:" diff --git a/EqualProps.thy b/EqualProps.thy index c114d37..708eb33 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -14,7 +14,7 @@ begin section \Symmetry / Path inverse\ -definition inv :: "Term \ Term" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. refl(x)) p" +definition inv :: "Term \ Term" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. (refl x)) p" text " In the proof below we begin by using path induction on \p\ with the application of \rule Equal_elim\, telling Isabelle the specific substitutions to use. @@ -22,7 +22,7 @@ text " " lemma inv_type: - assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "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 by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ @@ -33,7 +33,7 @@ text " " lemma inv_comp: - assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" + assumes "A : U i " and "a : A" shows "(refl a)\ \ refl a" unfolding inv_def proof compute show "\x. x: A \ refl x: x =\<^sub>A x" .. @@ -46,14 +46,14 @@ 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\. " -definition rpathcomp :: Term where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\x. refl(x)) q) p" +definition rpathcomp :: Term where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\x. (refl x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: " lemma rpathcomp_type: - assumes "A: U(i)" + assumes "A: U i" shows "rpathcomp: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" unfolding rpathcomp_def proof @@ -81,7 +81,7 @@ proof qed fact corollary - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" by (routine lems: assms rpathcomp_type) @@ -90,11 +90,11 @@ text " " lemma rpathcomp_comp: - assumes "A: U(i)" and "a: A" - shows "rpathcomp`a`a`refl(a)`a`refl(a) \ refl(a)" + assumes "A: U i" and "a: A" + shows "rpathcomp`a`a`(refl a)`a`(refl a) \ refl a" unfolding rpathcomp_def proof compute - { fix x assume 1: "x: A" + 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 fix y assume 2: "y: A" @@ -114,11 +114,11 @@ proof compute qed (rule assms) qed (routine lems: assms 1 2 3) qed (routine lems: assms 1 2) - qed (rule assms) } + 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)" + next show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \ refl a" proof compute - { fix y assume 1: "y: A" + 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 fix p assume 2: "p: a =\<^sub>A y" @@ -135,11 +135,11 @@ proof compute qed (routine lems: assms 3 4) qed fact qed (routine lems: assms 1 2) - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" + next show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \ refl a" proof compute - { fix p assume 1: "p: a =\<^sub>A a" + fix p assume 1: "p: a =\<^sub>A a" show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. a =\<^sub>A z \ a =\<^sub>A z" proof (rule Equal_elim[where ?x=a and ?y=a]) fix u assume 2: "u: A" @@ -152,11 +152,11 @@ proof compute by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) qed (routine lems: assms 2 3) qed fact - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" + next show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \ refl a" proof compute - { fix u assume 1: "u: A" + fix u assume 1: "u: A" show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" proof fix z assume 2: "z: A" @@ -165,22 +165,22 @@ proof compute show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) qed (routine lems: assms 1 2) - qed fact } + qed fact - show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" + next show "(\<^bold>\z q. ind\<^sub>= refl q)`a`(refl a) \ refl a" proof compute - { fix a assume 1: "a: A" + fix a assume 1: "a: A" show "\<^bold>\q. ind\<^sub>= refl q: a =\<^sub>A a \ a =\<^sub>A a" proof show "\q. q: a =\<^sub>A a \ ind\<^sub>= refl q: a =\<^sub>A a" by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(\<^bold>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" + next show "(\<^bold>\q. ind\<^sub>= refl q)`(refl a) \ refl a" 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]) (routine lems: assms) - show "ind\<^sub>= refl (refl(a)) \ refl(a)" + show "ind\<^sub>= refl (refl a) \ refl a" proof compute show "\x. x: A \ refl(x): x =\<^sub>A x" .. qed (routine lems: assms) @@ -196,23 +196,23 @@ text "The raw object lambda term is cumbersome to use, so we define a simpler co axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\" 120) where pathcomp_def: "\ - A: U(i); + A: U i; x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z \ \ p \ q \ rpathcomp`x`y`p`z`q" lemma pathcomp_type: - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "p \ q: x =\<^sub>A z" proof (subst pathcomp_def) - show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ + show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ qed (routine lems: assms rpathcomp_type) lemma pathcomp_comp: - assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" + assumes "A : U i" and "a : A" shows "(refl a) \ (refl a) \ refl a" by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) @@ -223,44 +223,45 @@ lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp section \Higher groupoid structure of types\ lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows - "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] p \ refl(y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] refl(x) \ p" + "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] p \ (refl y)" and + "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \ p" proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] p \ refl(y)" + show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] p \ (refl y)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] refl x \ p" + show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] (refl x) \ p" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ qed lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows - "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] refl(y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] refl(x)" + "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] (refl y)" and + "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] (refl x)" proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] refl(y)" + show "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] (refl y)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - show "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] refl(x)" + show "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] (refl x)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ qed lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows "ind\<^sub>= (\u. refl (refl u)) p: p\\ =[x =\<^sub>A y] p" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms) +text "Next we construct a proof term of associativity of path composition." schematic_goal assumes - "A: U(i)" + "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" shows @@ -268,8 +269,8 @@ schematic_goal apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) apply (rule assms)+ -apply (subst pathcomp_comp) - +\ \Continue by substituting \refl x \ q = q\ etc.\ +sorry end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 4e1a9be..a5b88fd 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -16,8 +16,6 @@ text "Meta syntactic type for object-logic types and terms." typedecl Term -section \Judgments\ - text " Formalize the typing judgment \a: A\. For judgmental/definitional equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it. @@ -38,13 +36,13 @@ axiomatization lt :: "[Ord, Ord] \ prop" (infix "<" 999) and leq :: "[Ord, Ord] \ prop" (infix "\" 999) where - Ord_lt_min: "\n. O < S(n)" + Ord_lt_min: "\n. O < S n" and - Ord_lt_monotone: "\m n. m < n \ S(m) < S(n)" + Ord_lt_monotone: "\m n. m < n \ S m < S n" and Ord_leq_min: "\n. O \ n" and - Ord_leq_monotone: "\m n. m \ n \ S(m) \ S(n)" + Ord_leq_monotone: "\m n. m \ n \ S m \ S n" lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone \ \Enables \standard\ to automatically solve inequalities.\ @@ -54,9 +52,9 @@ text "Define the universe types." axiomatization U :: "Ord \ Term" where - U_hierarchy: "\i j. i < j \ U(i): U(j)" + U_hierarchy: "\i j. i < j \ U i: U j" and - U_cumulative: "\A i j. \A: U(i); i \ j\ \ A: U(j)" + U_cumulative: "\A i j. \A: U i; i \ j\ \ A: U j" text " The rule \U_cumulative\ is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! @@ -71,7 +69,7 @@ text " " abbreviation (input) constrained :: "[Term \ Term, Term, Term] \ prop" ("(1_: _ \ _)") - where "f: A \ B \ (\x. x : A \ f(x): B)" + where "f: A \ B \ (\x. x : A \ f x: B)" text " The above is used to define type families, which are constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are small types. diff --git a/Nat.thy b/Nat.thy index 45c3a2e..e879c92 100644 --- a/Nat.thy +++ b/Nat.thy @@ -17,31 +17,31 @@ axiomatization succ :: "Term \ Term" and indNat :: "[[Term, Term] \ Term, Term, Term] \ Term" ("(1ind\<^sub>\)") where - Nat_form: "\: U(O)" + Nat_form: "\: U O" and Nat_intro_0: "0: \" and - Nat_intro_succ: "n: \ \ succ(n): \" + Nat_intro_succ: "n: \ \ succ n: \" and Nat_elim: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0); + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n); + a: C 0; n: \ - \ \ ind\<^sub>\(f)(a)(n): C(n)" + \ \ ind\<^sub>\ f a n: C n" and Nat_comp_0: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0) - \ \ ind\<^sub>\(f)(a)(0) \ a" + C: \ \ U i; + \n c. \n: \; c: C(n)\ \ f n c: C (succ n); + a: C 0 + \ \ ind\<^sub>\ f a 0 \ a" and Nat_comp_succ: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0); + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n); + a: C 0; n: \ - \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ f a n)" + \ \ ind\<^sub>\ f a (succ n) \ f n (ind\<^sub>\ f a n)" text "Rule attribute declarations:" diff --git a/Prod.thy b/Prod.thy index b0408b9..35d6b07 100644 --- a/Prod.thy +++ b/Prod.thy @@ -36,17 +36,17 @@ abbreviation Function :: "[Term, Term] \ Term" (infixr "\Type rules\ axiomatization where - Prod_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Prod_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and - Prod_intro: "\\x. x: A \ b(x): B(x); A: U(i)\ \ \<^bold>\x. b(x): \x:A. B(x)" + Prod_intro: "\\x. x: A \ b x: B x; A: U i\ \ \<^bold>\x. b x: \x:A. B x" and - Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" + Prod_elim: "\f: \x:A. B x; a: A\ \ f`a: B a" and - Prod_appl: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_appl: "\\x. x: A \ b x: B x; a: A\ \ (\<^bold>\x. b x)`a \ b a" and - Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" + Prod_uniq: "f : \x:A. B x \ \<^bold>\x. (f`x) \ f" and - Prod_eq: "\\x. x: A \ b(x) \ b'(x); A: U(i)\ \ \<^bold>\x. b(x) \ \<^bold>\x. b'(x)" + Prod_eq: "\\x. x: A \ b x \ c x; A: U i\ \ \<^bold>\x. b x \ \<^bold>\x. c x" text " The Pure rules for \\\ only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. @@ -55,15 +55,15 @@ text " " text " - 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)\. + 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. " axiomatization where - Prod_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" + Prod_wellform1: "(\x:A. B x: U i) \ A: U i" and - Prod_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Prod_wellform2: "(\x:A. B x: U i) \ B: A \ U i" text "Rule attribute declarations---set up various methods to use the type rules." @@ -75,9 +75,9 @@ lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \Function composition\ -definition compose :: "[Term, Term] \ Term" (infixr "o" 70) where "g o f \ \<^bold>\x. g`(f`x)" +definition compose :: "[Term, Term] \ Term" (infixr "o" 110) where "g o f \ \<^bold>\x. g`(f`x)" -syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 70) +syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 110) translations "g \ f" \ "g o f" diff --git a/ProdProps.thy b/ProdProps.thy index 1af6ad3..14556af 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -18,7 +18,7 @@ text " " lemma compose_assoc: - assumes "A: U(i)" and "f: A \ B" "g: B \ C" "h: \x:C. D(x)" + assumes "A: U i" and "f: A \ B" "g: B \ C" "h: \x:C. D x" shows "(h \ g) \ f \ h \ (g \ f)" proof (subst (0 1 2 3) compose_def) show "\<^bold>\x. (\<^bold>\y. h`(g`y))`(f`x) \ \<^bold>\x. h`((\<^bold>\y. g`(f`y))`x)" @@ -31,19 +31,19 @@ proof (subst (0 1 2 3) compose_def) proof compute show "\x. x: A \ g`(f`x): C" by (routine lems: assms) qed - show "\x. x: B \ h`(g`x): D(g`x)" by (routine lems: assms) + show "\x. x: B \ h`(g`x): D (g`x)" by (routine lems: assms) qed (routine lems: assms) qed fact qed lemma compose_comp: - assumes "A: U(i)" and "\x. x: A \ b(x): B" and "\x. x: B \ c(x): C(x)" - shows "(\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" + assumes "A: U i" and "\x. x: A \ b x: B" and "\x. x: B \ c x: C x" + shows "(\<^bold>\x. c x) \ (\<^bold>\x. b x) \ \<^bold>\x. c (b x)" proof (subst compose_def, subst Prod_eq) - show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c (b x))`a" + show "\a. a: A \ (\<^bold>\x. c x)`((\<^bold>\x. b x)`a) \ (\<^bold>\x. c (b x))`a" proof compute - show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c(b(x)))`a" + show "\a. a: A \ c ((\<^bold>\x. b x)`a) \ (\<^bold>\x. c (b x))`a" by (derive lems: assms) qed (routine lems: assms) qed (derive lems: assms) diff --git a/Proj.thy b/Proj.thy index a1c4c8f..74c561c 100644 --- a/Proj.thy +++ b/Proj.thy @@ -12,44 +12,44 @@ theory Proj begin -definition fst :: "Term \ Term" where "fst(p) \ ind\<^sub>\ (\x y. x) p" -definition snd :: "Term \ Term" where "snd(p) \ ind\<^sub>\ (\x y. y) p" +definition fst :: "Term \ Term" where "fst p \ ind\<^sub>\ (\x y. x) p" +definition snd :: "Term \ Term" where "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" + assumes "\x:A. B x: U i" and "p: \x:A. B x" shows "fst p: A" unfolding fst_def by (derive lems: assms) lemma fst_comp: - assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ a" + assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "fst \ a" unfolding fst_def proof compute - show "a: A" and "b: B(a)" by fact+ + show "a: A" and "b: B a" by fact+ qed (routine lems: assms)+ lemma snd_type: - assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" + 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)" by (derive lems: assms fst_type) + show "\p. p: \x:A. B x \ B (fst p): U i" by (derive lems: assms fst_type) fix x y - assume asm: "x: A" "y: B(x)" - show "y: B(fst )" + assume asm: "x: A" "y: B x" + show "y: B (fst )" proof (subst fst_comp) - show "A: U(i)" by (wellformed lems: assms(1)) - show "\x. x: A \ B(x): U(i)" by (wellformed lems: assms(1)) + show "A: U i" by (wellformed lems: assms(1)) + show "\x. x: A \ B x: U i" by (wellformed lems: assms(1)) qed fact+ qed fact lemma snd_comp: - assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ b" + assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "snd \ b" unfolding snd_def proof compute - show "\x y. y: B(x) \ y: B(x)" . + show "\x y. y: B x \ y: B x" . show "a: A" by fact - show "b: B(a)" by fact + show "b: B a" by fact qed (routine lems: assms) diff --git a/Sum.thy b/Sum.thy index 8d0b0e6..6de20fd 100644 --- a/Sum.thy +++ b/Sum.thy @@ -33,30 +33,30 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) section \Type rules\ axiomatization where - Sum_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Sum_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and - Sum_intro: "\B: A \ U(i); a: A; b: B(a)\ \ : \x:A. B(x)" + Sum_intro: "\B: A \ U i; a: A; b: B a\ \ : \x:A. B x" and Sum_elim: "\ - p: \x:A. B(x); - \x y. \x: A; y: B(x)\ \ f(x)(y): C(); - C: \x:A. B(x) \ U(i) - \ \ ind\<^sub>\(f)(p): C(p)" (* What does writing \x y. f(x, y) change? *) + p: \x:A. B x; + \x y. \x: A; y: B x\ \ f x y: C ; + C: \x:A. B x \ U i + \ \ ind\<^sub>\ f p: C p" (* What does writing \x y. f(x, y) change? *) and Sum_comp: "\ a: A; - b: B(a); - \x y. \x: A; y: B(x)\ \ f(x)(y): C(); + b: B a; + \x y. \x: A; y: B(x)\ \ f x y: C ; B: A \ U(i); - C: \x:A. B(x) \ U(i) - \ \ ind\<^sub>\(f)() \ f(a)(b)" + C: \x:A. B x \ U i + \ \ ind\<^sub>\ f \ f a b" text "Admissible inference rules for sum formation:" axiomatization where - Sum_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" + Sum_wellform1: "(\x:A. B x: U i) \ A: U i" and - Sum_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Sum_wellform2: "(\x:A. B x: U i) \ B: A \ U i" text "Rule attribute declarations:" diff --git a/Unit.thy b/Unit.thy index 6adfb02..9b86739 100644 --- a/Unit.thy +++ b/Unit.thy @@ -20,9 +20,9 @@ where and Unit_intro: "\: \" and - Unit_elim: "\C: \ \ U(i); c: C(\); a: \\ \ ind\<^sub>\(c)(a) : C(a)" + Unit_elim: "\C: \ \ U i; c: C \; a: \\ \ ind\<^sub>\ c a: C a" and - Unit_comp: "\C: \ \ U(i); c: C(\)\ \ ind\<^sub>\(c)(\) \ c" + Unit_comp: "\C: \ \ U i; c: C \\ \ ind\<^sub>\ c \ \ c" text "Rule attribute declarations:" -- cgit v1.2.3