110 (*set definition*) |
110 (*set definition*) |
111 fun add_def theory = |
111 fun add_def theory = |
112 if def then |
112 if def then |
113 theory |
113 theory |
114 |> Sign.add_consts_i [(name, setT', NoSyn)] |
114 |> Sign.add_consts_i [(name, setT', NoSyn)] |
115 |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))] |
115 |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) |
|
116 (PrimitiveDefs.mk_defpair (setC, set)))] |
116 |-> (fn [th] => pair (SOME th)) |
117 |-> (fn [th] => pair (SOME th)) |
117 else (NONE, theory); |
118 else (NONE, theory); |
118 fun contract_def NONE th = th |
119 fun contract_def NONE th = th |
119 | contract_def (SOME def_eq) th = |
120 | contract_def (SOME def_eq) th = |
120 let |
121 let |
128 #> Sign.add_consts_i |
129 #> Sign.add_consts_i |
129 [(Rep_name, newT --> oldT, NoSyn), |
130 [(Rep_name, newT --> oldT, NoSyn), |
130 (Abs_name, oldT --> newT, NoSyn)] |
131 (Abs_name, oldT --> newT, NoSyn)] |
131 #> add_def |
132 #> add_def |
132 #-> (fn set_def => |
133 #-> (fn set_def => |
133 PureThy.add_axioms [((typedef_name, typedef_prop), |
134 PureThy.add_axioms [((Binding.name typedef_name, typedef_prop), |
134 [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])] |
135 [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])] |
135 ##>> pair set_def) |
136 ##>> pair set_def) |
136 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
137 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
137 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
138 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
138 #-> (fn ([type_definition], set_def) => fn thy1 => |
139 #-> (fn ([type_definition], set_def) => fn thy1 => |
141 val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
142 val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
142 Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
143 Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
143 thy1 |
144 thy1 |
144 |> Sign.add_path name |
145 |> Sign.add_path name |
145 |> PureThy.add_thms |
146 |> PureThy.add_thms |
146 ([((Rep_name, make @{thm type_definition.Rep}), []), |
147 ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []), |
147 ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), |
148 ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), |
148 ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), |
149 ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), |
149 ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), |
150 ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), |
150 ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []), |
151 ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []), |
151 ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}), |
152 ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}), |