|
1 |
|
2 |
|
3 |
|
4 structure Quotient = |
|
5 struct |
|
6 |
|
7 (* constructs the term lambda (c::rty => bool). EX x. c= rel x *) |
|
8 fun typedef_term rel rty lthy = |
|
9 let |
|
10 val [x, c] = [("x", rty), ("c", rty --> @{typ bool})] |
|
11 |> Variable.variant_frees lthy [rel] |
|
12 |> map Free |
|
13 in |
|
14 lambda c |
|
15 (HOLogic.exists_const rty $ |
|
16 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
|
17 end |
|
18 |
|
19 (* makes the new type definitions and proves non-emptyness*) |
|
20 fun typedef_make (qty_name, mx, rel, rty) lthy = |
|
21 let |
|
22 val typedef_tac = |
|
23 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
|
24 rtac @{thm exI}, |
|
25 rtac @{thm exI}, |
|
26 rtac @{thm refl}] |
|
27 val tfrees = map fst (Term.add_tfreesT rty []) |
|
28 in |
|
29 LocalTheory.theory_result |
|
30 (Typedef.add_typedef false NONE |
|
31 (qty_name, tfrees, mx) |
|
32 (typedef_term rel rty lthy) |
|
33 NONE typedef_tac) lthy |
|
34 end |
|
35 |
|
36 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
|
37 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
|
38 let |
|
39 val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} |
|
40 val rep_thm = #Rep typedef_info |> unfold_mem |
|
41 val rep_inv = #Rep_inverse typedef_info |
|
42 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
|
43 val rep_inj = #Rep_inject typedef_info |
|
44 in |
|
45 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
|
46 rtac equiv_thm, |
|
47 rtac rep_thm, |
|
48 rtac rep_inv, |
|
49 rtac abs_inv, |
|
50 rtac @{thm exI}, |
|
51 rtac @{thm refl}, |
|
52 rtac rep_inj] |
|
53 end |
|
54 |
|
55 (* proves the QUOT_TYPE theorem *) |
|
56 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
|
57 let |
|
58 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
|
59 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
|
60 |> Syntax.check_term lthy |
|
61 in |
|
62 Goal.prove lthy [] [] goal |
|
63 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
|
64 end |
|
65 |
|
66 (* proves the quotient theorem *) |
|
67 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
|
68 let |
|
69 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
|
70 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
|
71 |> Syntax.check_term lthy |
|
72 |
|
73 val typedef_quotient_thm_tac = |
|
74 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
|
75 rtac @{thm QUOT_TYPE.QUOTIENT}, |
|
76 rtac quot_type_thm] |
|
77 in |
|
78 Goal.prove lthy [] [] goal |
|
79 (K typedef_quotient_thm_tac) |
|
80 end |
|
81 |
|
82 (* two wrappers for define and note *) |
|
83 fun make_def (name, mx, rhs) lthy = |
|
84 let |
|
85 val ((rhs, (_ , thm)), lthy') = |
|
86 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
87 in |
|
88 ((rhs, thm), lthy') |
|
89 end |
|
90 |
|
91 fun note_thm (name, thm) lthy = |
|
92 let |
|
93 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
|
94 in |
|
95 (thm', lthy') |
|
96 end |
|
97 |
|
98 (* main function for constructing the quotient type *) |
|
99 fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
|
100 let |
|
101 (* generates typedef *) |
|
102 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
|
103 |
|
104 (* abs and rep functions *) |
|
105 val abs_ty = #abs_type typedef_info |
|
106 val rep_ty = #rep_type typedef_info |
|
107 val abs_name = #Abs_name typedef_info |
|
108 val rep_name = #Rep_name typedef_info |
|
109 val abs = Const (abs_name, rep_ty --> abs_ty) |
|
110 val rep = Const (rep_name, abs_ty --> rep_ty) |
|
111 |
|
112 (* ABS and REP definitions *) |
|
113 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
|
114 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
|
115 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
|
116 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
|
117 val ABS_name = Binding.prefix_name "ABS_" qty_name |
|
118 val REP_name = Binding.prefix_name "REP_" qty_name |
|
119 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
|
120 lthy1 |> make_def (ABS_name, NoSyn, ABS_trm) |
|
121 ||>> make_def (REP_name, NoSyn, REP_trm) |
|
122 |
|
123 (* quot_type theorem *) |
|
124 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
|
125 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
|
126 |
|
127 (* quotient theorem *) |
|
128 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
|
129 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
|
130 |
|
131 (* interpretation *) |
|
132 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
|
133 val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; |
|
134 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
|
135 val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; |
|
136 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
|
137 |
|
138 val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4)); |
|
139 val exp_term = Morphism.term exp_morphism; |
|
140 val exp = Morphism.thm exp_morphism; |
|
141 |
|
142 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
|
143 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
|
144 val mthdt = Method.Basic (fn _ => mthd) |
|
145 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
146 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
|
147 Expression.Named [ |
|
148 ("R", rel), |
|
149 ("Abs", abs), |
|
150 ("Rep", rep) |
|
151 ]))] |
|
152 in |
|
153 lthy4 |
|
154 |> note_thm (quot_thm_name, quot_thm) |
|
155 ||>> note_thm (quotient_thm_name, quotient_thm) |
|
156 ||> LocalTheory.theory (fn thy => |
|
157 let |
|
158 val global_eqns = map exp_term [eqn2i, eqn1i]; |
|
159 (* Not sure if the following context should not be used *) |
|
160 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
|
161 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
|
162 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
|
163 end |
|
164 |
|
165 end; |
|
166 |
|
167 open Quotient |