diff options
| -rw-r--r-- | HoTT.thy | 4 | ||||
| -rw-r--r-- | HoTT_Base.thy | 21 | ||||
| -rw-r--r-- | Nat.thy | 49 | ||||
| -rw-r--r-- | Prod.thy | 34 | ||||
| -rw-r--r-- | Proj.thy | 28 | ||||
| -rw-r--r-- | Sum.thy | 16 | ||||
| -rw-r--r-- | scratch.thy | 192 |
7 files changed, 206 insertions, 138 deletions
@@ -12,9 +12,11 @@ HoTT_Base HoTT_Methods (* Types *) -Equal Prod Sum +Equal +Coprod +Nat (* Additional properties *) EqualProps diff --git a/HoTT_Base.thy b/HoTT_Base.thy index cf71813..c2bb092 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -9,6 +9,10 @@ theory HoTT_Base imports Pure begin +text "Use the syntax \<open>f(x)\<close> instead of \<open>f x\<close> for function application." + +setup Pure_Thy.old_appl_syntax_setup + section \<open>Foundational definitions\<close> @@ -20,12 +24,12 @@ typedecl Term section \<open>Judgments\<close> text " - Formalize the typing judgment \<open>a : A\<close>. + Formalize the typing judgment \<open>a: A\<close>. For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. " consts - has_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) + has_type :: "[Term, Term] \<Rightarrow> prop" ("(1_: _)" [0, 0] 1000) section \<open>Universe hierarchy\<close> @@ -39,11 +43,11 @@ axiomatization S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<-" 999) where - Ord_lt_min: "\<And>n. O <- S n" + Ord_min: "\<And>n. O <- S(n)" and - Ord_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" + Ord_monotone: "\<And>m n. m <- n \<Longrightarrow> S(m) <- S(n)" -lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans +lemmas Ord_rules [intro] = Ord_min Ord_monotone \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> text "Define the universe types." @@ -51,12 +55,11 @@ text "Define the universe types." axiomatization U :: "Ord \<Rightarrow> Term" where - U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" + U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i): U(j)" and - U_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" + U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)" \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> - section \<open>Type families\<close> text " @@ -64,7 +67,7 @@ text " " abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("(1_: _ \<longrightarrow> _)") - where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x : B)" + where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f(x): B)" text " The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types. @@ -0,0 +1,49 @@ +(* Title: HoTT/Nat.thy + Author: Josh Chen + Date: Aug 2018 + +Natural numbers. +*) + +theory Nat + imports HoTT_Base +begin + + +axiomatization + Nat :: Term ("\<nat>") and + zero :: Term ("0") and + succ :: "Term \<Rightarrow> Term" and + indNat :: "[Typefam, [Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)") +where + Nat_form: "\<nat> : U(O)" +and + Nat_intro1: "0 : \<nat>" +and + Nat_intro2: "\<And>n. n : \<nat> \<Longrightarrow> succ n : \<nat>" +and + Nat_elim: "\<And>i C f a n. \<lbrakk> + C: \<nat> \<longrightarrow> U(i); + \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n); + a : C 0; + n : \<nat> + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a n : C n" +and + Nat_comp1: "\<And>i C f a. \<lbrakk> + C: \<nat> \<longrightarrow> U(i); + \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n); + a : C 0 + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a 0 \<equiv> a" +and + Nat_comp2: "\<And> i C f a n. \<lbrakk> + C: \<nat> \<longrightarrow> U(i); + \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n); + a : C 0; + n : \<nat> + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a (succ n) \<equiv> f n (ind\<^sub>\<nat> C f a n)" + +lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2 +lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 + + +end
\ No newline at end of file @@ -15,7 +15,7 @@ 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" (infixl "`" 60) + appl :: "[Term, Term] \<Rightarrow> Term" ("(1_`_)" [61, 60] 60) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax @@ -27,48 +27,48 @@ syntax 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)" + "\<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." abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) - where "A \<rightarrow> B \<equiv> \<Prod>_:A. B" + where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" section \<open>Type rules\<close> axiomatization where - Prod_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U(i)" + Prod_form: "\<And>i A B. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)" and - Prod_intro: "\<And>i A B b. \<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: "\<And>i A B b. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x): \<Prod>x:A. B(x)" and - Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" + Prod_elim: "\<And>A B f a. \<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)" and - Prod_comp: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" + Prod_comp: "\<And>i A B b a. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and - Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (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 (*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>. That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. " axiomatization where - Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> A : U(i)" + Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" and - Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" + Prod_form_cond2: "\<And>i A B. (\<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 [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +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_comps [comp] = Prod_comp Prod_uniq @@ -84,9 +84,9 @@ where and Unit_intro: "\<star> : \<one>" and - Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>; a : \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c a : C a" + Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C(\<star>); a : \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(C, c, a) : C(a)" and - Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c \<star> \<equiv> c" + Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(C, c, \<star>) \<equiv> c" lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp @@ -52,6 +52,7 @@ unfolding fst_dep_def proof show "lambda (Sum A B) (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x)) : (\<Sum>x:A. B x) \<rightarrow> A" proof + show "A : U(i)" using assms(1) .. show "Sum A B : U(i)" by (rule assms) show "\<And>p. p : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A" proof @@ -66,11 +67,11 @@ lemma fst_dep_comp: shows "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def proof (subst comp) + show "Sum A B : U(i)" using assms(1-2) .. show "\<And>x. x : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) x : A" by (standard, rule assms(1), assumption+) - show "(a,b) : Sum A B" using assms(2-4) .. - show "ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a, b) \<equiv> a" - proof - oops + show "(a,b) : Sum A B" using assms .. + show "ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a, b) \<equiv> a" by (standard, (rule assms|assumption)+) +qed (rule assms) \<comment> \<open> (* Old proof *) proof - @@ -101,8 +102,23 @@ qed lemma snd_dep_type: assumes "\<Sum>x:A. B x : U(i)" and "p : \<Sum>x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" - unfolding fst_dep_def snd_dep_def - by (simplify lems: assms) +unfolding fst_dep_def snd_dep_def +proof (subst (3) comp) + show "Sum A B : U(i)" by (rule assms) + show "\<And>x. x : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) x : A" + proof + show "A : U(i)" using assms(1) .. + qed + show "A : U(i)" using assms(1) .. + show "p : Sum A B" by (rule assms(2)) + show "lambda + (Sum A B) + (ind\<^sub>\<Sum>[A, B] (\<lambda>q. B (lambda (Sum A B) (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x))`q)) (\<lambda>x y. y)) + ` p : B (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) p)" + proof (subst (2) comp) + show "Sum A B : U(i)" by (rule assms) + show " + \<comment> \<open> (* Old proof *) proof (derive lems: assms unfolds: snd_dep_def) @@ -36,7 +36,7 @@ section \<open>Type rules\<close> axiomatization where Sum_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U(i)" and - Sum_intro: "\<And>i A B a b. \<lbrakk>B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" + Sum_intro: "\<And>i A B a b. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" and Sum_elim: "\<And>i A B C f p. \<lbrakk> C: \<Sum>x:A. B x \<longrightarrow> U(i); @@ -45,6 +45,8 @@ and \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f p : C p" and Sum_comp: "\<And>i A B C f a b. \<lbrakk> + A : U(i); + B: A \<longrightarrow> U(i); C: \<Sum>x:A. B x \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); a : A; @@ -63,17 +65,17 @@ lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp -section \<open>Null type\<close> +section \<open>Empty type\<close> axiomatization - Null :: Term ("\<zero>") and - indNull :: "[Typefam, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") + Empty :: Term ("\<zero>") and + indEmpty :: "[Typefam, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") where - Null_form: "\<zero> : U(O)" + Empty_form: "\<zero> : U(O)" and - Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z" + Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z" -lemmas Null_rules [intro] = Null_form Null_elim +lemmas Empty_rules [intro] = Empty_form Empty_elim end
\ No newline at end of file diff --git a/scratch.thy b/scratch.thy index ae1bdb5..b88a8fc 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,108 +3,104 @@ theory scratch begin -(* Typechecking *) -schematic_goal "\<lbrakk>A : U(i); B : U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" - by derive - -lemma "\<zero> : U(S S S 0)" - by derive - - -(* Simplification *) - -notepad begin - -assume asm: - "f`a \<equiv> g" - "g`b \<equiv> \<^bold>\<lambda>x:A. d" - "c : A" - "d : B" - -have "f`a`b`c \<equiv> d" by (simplify lems: asm) - -end - -lemma "\<lbrakk>A : U(i); a : A\<rbrakk> \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" - by simplify - -lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" - by simplify - -schematic_goal "\<lbrakk>a : A; b: A \<longrightarrow> X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x" - by rsimplify - -lemma - assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x" - shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" - by (simplify lems: assms) - -lemma "\<lbrakk>a : A; b : B a; B: A \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk> - \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" - by (simplify) - -lemma - assumes - "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y" - "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b" - shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" -by (simplify lems: assms) - -lemma -assumes - "a : A" - "b : B a" - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y" -shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" -by (simplify lems: assms) - -lemma -assumes - "a : A" - "b : B a" - "c : C a b" - "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z" -shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> d a b c" -by (simplify lems: assms) - -(* Polymorphic identity function *) +abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<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_form) +apply assumption +apply (rule Nat_intro1) +apply (rule Equal_intro) +apply (rule Nat_intro1) +prefer 2 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_form) +apply assumption +apply (rule Nat_intro1) +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 assumption +apply (rule Nat_form) +done + +schematic_goal "?a : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n" +apply (rule Sum_intro) +apply (rule Prod_form) +apply (rule Nat_form)+ +apply (rule Prod_form) +apply (rule Nat_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +apply assumption +apply (elim Nat_intro2) +apply assumption +prefer 2 apply (rule Prod_intro) +apply (rule Nat_form) +prefer 3 apply (rule Prod_intro) +apply (rule Nat_form)+ +prefer 3 apply (rule Nat_elim) +back +oops -definition Id :: "Numeral \<Rightarrow> Term" where "Id n \<equiv> \<^bold>\<lambda>A:U(n). \<^bold>\<lambda>x:A. x" -lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \<equiv> x" unfolding Id_def by (simplify lems: assms) +(* Now try to derive pred directly *) +schematic_goal "?a : \<Sum>pred:?A . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" +(* At some point need to perform induction *) +apply (rule Sum_intro) +defer +apply (rule Sum_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +defer +apply (rule Nat_intro1)+ +prefer 5 apply assumption +prefer 4 apply (rule Prod_form) +apply (rule Nat_form)+ +apply (rule Prod_form) +apply (rule Nat_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +apply assumption +apply (rule Nat_intro2) +apply assumption+ +(* Now begins the hard part *) +prefer 2 apply (rule Sum_rules) +prefer 2 apply (rule Prod_rules) -(* See if we can find path inverse *) -schematic_goal "\<lbrakk>A : U(i); x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x" - apply (rule Prod_intro) - apply (rule Equal_elim) - back - back - back - back - back - back - back - defer - back - back - back - back - back - back - back - back - back - apply (rule Equal_form) - apply assumption+ - defer - defer - apply assumption - defer - defer - apply (rule Equal_intro) - apply assumption+ -oops end
\ No newline at end of file |