equal
deleted
inserted
replaced
85 asm_full_simp_tac |
85 asm_full_simp_tac |
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
87 *} |
87 *} |
88 |
88 |
89 ML {* |
89 ML {* |
|
90 fun all_eqvts ctxt = |
|
91 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
|
92 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
93 *} |
|
94 |
|
95 ML {* |
90 fun constr_rsp_tac inj rsp equivps = |
96 fun constr_rsp_tac inj rsp equivps = |
91 let |
97 let |
92 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
98 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
93 in |
99 in |
94 REPEAT o rtac impI THEN' |
100 REPEAT o rtac impI THEN' |
95 simp_tac (HOL_ss addsimps inj) THEN' |
101 simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW |
96 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
|
97 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
102 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
98 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
103 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
99 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
104 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
100 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
105 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
101 )) |
106 )) |
132 ML {* |
137 ML {* |
133 fun build_eqvts bind funs tac ctxt = |
138 fun build_eqvts bind funs tac ctxt = |
134 let |
139 let |
135 val pi = Free ("p", @{typ perm}); |
140 val pi = Free ("p", @{typ perm}); |
136 val types = map (domain_type o fastype_of) funs; |
141 val types = map (domain_type o fastype_of) funs; |
137 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
142 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); |
138 val args = map Free (indnames ~~ types); |
143 val args = map Free (indnames ~~ types); |
139 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
144 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
140 fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) |
145 fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) |
141 fun eqvtc (fnctn, arg) = |
146 fun eqvtc (fnctn, arg) = |
142 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
147 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
151 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
156 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
152 apply (erule exE) |
157 apply (erule exE) |
153 apply (rule_tac x="pi \<bullet> pia" in exI) |
158 apply (rule_tac x="pi \<bullet> pia" in exI) |
154 by auto |
159 by auto |
155 |
160 |
156 ML {* |
|
157 fun all_eqvts ctxt = |
|
158 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
|
159 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
160 *} |
|
161 |
161 |
162 ML {* |
162 ML {* |
163 fun mk_minimal_ss ctxt = |
163 fun mk_minimal_ss ctxt = |
164 Simplifier.context ctxt empty_ss |
164 Simplifier.context ctxt empty_ss |
165 setsubgoaler asm_simp_tac |
165 setsubgoaler asm_simp_tac |