139 val typedefC = |
139 val typedefC = |
140 Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
140 Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
141 val typedef_prop = |
141 val typedef_prop = |
142 Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
142 Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
143 |
143 |
|
144 fun add_def def def' thy = |
|
145 if def |
|
146 then |
|
147 thy |
|
148 |> PureThy.add_defs_i false [Thm.no_attributes def'] |
|
149 |-> (fn [def'] => pair (SOME def')) |
|
150 else |
|
151 (NONE, thy); |
|
152 |
144 fun typedef_result (theory, nonempty) = |
153 fun typedef_result (theory, nonempty) = |
145 theory |
154 theory |
146 |> put_typedef newT oldT (full Abs_name) (full Rep_name) |
155 |> put_typedef newT oldT (full Abs_name) (full Rep_name) |
147 |> add_typedecls [(t, vs, mx)] |
156 |> add_typedecls [(t, vs, mx)] |
148 |> Theory.add_consts_i |
157 |> Theory.add_consts_i |
149 ((if def then [(name, setT', NoSyn)] else []) @ |
158 ((if def then [(name, setT', NoSyn)] else []) @ |
150 [(Rep_name, newT --> oldT, NoSyn), |
159 [(Rep_name, newT --> oldT, NoSyn), |
151 (Abs_name, oldT --> newT, NoSyn)]) |
160 (Abs_name, oldT --> newT, NoSyn)]) |
152 |> (if def then (apsnd (SOME o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes)) |
161 |> add_def def (Logic.mk_defpair (setC, set)) |
153 [Logic.mk_defpair (setC, set)] |
162 ||>> (PureThy.add_axioms_i [((typedef_name, typedef_prop), |
154 else rpair NONE) |
163 [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] #> Library.swap) |
155 |>>> PureThy.add_axioms_i [((typedef_name, typedef_prop), |
164 ||> Theory.add_finals_i false [RepC, AbsC] |
156 [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] |
165 |-> (fn (set_def, [type_definition]) => fn theory' => |
157 |>> Theory.add_finals_i false [RepC, AbsC] |
|
158 |> (fn (theory', (set_def, [type_definition])) => |
|
159 let |
166 let |
160 fun make th = Drule.standard (th OF [type_definition]); |
167 fun make th = Drule.standard (th OF [type_definition]); |
161 val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
168 val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
162 Rep_cases, Abs_cases, Rep_induct, Abs_induct]) = |
169 Rep_cases, Abs_cases, Rep_induct, Abs_induct]) = |
163 theory' |
170 theory' |