106 val setT' = map Term.itselfT args_setT ---> setT; |
89 val setT' = map Term.itselfT args_setT ---> setT; |
107 val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); |
90 val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); |
108 val RepC = Const (full Rep_name, newT --> oldT); |
91 val RepC = Const (full Rep_name, newT --> oldT); |
109 val AbsC = Const (full Abs_name, oldT --> newT); |
92 val AbsC = Const (full Abs_name, oldT --> newT); |
110 |
93 |
111 val set' = if def then setC else set; |
94 val A = if def then setC else set; |
112 fun mk_inhabited A = |
95 val goal = |
113 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
96 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
114 val goal = mk_inhabited set'; |
97 val term_binding = (the_default (name, 0) (Syntax.read_variable name), SOME set); |
115 val term_binding = (the_default (name, 0) (Syntax.read_variable name), SOME set) |
|
116 |
98 |
117 val typedef_name = "type_definition_" ^ name; |
99 val typedef_name = "type_definition_" ^ name; |
118 val typedefC = |
100 val typedefC = |
119 Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
101 Const (@{const_name type_definition}, |
120 val typedef_prop = |
102 (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
121 Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
103 val typedef_prop = Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)); |
122 val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' []; |
104 val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) A []; |
123 |
105 |
124 val (set_def, thy') = if def then |
106 val (set_def, thy') = |
|
107 if def then |
125 thy |
108 thy |
126 |> Sign.add_consts_i [(name, setT', NoSyn)] |
109 |> Sign.add_consts_i [(name, setT', NoSyn)] |
127 |> PureThy.add_defs false [Thm.no_attributes (PrimitiveDefs.mk_defpair (setC, set))] |
110 |> PureThy.add_defs false [Thm.no_attributes (PrimitiveDefs.mk_defpair (setC, set))] |
128 |-> (fn [th] => pair (SOME th)) |
111 |-> (fn [th] => pair (SOME th)) |
129 else (NONE, thy); |
112 else (NONE, thy); |
130 |
113 |
131 fun typedef_result inhabited = |
114 fun typedef_result inhabited = |
132 ObjectLogic.typedecl (t, vs, mx) |
115 ObjectLogic.typedecl (t, vs, mx) |
133 #> snd |
116 #> snd |
134 #> Sign.add_consts_i |
117 #> Sign.add_consts_i |
135 [(Rep_name, newT --> oldT, NoSyn), |
118 [(Rep_name, newT --> oldT, NoSyn), |
136 (Abs_name, oldT --> newT, NoSyn)] |
119 (Abs_name, oldT --> newT, NoSyn)] |
137 #> PureThy.add_axioms [((typedef_name, typedef_prop), |
120 #> PureThy.add_axioms [((typedef_name, typedef_prop), |
138 [apsnd (fn cond_axm => inhabited RS cond_axm)])] |
121 [Thm.rule_attribute (fn _ => fn cond_axm => inhabited RS cond_axm)])] |
139 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
122 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
140 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
123 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
141 #-> (fn [type_definition] => fn thy1 => |
124 #-> (fn [type_definition] => fn thy1 => |
142 let |
125 let |
143 fun make th = Drule.standard (th OF [type_definition]); |
126 fun make th = Drule.standard (th OF [type_definition]); |
144 val abs_inject = make Abs_inject; |
|
145 val abs_inverse = make Abs_inverse; |
|
146 val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
127 val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
147 Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
128 Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
148 thy1 |
129 thy1 |
149 |> Sign.add_path name |
130 |> Sign.add_path name |
150 |> PureThy.add_thms |
131 |> PureThy.add_thms |
151 ([((Rep_name, make Rep), []), |
132 ([((Rep_name, make @{thm type_definition.Rep}), []), |
152 ((Rep_name ^ "_inverse", make Rep_inverse), []), |
133 ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), |
153 ((Abs_name ^ "_inverse", abs_inverse), []), |
134 ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), |
154 ((Rep_name ^ "_inject", make Rep_inject), []), |
135 ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), |
155 ((Abs_name ^ "_inject", abs_inject), []), |
136 ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []), |
156 ((Rep_name ^ "_cases", make Rep_cases), |
137 ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}), |
157 [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), |
138 [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), |
158 ((Abs_name ^ "_cases", make Abs_cases), |
139 ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}), |
159 [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), |
140 [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), |
160 ((Rep_name ^ "_induct", make Rep_induct), |
141 ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}), |
161 [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), |
142 [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), |
162 ((Abs_name ^ "_induct", make Abs_induct), |
143 ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}), |
163 [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
144 [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
164 ||> Sign.parent_path; |
145 ||> Sign.parent_path; |
165 val info = {rep_type = oldT, abs_type = newT, |
146 val info = {rep_type = oldT, abs_type = newT, |
166 Rep_name = full Rep_name, Abs_name = full Abs_name, |
147 Rep_name = full Rep_name, Abs_name = full Abs_name, |
167 inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
148 inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
218 handle ERROR msg => cat_error msg |
200 handle ERROR msg => cat_error msg |
219 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
201 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
220 in typedef_result non_empty thy' end; |
202 in typedef_result non_empty thy' end; |
221 |
203 |
222 |
204 |
223 (* Isar typedef interface *) |
205 (* typedef: proof interface *) |
224 |
206 |
225 local |
207 local |
226 |
208 |
227 fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = |
209 fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = |
228 let |
210 let |
229 val ((_, goal, term_binding, set_def, typedef_result), thy') = |
211 val ((_, goal, term_binding, set_def, typedef_result), thy') = |
230 prepare_typedef prep_term def name typ set opt_morphs thy; |
212 prepare_typedef prep_term def name typ set opt_morphs thy; |
231 fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); |
213 fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); |
232 in |
214 in |
233 Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy') |
215 ProofContext.init thy' |
234 |> Proof.add_binds_i [term_binding] |
216 |> Proof.theorem_i NONE after_qed [[(goal, [])]] |
235 |> (if def |
217 |> Proof.add_binds_i [term_binding] |
236 then Seq.hd o Proof.refine (Method.Basic (Method.unfold [the set_def], Position.none)) |
218 |> Proof.unfolding_i [[(the_list set_def, [])]] |
237 else I) |
|
238 end; |
219 end; |
239 |
220 |
240 in |
221 in |
241 |
222 |
242 val typedef = gen_typedef Syntax.check_term; |
223 val typedef = gen_typedef Syntax.check_term; |