Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Testing the new tactic everywhere
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 04 Dec 2009 09:08:51 +0100
changeset 513 eed5d55ea9a6
parent 512 8c7597b19f0e
child 514 6b3be083229c
Testing the new tactic everywhere
LFex.thy file | annotate | diff | comparison | revisions
LamEx.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/LFex.thy	Fri Dec 04 09:01:13 2009 +0100
+++ b/LFex.thy	Fri Dec 04 09:08:51 2009 +0100
@@ -298,10 +298,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
-apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
-apply(tactic {* clean_tac @{context} quot 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} quot 1 *})
 done
 
 print_quotients
--- a/LamEx.thy	Fri Dec 04 09:01:13 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 09:08:51 2009 +0100
@@ -308,32 +308,32 @@
 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s"
 sorry
 
-lemma real_alpha:
+lemma real_alpha_lift:
   "\<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} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [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 {* 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 (simp only: perm_prs)
 prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 prefer 3
 apply (tactic {* clean_tac @{context} [quot] 1 *})
 
@@ -344,8 +344,8 @@
 
 thm perm_lam_def
 apply (simp only: perm_prs)
-
-apply (tactic {* regularize_tac @{context} [quot] 1 *})
+(*apply (tactic {* regularize_tac @{context} [quot] 1 *})*)
+sorry
 
 done
 
--- a/QuotMain.thy	Fri Dec 04 09:01:13 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:08:51 2009 +0100
@@ -1287,7 +1287,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac' lthy quot rel_refl trans2,
                clean_tac lthy quot]]
     end) lthy
 *}
nominal2