diff options
Diffstat (limited to '')
-rw-r--r-- | scratch.thy | 192 |
1 files changed, 94 insertions, 98 deletions
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 |