30 let |
30 let |
31 val str = Sign.full_name thy name; |
31 val str = Sign.full_name thy name; |
32 |
32 |
33 (* typedef *) |
33 (* typedef *) |
34 val set = atom_decl_set str; |
34 val set = atom_decl_set str; |
35 fun tac _ = rtac @{thm exists_eq_simple_sort} 1; |
35 fun tac ctxt = resolve_tac ctxt @{thms exists_eq_simple_sort} 1; |
36 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
36 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
37 Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy; |
37 Typedef.add_typedef_global {overloaded = false} (name, [], NoSyn) set NONE tac thy; |
38 |
38 |
39 (* definition of atom and permute *) |
39 (* definition of atom and permute *) |
40 val newT = #abs_type (fst info); |
40 val newT = #abs_type (fst info); |
41 val RepC = Const (Rep_name, newT --> @{typ atom}); |
41 val RepC = Const (Rep_name, newT --> @{typ atom}); |
42 val AbsC = Const (Abs_name, @{typ atom} --> newT); |
42 val AbsC = Const (Abs_name, @{typ atom} --> newT); |
66 val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; |
66 val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; |
67 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
67 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
68 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
68 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
69 val thy = lthy |
69 val thy = lthy |
70 |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) |
70 |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) |
71 |> Class.prove_instantiation_instance (K (rtac class_thm 1)) |
71 |> Class.prove_instantiation_instance (fn ctxt => resolve_tac ctxt [class_thm] 1) |
72 |> Local_Theory.exit_global; |
72 |> Local_Theory.exit_global; |
73 in |
73 in |
74 thy |
74 thy |
75 end; |
75 end; |
76 |
76 |