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.
Initial proof modifications for alpha_res
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sat, 27 Mar 2010 08:17:43 +0100
changeset 1672 94b8b70f7bc0
parent 1671 6a114f8d45e6
child 1673 e8cf0520c820
Initial proof modifications for alpha_res
Nominal/Fv.thy file | annotate | diff | comparison | revisions
Nominal/Rsp.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Fv.thy	Sat Mar 27 08:11:45 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:17:43 2010 +0100
@@ -653,7 +653,7 @@
   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
 
@@ -898,7 +898,7 @@
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
--- a/Nominal/Rsp.thy	Sat Mar 27 08:11:45 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 08:17:43 2010 +0100
@@ -63,7 +63,7 @@
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
 *}
 
@@ -111,7 +111,7 @@
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
@@ -261,7 +261,7 @@
 ML {*
 fun fvbv_rsp_tac' simps ctxt =
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
nominal2