aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT.thy4
-rw-r--r--HoTT_Base.thy21
-rw-r--r--Nat.thy49
-rw-r--r--Prod.thy34
-rw-r--r--Proj.thy28
-rw-r--r--Sum.thy16
-rw-r--r--scratch.thy192
7 files changed, 206 insertions, 138 deletions
diff --git a/HoTT.thy b/HoTT.thy
index fa50f61..ce77ec7 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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.
diff --git a/Nat.thy b/Nat.thy
new file mode 100644
index 0000000..93b7a2e
--- /dev/null
+++ b/Nat.thy
@@ -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
diff --git a/Prod.thy b/Prod.thy
index 8fa73f3..e4e7091 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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
diff --git a/Proj.thy b/Proj.thy
index bcef939..e6ed0bb 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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)
diff --git a/Sum.thy b/Sum.thy
index 80f8a9c..18d4186 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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