diff options
Diffstat (limited to 'scratch.thy')
| -rw-r--r-- | scratch.thy | 50 |
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 |