equal
deleted
inserted
replaced
12 val add_atom_decl: (binding * (binding option)) -> theory -> theory |
12 val add_atom_decl: (binding * (binding option)) -> theory -> theory |
13 end; |
13 end; |
14 |
14 |
15 structure Atom_Decl :> ATOM_DECL = |
15 structure Atom_Decl :> ATOM_DECL = |
16 struct |
16 struct |
|
17 |
|
18 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
17 |
19 |
18 fun atom_decl_set (str : string) : term = |
20 fun atom_decl_set (str : string) : term = |
19 let |
21 let |
20 val a = Free ("a", @{typ atom}); |
22 val a = Free ("a", @{typ atom}); |
21 val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) |
23 val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) |
46 val permute_eqn = |
48 val permute_eqn = |
47 HOLogic.mk_Trueprop (HOLogic.mk_eq |
49 HOLogic.mk_Trueprop (HOLogic.mk_eq |
48 (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); |
50 (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); |
49 val atom_def_name = |
51 val atom_def_name = |
50 Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); |
52 Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); |
|
53 val sort_thm_name = |
|
54 Binding.prefix_name "atom_" (Binding.suffix_name "_sort" name); |
51 val permute_def_name = |
55 val permute_def_name = |
52 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
56 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
53 |
57 |
54 (* at class instance *) |
58 (* at class instance *) |
55 val lthy = |
59 val lthy = |
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
64 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
61 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
65 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
62 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
66 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
63 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
67 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
64 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
68 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
|
69 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
65 val thy = lthy |
70 val thy = lthy |
66 |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) |
71 |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) |
|
72 |> Class.prove_instantiation_instance (K (rtac class_thm 1)) |
67 |> Local_Theory.exit_global; |
73 |> Local_Theory.exit_global; |
68 in |
74 in |
69 thy |
75 thy |
70 end; |
76 end; |
71 |
77 |