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 )) |
118 val fv_simps = @{thms rbv2.simps} |
123 val fv_simps = @{thms rbv2.simps} |
119 *} |
124 *} |
120 *) |
125 *) |
121 |
126 |
122 ML {* |
127 ML {* |
123 fun build_eqvts bind funs perms simps induct ctxt = |
128 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
129 *} |
|
130 |
|
131 ML {* |
|
132 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW |
|
133 (asm_full_simp_tac (HOL_ss addsimps |
|
134 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
|
135 *} |
|
136 |
|
137 ML {* |
|
138 fun build_eqvts bind funs tac ctxt = |
124 let |
139 let |
125 val pi = Free ("p", @{typ perm}); |
140 val pi = Free ("p", @{typ perm}); |
126 val types = map (domain_type o fastype_of) funs; |
141 val types = map (domain_type o fastype_of) funs; |
127 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); |
128 val args = map Free (indnames ~~ types); |
143 val args = map Free (indnames ~~ types); |
129 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"} |
130 fun eqvtc (fnctn, (arg, perm)) = |
145 fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) |
131 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
146 fun eqvtc (fnctn, arg) = |
132 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
147 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
133 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
148 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) |
134 (asm_full_simp_tac (HOL_ss addsimps |
149 val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) |
135 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
|
136 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
|
137 val thms = HOLogic.conj_elims thm |
150 val thms = HOLogic.conj_elims thm |
138 in |
151 in |
139 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
152 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
140 end |
153 end |
141 *} |
154 *} |
143 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" |
144 apply (erule exE) |
157 apply (erule exE) |
145 apply (rule_tac x="pi \<bullet> pia" in exI) |
158 apply (rule_tac x="pi \<bullet> pia" in exI) |
146 by auto |
159 by auto |
147 |
160 |
148 ML {* |
|
149 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
150 *} |
|
151 ML {* |
|
152 fun all_eqvts ctxt = |
|
153 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
|
154 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
155 *} |
|
156 |
161 |
157 ML {* |
162 ML {* |
158 fun mk_minimal_ss ctxt = |
163 fun mk_minimal_ss ctxt = |
159 Simplifier.context ctxt empty_ss |
164 Simplifier.context ctxt empty_ss |
160 setsubgoaler asm_simp_tac |
165 setsubgoaler asm_simp_tac |