Mercurial Mercurial > hg > nominal2 / comparison
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.
Nominal/Fv.thy
changeset 1672 94b8b70f7bc0
parent 1670 ed89a26b7074
child 1673 e8cf0520c820
equal deleted inserted replaced
1671:6a114f8d45e6 1672:94b8b70f7bc0 
   651 fun reflp_tac induct eq_iff =
 
   651 fun reflp_tac induct eq_iff =
 
   652   rtac induct THEN_ALL_NEW
 
   652   rtac induct THEN_ALL_NEW
 
   653   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
 
   653   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
 
   654   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   654   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   655   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   655   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   656      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   656      @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   657        add_0_left supp_zero_perm Int_empty_left split_conv})
 
   657        add_0_left supp_zero_perm Int_empty_left split_conv})
 
   658 *}
 
   658 *}
 
   659 
   659 
   660 ML {*
 
   660 ML {*
 
   661 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 
   661 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 
   896   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
 
   896   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
 
   897   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
 
   897   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
 
   898   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
 
   898   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
 
   899   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
 
   899   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
 
   900   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
 
   900   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
 
   901   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
 
   901   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
 
   902   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
 
   902   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
 
   903   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
 
   903   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
 
   904   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
 
   904   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
 
   905   simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
 
   905   simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
 
   906   simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
 
   906   simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
nominal2