26 infix -->>; |
26 infix -->>; |
27 |
27 |
28 (** type definitions **) |
28 (** type definitions **) |
29 |
29 |
30 type rep_info = |
30 type rep_info = |
31 { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }; |
31 { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm }; |
32 |
32 |
33 (* building types and terms *) |
33 (* building types and terms *) |
34 |
34 |
35 val udomT = @{typ udom}; |
35 val udomT = @{typ udom}; |
36 fun alg_deflT T = Type (@{type_name alg_defl}, [T]); |
36 val sfpT = @{typ sfp}; |
37 fun emb_const T = Const (@{const_name emb}, T ->> udomT); |
37 fun emb_const T = Const (@{const_name emb}, T ->> udomT); |
38 fun prj_const T = Const (@{const_name prj}, udomT ->> T); |
38 fun prj_const T = Const (@{const_name prj}, udomT ->> T); |
39 fun approx_const T = Const (@{const_name approx}, natT --> (T ->> T)); |
39 fun sfp_const T = Const (@{const_name sfp}, Term.itselfT T --> sfpT); |
40 |
40 |
41 fun cast_const T = Const (@{const_name cast}, alg_deflT T ->> T ->> T); |
|
42 fun mk_cast (t, x) = |
41 fun mk_cast (t, x) = |
43 capply_const (udomT, udomT) |
42 capply_const (udomT, udomT) |
44 $ (capply_const (alg_deflT udomT, udomT ->> udomT) $ cast_const udomT $ t) |
43 $ (capply_const (sfpT, udomT ->> udomT) $ @{const cast} $ t) |
45 $ x; |
44 $ x; |
46 |
45 |
47 (* manipulating theorems *) |
46 (* manipulating theorems *) |
48 |
47 |
49 (* proving class instances *) |
48 (* proving class instances *) |
83 (*morphisms*) |
82 (*morphisms*) |
84 val morphs = opt_morphs |
83 val morphs = opt_morphs |
85 |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); |
84 |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); |
86 |
85 |
87 (*set*) |
86 (*set*) |
88 val in_defl = @{term "in_deflation :: udom => udom alg_defl => bool"}; |
87 val in_defl = @{term "in_sfp :: udom => sfp => bool"}; |
89 val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); |
88 val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); |
90 |
89 |
91 (*pcpodef*) |
90 (*pcpodef*) |
92 val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; |
91 val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_sfp} 1; |
93 val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; |
92 val tac2 = rtac @{thm adm_mem_Collect_in_sfp} 1; |
94 val ((info, cpo_info, pcpo_info), thy) = thy |
93 val ((info, cpo_info, pcpo_info), thy) = thy |
95 |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); |
94 |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); |
96 |
95 |
97 (*definitions*) |
96 (*definitions*) |
98 val Rep_const = Const (#Rep_name (#1 info), newT --> udomT); |
97 val Rep_const = Const (#Rep_name (#1 info), newT --> udomT); |
99 val Abs_const = Const (#Abs_name (#1 info), udomT --> newT); |
98 val Abs_const = Const (#Abs_name (#1 info), udomT --> newT); |
100 val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const); |
99 val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const); |
101 val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ |
100 val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $ |
102 Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); |
101 Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0))); |
103 val repdef_approx_const = |
102 val sfp_eqn = Logic.mk_equals (sfp_const newT, |
104 Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) |
103 Abs ("x", Term.itselfT newT, defl)); |
105 --> alg_deflT udomT --> natT --> (newT ->> newT)); |
|
106 val approx_eqn = Logic.mk_equals (approx_const newT, |
|
107 repdef_approx_const $ Rep_const $ Abs_const $ defl); |
|
108 val name_def = Binding.suffix_name "_def" name; |
104 val name_def = Binding.suffix_name "_def" name; |
109 val emb_bind = (Binding.prefix_name "emb_" name_def, []); |
105 val emb_bind = (Binding.prefix_name "emb_" name_def, []); |
110 val prj_bind = (Binding.prefix_name "prj_" name_def, []); |
106 val prj_bind = (Binding.prefix_name "prj_" name_def, []); |
111 val approx_bind = (Binding.prefix_name "approx_" name_def, []); |
107 val sfp_bind = (Binding.prefix_name "sfp_" name_def, []); |
112 |
108 |
113 (*instantiate class rep*) |
109 (*instantiate class rep*) |
114 val lthy = thy |
110 val lthy = thy |
115 |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep}); |
111 |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp}); |
116 val ((_, (_, emb_ldef)), lthy) = |
112 val ((_, (_, emb_ldef)), lthy) = |
117 Specification.definition (NONE, (emb_bind, emb_eqn)) lthy; |
113 Specification.definition (NONE, (emb_bind, emb_eqn)) lthy; |
118 val ((_, (_, prj_ldef)), lthy) = |
114 val ((_, (_, prj_ldef)), lthy) = |
119 Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; |
115 Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; |
120 val ((_, (_, approx_ldef)), lthy) = |
116 val ((_, (_, sfp_ldef)), lthy) = |
121 Specification.definition (NONE, (approx_bind, approx_eqn)) lthy; |
117 Specification.definition (NONE, (sfp_bind, sfp_eqn)) lthy; |
122 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
118 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
123 val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; |
119 val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; |
124 val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef; |
120 val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef; |
125 val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef; |
121 val sfp_def = singleton (ProofContext.export lthy ctxt_thy) sfp_ldef; |
126 val type_definition_thm = |
122 val type_definition_thm = |
127 MetaSimplifier.rewrite_rule |
123 MetaSimplifier.rewrite_rule |
128 (the_list (#set_def (#2 info))) |
124 (the_list (#set_def (#2 info))) |
129 (#type_definition (#2 info)); |
125 (#type_definition (#2 info)); |
130 val typedef_thms = |
126 val typedef_thms = |
131 [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; |
127 [type_definition_thm, #below_def cpo_info, emb_def, prj_def, sfp_def]; |
132 val thy = lthy |
128 val thy = lthy |
133 |> Class.prove_instantiation_instance |
129 |> Class.prove_instantiation_instance |
134 (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |
130 (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |
135 |> Local_Theory.exit_global; |
131 |> Local_Theory.exit_global; |
136 |
132 |
137 (*other theorems*) |
133 (*other theorems*) |
138 val typedef_thms' = map (Thm.transfer thy) |
134 val sfp_thm' = Thm.transfer thy sfp_def; |
139 [type_definition_thm, #below_def cpo_info, emb_def, prj_def]; |
135 val (SFP_thm, thy) = thy |
140 val (REP_thm, thy) = thy |
|
141 |> Sign.add_path (Binding.name_of name) |
136 |> Sign.add_path (Binding.name_of name) |
142 |> Global_Theory.add_thm |
137 |> Global_Theory.add_thm |
143 ((Binding.prefix_name "REP_" name, |
138 ((Binding.prefix_name "SFP_" name, |
144 Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), []) |
139 Drule.zero_var_indexes (@{thm typedef_SFP} OF [sfp_thm'])), []) |
145 ||> Sign.restore_naming thy; |
140 ||> Sign.restore_naming thy; |
146 |
141 |
147 val rep_info = |
142 val rep_info = |
148 { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; |
143 { emb_def = emb_def, prj_def = prj_def, sfp_def = sfp_def, SFP = SFP_thm }; |
149 in |
144 in |
150 ((info, cpo_info, pcpo_info, rep_info), thy) |
145 ((info, cpo_info, pcpo_info, rep_info), thy) |
151 end |
146 end |
152 handle ERROR msg => |
147 handle ERROR msg => |
153 cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); |
148 cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); |