From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 18 Sep 2018 11:38:54 +0200 Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0! --- Coprod.thy | 1 + Empty.thy | 1 + Equal.thy | 1 + HoTT.thy | 9 +++-- HoTT_Base.thy | 29 ++++++++------- HoTT_Methods.thy | 25 ++++++++++++- Nat.thy | 1 + Prod.thy | 1 + Sum.thy | 1 + Unit.thy | 1 + ex/HoTT book/Ch1.thy | 47 +++++++++++------------ ex/Methods.thy | 73 ++++++++++++------------------------ ex/Synthesis.thy | 94 ++++++++++++++++++---------------------------- tests/Subgoal.thy | 63 ------------------------------- tests/Test.thy | 103 +++++++++++++++++++++++---------------------------- 15 files changed, 177 insertions(+), 273 deletions(-) delete mode 100644 tests/Subgoal.thy diff --git a/Coprod.thy b/Coprod.thy index d97228e..431e103 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -42,6 +42,7 @@ where \x. x: A \ c x: C (inl x); \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ (\x. c x) (\y. d y) (inr b) \ d b" +lemmas Coprod_form [form] lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr diff --git a/Empty.thy b/Empty.thy index 3060867..ee11045 100644 --- a/Empty.thy +++ b/Empty.thy @@ -20,6 +20,7 @@ where Empty_elim: "\a: \; C: \ \ U i\ \ ind\<^sub>\ a: C a" +lemmas Empty_form [form] lemmas Empty_routine [intro] = Empty_form Empty_elim diff --git a/Equal.thy b/Equal.thy index 7a31e37..19e3939 100644 --- a/Equal.thy +++ b/Equal.thy @@ -44,6 +44,7 @@ axiomatization where \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>= (\x. f x) (refl a) \ f a" +lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] diff --git a/HoTT.thy b/HoTT.thy index e2a7e35..0e7a674 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -1,5 +1,7 @@ -(* Title: HoTT/HoTT.thy - Author: Josh Chen +(* +Title: HoTT.thy +Author: Joshua Chen +Date: 2018 Homotopy type theory *) @@ -26,8 +28,7 @@ Proj begin -lemmas forms = - Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form +text \Rule bundles:\ lemmas intros = Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 7453883..2ad0ac5 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,7 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty *) theory HoTT_Base -imports Pure "HOL-Eisbach.Eisbach" +imports Pure begin @@ -18,17 +18,14 @@ typedecl t \ \Type of object types and terms\ typedecl ord \ \Type of meta-level numerals\ axiomatization - O :: ord and + O :: ord and Suc :: "ord \ ord" and - lt :: "[ord, ord] \ prop" (infix "<" 999) + lt :: "[ord, ord] \ prop" (infix "<" 999) and + leq :: "[ord, ord] \ prop" (infix "\" 999) where lt_Suc [intro]: "n < (Suc n)" and lt_trans [intro]: "\m1 < m2; m2 < m3\ \ m1 < m3" and - Suc_monotone [simp]: "m < n \ (Suc m) < (Suc n)" - -method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+) - -text \Method @{method proveSuc} proves statements of the form \n < (Suc (... (Suc n) ...))\.\ + leq_min [intro]: "O \ n" section \Judgment\ @@ -42,15 +39,15 @@ axiomatization U :: "ord \ t" where U_hierarchy: "i < j \ U i: U j" and - U_cumulative: "\A: U i; i < j\ \ A: U j" + U_cumulative: "\A: U i; i < j\ \ A: U j" and + U_cumulative': "\A: U i; i \ j\ \ A: U j" text \ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination. One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. -\ -method cumulativity = (elim U_cumulative, proveSuc) \ \Proves \A: U i \ A: U (Suc (... (Suc i) ...))\\ -method hierarchy = (rule U_hierarchy, proveSuc) \ \Proves \U i: U (Suc (... (Suc i) ...))\\ +@{thm U_cumulative'} is an alternative rule used by the method \lift\ in @{file HoTT_Methods.thy}. +\ section \Type families\ @@ -68,11 +65,15 @@ type_synonym tf = "t \ t" \ \Type of type families\< section \Named theorems\ named_theorems comp +named_theorems form text \ Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}. -@{attribute comp} declares computation rules. -These are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. + +@{attribute comp} declares computation rules, which are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. + +@{attribute form} declares type formation rules. +These are mainly used by the \cumulativity\ method, which lifts types into higher universes. \ (* Todo: Set up the Simplifier! *) diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 8929f69..f0cee6c 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -12,6 +12,26 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin +section \Handling universes\ + +method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+) + +method hierarchy = (rule U_hierarchy, provelt) + +method cumulativity declares form = ( + ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) | + ((elim U_cumulative | (rule U_cumulative, rule form)), provelt) +) + +text \ +Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form +\<^item> \n < (Suc (... (Suc n) ...))\, +\<^item> \U i: U (Suc (... (Suc i) ...))\, and +\<^item> @{prop "A: U i \ A: U j"}, where @{prop "i \ j"} +respectively. +\ + + section \Deriving typing judgments\ method routine uses add = (assumption | rule add | rule)+ @@ -38,14 +58,15 @@ Method @{method compute} performs single-step simplifications, using any rules d Premises of the rule(s) applied are added as new subgoals. \ + section \Derivation search\ text \ Combine @{method routine} and @{method compute} to search for derivations of judgments. -Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}. +Also handle universes using @{method hierarchy} and @{method cumulativity}. \ -method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+ +method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \Induction\ diff --git a/Nat.thy b/Nat.thy index 46b1af5..8a55852 100644 --- a/Nat.thy +++ b/Nat.thy @@ -41,6 +41,7 @@ where C: \ \ U i; \n c. \n: \; c: C n\ \ f n c: C (succ n) \ \ ind\<^sub>\ (\n c. f n c) a (succ n) \ f n (ind\<^sub>\ f a n)" +lemmas Nat_form [form] lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ diff --git a/Prod.thy b/Prod.thy index 4aa7119..f90ee9c 100644 --- a/Prod.thy +++ b/Prod.thy @@ -61,6 +61,7 @@ Note that this is a separate rule from function extensionality. Note that the bold lambda symbol \\<^bold>\\ used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation). \ +lemmas Prod_form [form] lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim lemmas Prod_comps [comp] = Prod_comp Prod_uniq diff --git a/Sum.thy b/Sum.thy index 422e01b..463a9d4 100644 --- a/Sum.thy +++ b/Sum.thy @@ -51,6 +51,7 @@ axiomatization where Sum_form_eq: "\A: U i; B: A \ U i; C: A \ U i; \x. x: A \ B x \ C x\ \ \x:A. B x \ \x:A. C x" +lemmas Sum_form [form] lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim lemmas Sum_comp [comp] diff --git a/Unit.thy b/Unit.thy index 61c6439..7c221f0 100644 --- a/Unit.thy +++ b/Unit.thy @@ -25,6 +25,7 @@ where Unit_comp: "\c: C \; C: \ \ U i\ \ ind\<^sub>\ c \ \ c" +lemmas Unit_form [form] lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim lemmas Unit_comp [comp] diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index a577fca..263f43d 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,55 +1,50 @@ -(* Title: HoTT/ex/HoTT book/Ch1.thy - Author: Josh Chen +(* +Title: ex/HoTT book/Ch1.thy +Author: Josh Chen +Date: 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) theory Ch1 - imports "../../HoTT" +imports "../../HoTT" + begin chapter \HoTT Book, Chapter 1\ -section \1.6 Dependent pair types (\-types)\ +section \1.6 Dependent pair types (\-types)\ -text "Propositional uniqueness principle:" +paragraph \Propositional uniqueness principle.\ schematic_goal - assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" - shows "?a: p =[\x:A. B(x)] " + assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" + shows "?a: p =[\x:A. B x] " -text "Proof by induction on \p: \x:A. B(x)\:" +text \Proof by induction on @{term "p: \x:A. B x"}:\ proof (rule Sum_elim[where ?p=p]) - text "We just need to prove the base case; the rest will be taken care of automatically." - - fix x y assume asm: "x: A" "y: B(x)" show - "refl(): =[\x:A. B(x)] , snd >" - proof (subst (0 1) comp) - text " - The computation rules for \fst\ and \snd\ require that \x\ and \y\ have appropriate types. - The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, - " - show "x: A" and "y: B(x)" by (fact asm)+ - - text "...twice, once each for the substitutions of \fst\ and \snd\." - show "x: A" and "y: B(x)" by (fact asm)+ + text \We prove the base case.\ + fix x y assume asm: "x: A" "y: B x" show "refl : =[\x:A. B x] , snd >" + proof compute + show "x: A" and "y: B x" by (fact asm)+ \ \Hint the correct types.\ + text \And now @{method derive} takes care of the rest. +\ qed (derive lems: assms asm) - qed (derive lems: assms) section \Exercises\ -text "Exercise 1.13" +paragraph \Exercise 1.13\ -abbreviation "not" ("\'(_')") where "\(A) \ A \ \" +abbreviation "not" ("\_") where "\A \ A \ \" text "This proof requires the use of universe cumulativity." -proposition assumes "A: U(i)" shows "\<^bold>\f. f`(inr(\<^bold>\a. f`inl(a))): \(\(A + \(A)))" -by (derive lems: assms U_cumulative[where ?A=\ and ?i=O and ?j=i]) +proposition assumes "A: U i" shows "\<^bold>\f. f`(inr(\<^bold>\a. f`(inl a))): \(\(A + \A))" +by (derive lems: assms) end diff --git a/ex/Methods.thy b/ex/Methods.thy index c78af14..09975b0 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,76 +1,49 @@ -(* Title: HoTT/ex/Methods.thy - Author: Josh Chen +(* +Title: ex/Methods.thy +Author: Joshua Chen +Date: 2018 -HoTT method usage examples +Basic HoTT method usage examples. *) theory Methods - imports "../HoTT" -begin +imports "../HoTT" +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)" -by (routine lems: assms) - - -lemma - assumes "\x:A. \y: B x. \z: C x y. D x y z: U(i)" - shows - "A : U(i)" and - "B: A \ U(i)" and - "\x. x : A \ C x: B x \ U(i)" and - "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" -proof - - show - "A : U(i)" and - "B: A \ U(i)" and - "\x. x : A \ C x: B x \ U(i)" and - "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" - by (derive lems: assms) -qed - - -text "Typechecking and constructing inhabitants:" + shows "\x:A. \y:B x. \z:C x y. \w:A. x =\<^sub>A w: U(i)" +by (routine add: assms) -\ \Correctly determines the type of the pair\ +\ \Correctly determines the type of the pair.\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ : ?A" by routine \ \Finds pair (too easy).\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ ?x : A \ B" -apply (rule Sum_intro) +apply (rule intros) 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 \ " +\ \Function application. We still often have to explicitly specify types.\ +lemma "\A: U i; a: A\ \ (\<^bold>\x. )`a \ " proof compute show "\x. x: A \ : A \ \" by routine -qed (routine lems: assms) - +qed -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 (routine lems: assms) +text \ +The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof. +\ - show "(\<^bold>\b. )`b \ " +lemma "\A: U i; B: A \ U i; a: A; b: B a\ \ (\<^bold>\x y. )`a`b \ " +proof (compute, routine) + show "\A: U i; B: A \ U i; a: A; b: B a\ \ (\<^bold>\y. )`b \ " proof compute - show "\b. b: B(a) \ : \x:A. B(x)" by (routine lems: assms) - qed fact -qed fact + show "\b. \A: U i; B: A \ U i; a: A; b: B a\ \ : \x:A. B x" by routine + qed +qed end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index a5e77ec..3ee973c 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,78 +1,58 @@ -(* Title: HoTT/ex/Synthesis.thy - Author: Josh Chen +(* +Title: ex/Synthesis.thy +Author: Joshua Chen +Date: 2018 -Examples of synthesis. +Examples of synthesis *) theory Synthesis - imports "../HoTT" +imports "../HoTT" + begin section \Synthesis of the predecessor function\ -text " - In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers. - - This is also done in \CTT.thy\; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely. -" +text \ +In this example we construct a predecessor function for the natural numbers. +This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional. +\ -text "First we show that the property we want is well-defined." +text \First we show that the property we want is well-defined.\ -lemma pred_welltyped: "\pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n): U(O)" +lemma pred_welltyped: "\pred: \\\. (pred`0 =\<^sub>\ 0) \ (\n:\. pred`(succ n) =\<^sub>\ n): U O" by routine -text " - Now we look for an inhabitant of this type. - Observe that we're looking for a lambda term \pred\ satisfying \(pred`0) =\<^sub>\ 0\ and \\n:\. (pred`(succ n)) =\<^sub>\ n\. - What if we require **definitional** equality instead of just propositional equality? -" +text \ +Now we look for an inhabitant of this type. +Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\ 0"} and @{term "\n:\. pred`(succ n) =\<^sub>\ n"}. +What if we require *definitional* instead of just propositional equality? +\ schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ n" apply compute prefer 4 apply compute -prefer 3 apply compute -apply (rule Nat_routine Nat_elim | compute | assumption)+ -done - -text " - The above proof finds a candidate, namely \\<^bold>\n. ind\<^sub>\ (\a b. a) 0 n\. - We prove this has the required type and properties. -" - -definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" - -lemma pred_type: "pred: \ \ \" unfolding pred_def by routine - -lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -proof (routine lems: pred_type) - have *: "pred`0 \ 0" unfolding pred_def - proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine - show "ind\<^sub>\ (\a b. a) 0 0 \ 0" - proof compute - show "\: U(O)" .. - qed routine - qed rule - then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) routine - - 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) 0 n)`succ(n)) =\<^sub>\ n" - proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine - show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) 0 (succ n) =\<^sub>\ n" - proof compute - show "\: U(O)" .. - qed routine - qed rule - qed rule -qed - -theorem - "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -by (routine lems: pred_welltyped pred_type pred_props) +apply (rule Nat_routine | compute)+ +oops +\ \Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\ + +text \ +The above proof finds a candidate, namely @{term "\n. ind\<^sub>\ (\a b. a) 0 n"}. +We prove this has the required type and properties. +\ + +definition pred :: t where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" + +lemma pred_type: "pred: \ \ \" +unfolding pred_def by routine + +lemma pred_props: "\n. refl n>: (pred`0 =\<^sub>\ 0) \ (\n:\. pred`(succ n) =\<^sub>\ n)" +unfolding pred_def by derive + +theorem "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +by (derive lems: pred_type pred_props) end diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy deleted file mode 100644 index 82d7e5d..0000000 --- a/tests/Subgoal.thy +++ /dev/null @@ -1,63 +0,0 @@ -theory Subgoal - imports "../HoTT" -begin - - -text " - Proof of \rpathcomp_type\ (see EqualProps.thy) in apply-style. - Subgoaling can be used to fix variables and apply the elimination rules. -" - -lemma rpathcomp_type: - 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 -apply standard - subgoal premises 1 for x \ \\subgoal\ is the proof script version of \fix-assume-show\.\ - apply standard - subgoal premises 2 for y - apply standard - subgoal premises 3 for p - apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) - \ \specifying \?A=A\ is crucial here to prevent the next \subgoal\ from binding a schematic ?A which should be instantiated to \A\.\ - prefer 4 - apply standard - apply (rule Prod_intro) - subgoal premises 4 for u z q - apply (rule Equal_elim[where ?x=u and ?y=z]) - apply (routine lems: assms 4) - done - apply (routine lems: assms 1 2 3) - done - apply (routine lems: assms 1 2) - done - apply fact - done -apply fact -done - - -text " - \subgoal\ converts schematic variables to fixed free variables, making it unsuitable for use in \schematic_goal\ proofs. - This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof. - - This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact. -" - -schematic_goal rpathcomp_synthesis: - assumes "A: U(i)" - shows "?a: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" - -text " - Try (and fail) to synthesize the constant for path composition, following the proof of \rpathcomp_type\ below. -" - -apply (rule intros) - apply (rule intros) - apply (rule intros) - subgoal 123 for x y p - apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) - oops - - -end diff --git a/tests/Test.thy b/tests/Test.thy index de65dbd..6f9f996 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -1,121 +1,110 @@ -(* Title: HoTT/tests/Test.thy - Author: Josh Chen - Date: Aug 2018 +(* +Title: tests/Test.thy +Author: Joshua Chen +Date: 2018 -This is an old "test suite" from early implementations of the theory. -It is not always guaranteed to be up to date, or reflect most recent versions of the theory. +This is an old test suite from early implementations. +It is not always guaranteed to be up to date or to reflect most recent versions of the theory. *) theory Test - imports "../HoTT" +imports "../HoTT" + begin -text " - A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. - - Things that *should* be automated: - - Checking that \A\ is a well-formed type, when writing things like \x : A\ and \A : U\. - - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? -" +text \ +A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. + +Things that *should* be automated: +\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}. +\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? +\ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] - \ \Turn on trace for unification and the simplifier, for debugging.\ +\ \Turn on trace for unification and the Simplifier, for debugging.\ section \\-type\ subsection \Typing functions\ -text " - Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following. -" +text \Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\ -proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" by (routine lems: assms) +proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" +by (routine add: assms) proposition assumes "A : U(i)" and "A \ B" shows "\<^bold>\x. x : B \ A" proof - have "A \ A \ B \ A" using assms by simp - moreover have "\<^bold>\x. x : A \ A" by (routine lems: assms) + moreover have "\<^bold>\x. x : A \ A" by (routine add: assms) ultimately show "\<^bold>\x. x : B \ A" by simp qed proposition assumes "A : U(i)" and "B : U(i)" shows "\<^bold>\x y. x : A \ B \ A" -by (routine lems: assms) - +by (routine add: assms) subsection \Function application\ -proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" by (derive lems: assms) - -text "Currying:" +proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" +by (derive lems: assms) lemma assumes "a : A" and "\x. x: A \ B(x): U(i)" shows "(\<^bold>\x y. y)`a \ \<^bold>\y. y" -proof compute - show "\x. x : A \ \<^bold>\y. y : B(x) \ B(x)" by (routine lems: assms) -qed fact +by (derive lems: assms) -lemma "\A: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" by derive +lemma "\A: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" +by derive -lemma "\A: U(i); a : A \ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" -proof compute - show "\x. \A: U(i); x: A\ \ \<^bold>\y. f x y: \y:B(x). C x y" - proof - oops +lemma "\A: U(i); a : A\ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" +proof derive +oops \ \Missing some premises.\ lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x. \<^bold>\y. \<^bold>\z. f x y z)`a`b`c \ f a b c" - oops +proof derive +oops subsection \Currying functions\ proposition curried_function_formation: - fixes A B C - assumes - "A : U(i)" and - "B: A \ U(i)" and - "\x. C(x): B(x) \ U(i)" + assumes "A : U(i)" and "B: A \ U(i)" and "\x. C(x): B(x) \ U(i)" shows "\x:A. \y:B(x). C x y : U(i)" - by (routine lems: assms) - +by (routine add: assms) proposition higher_order_currying_formation: assumes - "A: U(i)" and - "B: A \ U(i)" and + "A: U(i)" and "B: A \ U(i)" and "\x y. y: B(x) \ C(x)(y): U(i)" and "\x y z. z : C(x)(y) \ D(x)(y)(z): U(i)" shows "\x:A. \y:B(x). \z:C(x)(y). D(x)(y)(z): U(i)" - by (routine lems: assms) - +by (routine add: assms) lemma curried_type_judgment: - assumes "A: U(i)" "B: A \ U(i)" "\x y. \x : A; y : B(x)\ \ f x y : C x y" + assumes "A: U(i)" and "B: A \ U(i)" and "\x y. \x : A; y : B(x)\ \ f x y : C x y" shows "\<^bold>\x y. f x y : \x:A. \y:B(x). C x y" - by (routine lems: assms) +by (routine add: assms) -text " - Polymorphic identity function is now trivial due to lambda expression polymorphism. - (Was more involved in previous monomorphic incarnations.) -" +text \ +Polymorphic identity function is now trivial due to lambda expression polymorphism. +It was more involved in previous monomorphic incarnations. +\ -definition Id :: "Term" where "Id \ \<^bold>\x. x" - -lemma "\x: A\ \ Id`x \ x" -unfolding Id_def by (compute, routine) +lemma "x: A \ id`x \ x" +by derive section \Natural numbers\ -text "Automatic proof methods recognize natural numbers." +text \Automatic proof methods recognize natural numbers.\ + +proposition "succ(succ(succ 0)): \" by routine -proposition "succ(succ(succ 0)): Nat" by routine end -- cgit v1.2.3