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