8 |
8 |
9 signature TYPEDEF_PACKAGE = |
9 signature TYPEDEF_PACKAGE = |
10 sig |
10 sig |
11 type info = |
11 type info = |
12 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
12 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
13 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
13 inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
14 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
14 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
15 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
15 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
16 val get_info: theory -> string -> info option |
16 val get_info: theory -> string -> info option |
17 val add_typedef: bool -> string option -> bstring * string list * mixfix -> |
17 val add_typedef: bool -> string option -> bstring * string list * mixfix -> |
18 term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory |
18 term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory |
47 |
47 |
48 (* theory data *) |
48 (* theory data *) |
49 |
49 |
50 type info = |
50 type info = |
51 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
51 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
52 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
52 inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
53 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
53 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
54 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
54 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
55 |
55 |
56 structure TypedefData = TheoryDataFun |
56 structure TypedefData = TheoryDataFun |
57 ( |
57 ( |
88 val setT = Term.fastype_of set; |
88 val setT = Term.fastype_of set; |
89 val rhs_tfrees = Term.add_tfrees set []; |
89 val rhs_tfrees = Term.add_tfrees set []; |
90 val rhs_tfreesT = Term.add_tfreesT setT []; |
90 val rhs_tfreesT = Term.add_tfreesT setT []; |
91 val oldT = HOLogic.dest_setT setT handle TYPE _ => |
91 val oldT = HOLogic.dest_setT setT handle TYPE _ => |
92 error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
92 error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
93 fun mk_nonempty A = |
93 fun mk_inhabited A = |
94 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
94 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
95 val goal = mk_nonempty set; |
95 val goal = mk_inhabited set; |
96 val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT)); |
96 val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT)); |
97 |
97 |
98 (*lhs*) |
98 (*lhs*) |
99 val defS = Sign.defaultS thy; |
99 val defS = Sign.defaultS thy; |
100 val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
100 val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
101 val args_setT = lhs_tfrees |
101 val args_setT = lhs_tfrees |
128 thy |
128 thy |
129 |> PureThy.add_defs false [Thm.no_attributes eq] |
129 |> PureThy.add_defs false [Thm.no_attributes eq] |
130 |-> (fn [th] => pair (SOME th)) |
130 |-> (fn [th] => pair (SOME th)) |
131 else (NONE, thy); |
131 else (NONE, thy); |
132 |
132 |
133 fun typedef_result nonempty = |
133 fun typedef_result inhabited = |
134 ObjectLogic.typedecl (t, vs, mx) |
134 ObjectLogic.typedecl (t, vs, mx) |
135 #> snd |
135 #> snd |
136 #> Sign.add_consts_i |
136 #> Sign.add_consts_i |
137 ((if def then [(name, setT', NoSyn)] else []) @ |
137 ((if def then [(name, setT', NoSyn)] else []) @ |
138 [(Rep_name, newT --> oldT, NoSyn), |
138 [(Rep_name, newT --> oldT, NoSyn), |
139 (Abs_name, oldT --> newT, NoSyn)]) |
139 (Abs_name, oldT --> newT, NoSyn)]) |
140 #> add_def (PrimitiveDefs.mk_defpair (setC, set)) |
140 #> add_def (PrimitiveDefs.mk_defpair (setC, set)) |
141 ##>> PureThy.add_axioms [((typedef_name, typedef_prop), |
141 ##>> PureThy.add_axioms [((typedef_name, typedef_prop), |
142 [apsnd (fn cond_axm => nonempty RS cond_axm)])] |
142 [apsnd (fn cond_axm => inhabited RS cond_axm)])] |
143 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
143 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
144 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
144 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
145 #-> (fn (set_def, [type_definition]) => fn thy1 => |
145 #-> (fn (set_def, [type_definition]) => fn thy1 => |
146 let |
146 let |
147 fun make th = Drule.standard (th OF [type_definition]); |
147 fun make th = Drule.standard (th OF [type_definition]); |
166 ((Abs_name ^ "_induct", make Abs_induct), |
166 ((Abs_name ^ "_induct", make Abs_induct), |
167 [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
167 [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
168 ||> Sign.parent_path; |
168 ||> Sign.parent_path; |
169 val info = {rep_type = oldT, abs_type = newT, |
169 val info = {rep_type = oldT, abs_type = newT, |
170 Rep_name = full Rep_name, Abs_name = full Abs_name, |
170 Rep_name = full Rep_name, Abs_name = full Abs_name, |
171 type_definition = type_definition, set_def = set_def, |
171 inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
172 Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
172 Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
173 Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, |
173 Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, |
174 Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; |
174 Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; |
175 in |
175 in |
176 thy2 |
176 thy2 |