Unit and Null types. Methods.

1 files changed, 34 insertions, 16 deletions

diff --git a/scratch.thy b/scratch.thy
index 3f66083..ae1bdb5 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,10 +3,11 @@ theory scratch
 
 begin
 
-term "UN"
-
 (* Typechecking *)
-schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A"
+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
 
 
@@ -24,13 +25,13 @@ have "f`a`b`c \<equiv> d" by (simplify lems: asm)
 
 end
 
-lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
+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; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x"
+schematic_goal "\<lbrakk>a : A; b: A \<longrightarrow> X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x"
   by rsimplify
 
 lemma
@@ -38,7 +39,7 @@ lemma
   shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
   by (simplify lems: assms)
 
-lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk>
+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)
 
@@ -53,7 +54,6 @@ lemma
 assumes
   "a : A"
   "b : B a"
-  "B: A \<rightarrow> U"
   "\<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)
@@ -63,19 +63,20 @@ assumes
   "a : A"
   "b : B a"
   "c : C a b"
-  "B: A \<rightarrow> U"
-  "\<And>x. x : A\<Longrightarrow> C x: B x \<rightarrow> U"
   "\<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 *)
+
+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)
 
-(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *)
 
-schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
+(* 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_form)
-  apply assumption+
   apply (rule Equal_elim)
   back
   back
@@ -84,9 +85,26 @@ schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =
   back
   back
   back
-  back back back back back back
-
-thm comp
+  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