74 (qty_name, tfrees, mx) |
74 (qty_name, tfrees, mx) |
75 (typedef_term rel rty lthy) |
75 (typedef_term rel rty lthy) |
76 NONE typedef_tac) lthy |
76 NONE typedef_tac) lthy |
77 end |
77 end |
78 |
78 |
79 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
79 (* tactic to prove the Quot_Type theorem for the new type *) |
80 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
80 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
81 let |
81 let |
82 val rep_thm = (#Rep typedef_info) RS mem_def1 |
82 val rep_thm = (#Rep typedef_info) RS mem_def1 |
83 val rep_inv = #Rep_inverse typedef_info |
83 val rep_inv = #Rep_inverse typedef_info |
84 val abs_inv = mem_def2 RS (#Abs_inverse typedef_info) |
84 val abs_inv = mem_def2 RS (#Abs_inverse typedef_info) |
85 val rep_inj = #Rep_inject typedef_info |
85 val rep_inj = #Rep_inject typedef_info |
86 in |
86 in |
87 (rtac @{thm QUOT_TYPE.intro} THEN' |
87 (rtac @{thm Quot_Type.intro} THEN' |
88 RANGE [rtac equiv_thm, |
88 RANGE [rtac equiv_thm, |
89 rtac rep_thm, |
89 rtac rep_thm, |
90 rtac rep_inv, |
90 rtac rep_inv, |
91 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
91 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
92 rtac rep_inj]) 1 |
92 rtac rep_inj]) 1 |
93 end |
93 end |
94 |
94 |
95 (* proves the QUOT_TYPE theorem *) |
95 (* proves the Quot_Type theorem *) |
96 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
96 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
97 let |
97 let |
98 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
98 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
99 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
99 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
100 |> Syntax.check_term lthy |
100 |> Syntax.check_term lthy |
101 in |
101 in |
102 Goal.prove lthy [] [] goal |
102 Goal.prove lthy [] [] goal |
103 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
103 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
132 val rep_name = #Rep_name typedef_info |
132 val rep_name = #Rep_name typedef_info |
133 val abs = Const (abs_name, rep_ty --> abs_ty) |
133 val abs = Const (abs_name, rep_ty --> abs_ty) |
134 val rep = Const (rep_name, abs_ty --> rep_ty) |
134 val rep = Const (rep_name, abs_ty --> rep_ty) |
135 |
135 |
136 (* more abstract ABS and REP definitions *) |
136 (* more abstract ABS and REP definitions *) |
137 val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) |
137 val ABS_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
138 val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) |
138 val REP_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
139 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
139 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
140 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
140 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
141 val ABS_name = Binding.prefix_name "abs_" qty_name |
141 val ABS_name = Binding.prefix_name "abs_" qty_name |
142 val REP_name = Binding.prefix_name "rep_" qty_name |
142 val REP_name = Binding.prefix_name "rep_" qty_name |
143 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
143 |
144 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
144 val ((ABS, ABS_def), lthy2) = define (ABS_name, NoSyn, ABS_trm) lthy1 |
145 ||>> define (REP_name, NoSyn, REP_trm) |
145 val ((REP, REP_def), lthy3) = define (REP_name, NoSyn, REP_trm) lthy2 |
146 |
146 |
147 (* quot_type theorem - needed below *) |
147 (* quot_type theorem - needed below *) |
148 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
148 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy3 |
149 |
149 |
150 (* quotient theorem *) |
150 (* quotient theorem *) |
151 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
151 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy3 |
152 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
152 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
153 |
153 |
154 (* storing the quot-info *) |
154 (* storing the quot-info *) |
155 val qty_str = fst (Term.dest_Type abs_ty) |
155 val qty_str = fst (Term.dest_Type abs_ty) |
156 val lthy3 = quotdata_update qty_str |
156 val lthy4 = quotdata_update qty_str |
157 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
157 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3 |
158 (* FIXME: varifyT should not be used *) |
158 (* FIXME: varifyT should not be used *) |
159 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
159 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
160 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
160 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
161 |
161 |
162 in |
162 in |
163 lthy3 |
163 lthy4 |
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 end |
166 end |
167 |
|
168 |
|
169 |
167 |
170 |
168 |
171 (* interface and syntax setup *) |
169 (* interface and syntax setup *) |
172 |
170 |
173 (* the ML-interface takes a list of 4-tuples consisting of *) |
171 (* the ML-interface takes a list of 4-tuples consisting of *) |