66 (*rhs*) |
66 (*rhs*) |
67 val (_, tmp_lthy) = |
67 val (_, tmp_lthy) = |
68 thy |> Theory.copy |> Theory_Target.init NONE |
68 thy |> Theory.copy |> Theory_Target.init NONE |
69 |> Typedecl.predeclare_constraints (tname, raw_args, mx); |
69 |> Typedecl.predeclare_constraints (tname, raw_args, mx); |
70 val defl = prep_term tmp_lthy raw_defl; |
70 val defl = prep_term tmp_lthy raw_defl; |
71 val tmp_lthy' = tmp_lthy |> Variable.declare_constraints defl; |
71 val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl; |
72 |
72 |
73 val deflT = Term.fastype_of defl; |
73 val deflT = Term.fastype_of defl; |
74 val _ = if deflT = @{typ "udom alg_defl"} then () |
74 val _ = if deflT = @{typ "udom alg_defl"} then () |
75 else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT)); |
75 else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT)); |
76 |
76 |
77 (*lhs*) |
77 (*lhs*) |
78 val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; |
78 val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args; |
79 val lhs_sorts = map snd lhs_tfrees; |
79 val lhs_sorts = map snd lhs_tfrees; |
80 val full_tname = Sign.full_name thy tname; |
80 val full_tname = Sign.full_name thy tname; |
81 val newT = Type (full_tname, map TFree lhs_tfrees); |
81 val newT = Type (full_tname, map TFree lhs_tfrees); |
82 |
82 |
83 (*morphisms*) |
83 (*morphisms*) |
89 val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); |
89 val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl); |
90 |
90 |
91 (*pcpodef*) |
91 (*pcpodef*) |
92 val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; |
92 val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1; |
93 val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; |
93 val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1; |
94 val ((info, cpo_info, pcpo_info), thy2) = thy |
94 val ((info, cpo_info, pcpo_info), thy) = thy |
95 |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); |
95 |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2); |
96 |
96 |
97 (*definitions*) |
97 (*definitions*) |
98 val Rep_const = Const (#Rep_name info, newT --> udomT); |
98 val Rep_const = Const (#Rep_name info, newT --> udomT); |
99 val Abs_const = Const (#Abs_name info, udomT --> newT); |
99 val Abs_const = Const (#Abs_name info, udomT --> newT); |
103 val repdef_approx_const = |
103 val repdef_approx_const = |
104 Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) |
104 Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT) |
105 --> alg_deflT udomT --> natT --> (newT ->> newT)); |
105 --> alg_deflT udomT --> natT --> (newT ->> newT)); |
106 val approx_eqn = Logic.mk_equals (approx_const newT, |
106 val approx_eqn = Logic.mk_equals (approx_const newT, |
107 repdef_approx_const $ Rep_const $ Abs_const $ defl); |
107 repdef_approx_const $ Rep_const $ Abs_const $ defl); |
|
108 val name_def = Binding.suffix_name "_def" name; |
|
109 val emb_bind = (Binding.prefix_name "emb_" name_def, []); |
|
110 val prj_bind = (Binding.prefix_name "prj_" name_def, []); |
|
111 val approx_bind = (Binding.prefix_name "approx_" name_def, []); |
108 |
112 |
109 (*instantiate class rep*) |
113 (*instantiate class rep*) |
110 val name_def = Binding.suffix_name "_def" name; |
114 val lthy = thy |
111 val ([emb_ldef, prj_ldef, approx_ldef], lthy3) = thy2 |
115 |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep}); |
112 |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep}) |
116 val ((_, (_, emb_ldef)), lthy) = |
113 |> fold_map Specification.definition |
117 Specification.definition (NONE, (emb_bind, emb_eqn)) lthy; |
114 [ (NONE, ((Binding.prefix_name "emb_" name_def, []), emb_eqn)) |
118 val ((_, (_, prj_ldef)), lthy) = |
115 , (NONE, ((Binding.prefix_name "prj_" name_def, []), prj_eqn)) |
119 Specification.definition (NONE, (prj_bind, prj_eqn)) lthy; |
116 , (NONE, ((Binding.prefix_name "approx_" name_def, []), approx_eqn)) ] |
120 val ((_, (_, approx_ldef)), lthy) = |
117 |>> map (snd o snd); |
121 Specification.definition (NONE, (approx_bind, approx_eqn)) lthy; |
118 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3); |
122 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); |
119 val [emb_def, prj_def, approx_def] = |
123 val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef; |
120 ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef]; |
124 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 type_definition_thm = |
126 val type_definition_thm = |
122 MetaSimplifier.rewrite_rule |
127 MetaSimplifier.rewrite_rule |
123 (the_list (#set_def info)) |
128 (the_list (#set_def info)) |
124 (#type_definition info); |
129 (#type_definition info); |
125 val typedef_thms = |
130 val typedef_thms = |
126 [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; |
131 [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def]; |
127 val thy4 = lthy3 |
132 val thy = lthy |
128 |> Class.prove_instantiation_instance |
133 |> Class.prove_instantiation_instance |
129 (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |
134 (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1)) |
130 |> Local_Theory.exit_global; |
135 |> Local_Theory.exit_global; |
131 |
136 |
132 (*other theorems*) |
137 (*other theorems*) |
133 val typedef_thms' = map (Thm.transfer thy4) |
138 val typedef_thms' = map (Thm.transfer thy) |
134 [type_definition_thm, #below_def cpo_info, emb_def, prj_def]; |
139 [type_definition_thm, #below_def cpo_info, emb_def, prj_def]; |
135 val ([REP_thm], thy5) = thy4 |
140 val (REP_thm, thy) = thy |
136 |> Sign.add_path (Binding.name_of name) |
141 |> Sign.add_path (Binding.name_of name) |
137 |> PureThy.add_thms |
142 |> PureThy.add_thm |
138 [((Binding.prefix_name "REP_" name, |
143 ((Binding.prefix_name "REP_" name, |
139 Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])] |
144 Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), []) |
140 ||> Sign.restore_naming thy4; |
145 ||> Sign.restore_naming thy; |
141 |
146 |
142 val rep_info = |
147 val rep_info = |
143 { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; |
148 { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; |
144 in |
149 in |
145 ((info, cpo_info, pcpo_info, rep_info), thy5) |
150 ((info, cpo_info, pcpo_info, rep_info), thy) |
146 end |
151 end |
147 handle ERROR msg => |
152 handle ERROR msg => |
148 cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); |
153 cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name)); |
149 |
154 |
150 fun add_repdef def opt_name typ defl opt_morphs thy = |
155 fun add_repdef def opt_name typ defl opt_morphs thy = |