144 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
144 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
145 val perms_name = space_implode "_" perm_fn_names |
145 val perms_name = space_implode "_" perm_fn_names |
146 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
146 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
147 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
147 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
148 |
148 |
149 fun tac _ (_, simps, _) = |
149 fun tac _ (_, _, simps) = |
150 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
150 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
151 |
151 |
152 fun morphism phi (dfs, simps, fvs) = |
152 fun morphism phi (fvs, dfs, simps) = |
153 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
153 (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
|
154 |
|
155 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
154 in |
156 in |
155 lthy' |
157 lthy' |
|
158 (*|> snd o (Local_Theory.note ((Binding.empty, [eqvt_attrib]), perm_eq_thms))*) |
156 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
159 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
157 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
160 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
158 |> Class_Target.prove_instantiation_exit_result morphism tac |
161 |> Class_Target.prove_instantiation_exit_result morphism tac |
159 (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs) |
162 (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') |
160 end |
163 end |
161 *} |
164 *} |
162 |
165 |
163 |
166 |
164 |
167 |