Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LamEx.thy
changeset 514 6b3be083229c
parent 513 eed5d55ea9a6
parent 510 8dbc521ee97f
child 515 b00a9b58264d 
--- a/LamEx.thy	Fri Dec 04 09:08:51 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -128,7 +128,7 @@
 unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp[quot_rsp]:
+lemma perm_rsp[quotient_rsp]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp[quot_rsp]:
+lemma rVar_rsp[quotient_rsp]:
   "(op = ===> alpha) rVar rVar"
 by (auto intro:a1)
 
-lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 by (auto intro:a2)
 
-lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -174,7 +174,7 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -312,39 +312,32 @@
   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
 prefer 2
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 apply (simp only: perm_prs)
 prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 prefer 3
-apply (tactic {* clean_tac @{context} [quot] 1 *})
-
-thm all_prs
-thm REP_ABS_RSP
-thm ball_reg_eqv_range
-
-
-thm perm_lam_def
+apply (tactic {* clean_tac @{context} 1 *})
 apply (simp only: perm_prs)
-(*apply (tactic {* regularize_tac @{context} [quot] 1 *})*)
+(*apply (tactic {* regularize_tac @{context} 1 *})*)
 sorry
 
 done
nominal2