130 fun eqvtc (fnctn, (arg, perm)) = |
130 fun eqvtc (fnctn, (arg, perm)) = |
131 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
131 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
132 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
132 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
133 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
133 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
134 (asm_full_simp_tac (HOL_ss addsimps |
134 (asm_full_simp_tac (HOL_ss addsimps |
135 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
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 |
136 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
137 val thms = HOLogic.conj_elims thm |
137 val thms = HOLogic.conj_elims thm |
138 in |
138 in |
139 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
139 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
140 end |
140 end |
159 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
159 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
160 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
160 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
161 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
161 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
162 ( |
162 ( |
163 (asm_full_simp_tac (HOL_ss addsimps |
163 (asm_full_simp_tac (HOL_ss addsimps |
164 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
164 ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))) |
165 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' |
165 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' |
166 REPEAT o etac conjE THEN' |
166 REPEAT o etac conjE THEN' |
167 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
167 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
168 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
168 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
169 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
169 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
170 (asm_full_simp_tac (HOL_ss addsimps |
170 (asm_full_simp_tac (HOL_ss addsimps |
171 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1 |
171 ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1 |
172 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
172 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
173 in |
173 in |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
175 end |
175 end |
176 *} |
176 *} |