1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
|
3 exception LIFT_MATCH of string |
|
4 |
3 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
4 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
5 |
7 |
6 val note: binding * thm -> local_theory -> thm * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
7 end; |
9 end; |
8 |
10 |
9 structure Quotient: QUOTIENT = |
11 structure Quotient: QUOTIENT = |
10 struct |
12 struct |
|
13 |
|
14 (* exception for when quotient and lifted things do not match *) |
|
15 exception LIFT_MATCH of string |
11 |
16 |
12 (* wrappers for define, note and theorem_i *) |
17 (* wrappers for define, note and theorem_i *) |
13 fun define (name, mx, rhs) lthy = |
18 fun define (name, mx, rhs) lthy = |
14 let |
19 let |
15 val ((rhs, (_ , thm)), lthy') = |
20 val ((rhs, (_ , thm)), lthy') = |
148 (* storing the quot-info *) |
153 (* storing the quot-info *) |
149 val qty_str = fst (Term.dest_Type abs_ty) |
154 val qty_str = fst (Term.dest_Type abs_ty) |
150 val _ = tracing ("storing under: " ^ qty_str) |
155 val _ = tracing ("storing under: " ^ qty_str) |
151 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
156 val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
152 (* FIXME: varifyT should not be used *) |
157 (* FIXME: varifyT should not be used *) |
|
158 (* storing of the equiv_thm under a name *) |
|
159 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3 |
153 |
160 |
154 (* interpretation *) |
161 (* interpretation *) |
155 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
162 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
156 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
163 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
157 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
164 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
158 val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4; |
165 val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; |
159 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
166 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
160 |
167 |
161 val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5)); |
168 val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); |
162 val exp_term = Morphism.term exp_morphism; |
169 val exp_term = Morphism.term exp_morphism; |
163 val exp = Morphism.thm exp_morphism; |
170 val exp = Morphism.thm exp_morphism; |
164 |
171 |
165 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
172 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
166 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
173 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
167 val mthdt = Method.Basic (fn _ => mthd) |
174 val mthdt = Method.Basic (fn _ => mthd) |
168 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
175 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
169 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
176 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
170 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
177 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
171 in |
178 in |
172 lthy5 |
179 lthy6 |
173 |> note (quot_thm_name, quot_thm) |
180 |> note (quot_thm_name, quot_thm) |
174 ||>> note (quotient_thm_name, quotient_thm) |
181 ||>> note (quotient_thm_name, quotient_thm) |
175 ||> Local_Theory.theory (fn thy => |
182 ||> Local_Theory.theory (fn thy => |
176 let |
183 let |
177 val global_eqns = map exp_term [eqn2i, eqn1i]; |
184 val global_eqns = map exp_term [eqn2i, eqn1i]; |
178 (* Not sure if the following context should not be used *) |
185 (* Not sure if the following context should not be used *) |
179 val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; |
186 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |
180 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
187 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
181 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
188 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
182 end |
189 end |
183 |
190 |
184 |
191 |