72 |
72 |
73 |
73 |
74 (* tactic to prove the Quot_Type theorem for the new type *) |
74 (* tactic to prove the Quot_Type theorem for the new type *) |
75 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
75 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
76 let |
76 let |
77 val rep_thm = (#Rep typedef_info) RS mem_def1 |
77 val rep_thm = #Rep typedef_info RS mem_def1 |
78 val rep_inv = #Rep_inverse typedef_info |
78 val rep_inv = #Rep_inverse typedef_info |
79 val abs_inv = mem_def2 RS (#Abs_inverse typedef_info) |
79 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
80 val rep_inj = #Rep_inject typedef_info |
80 val rep_inj = #Rep_inject typedef_info |
81 in |
81 in |
82 (rtac @{thm Quot_Type.intro} THEN' |
82 (rtac @{thm Quot_Type.intro} THEN' |
83 RANGE [rtac equiv_thm, |
83 RANGE [rtac equiv_thm, |
84 rtac rep_thm, |
84 rtac rep_thm, |
86 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
86 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
87 rtac rep_inj]) 1 |
87 rtac rep_inj]) 1 |
88 end |
88 end |
89 |
89 |
90 |
90 |
91 (* proves the Quot_Type theorem *) |
91 (* proves the Quot_Type theorem for the new type *) |
92 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
92 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
93 let |
93 let |
94 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
94 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
95 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
95 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
96 |> Syntax.check_term lthy |
96 |> Syntax.check_term lthy |
97 in |
97 in |
98 Goal.prove lthy [] [] goal |
98 Goal.prove lthy [] [] goal |
99 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
99 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
100 end |
100 end |
101 |
101 |
102 (* proves the quotient theorem *) |
102 (* proves the quotient theorem for the new type *) |
103 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
103 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
104 let |
104 let |
105 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
105 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
106 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
106 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
107 |> Syntax.check_term lthy |
107 |> Syntax.check_term lthy |
115 (K typedef_quotient_thm_tac) |
115 (K typedef_quotient_thm_tac) |
116 end |
116 end |
117 |
117 |
118 |
118 |
119 (* main function for constructing a quotient type *) |
119 (* main function for constructing a quotient type *) |
120 fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
120 fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
121 let |
121 let |
122 (* generates the typedef *) |
122 (* generates the typedef *) |
123 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
123 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
124 |
124 |
125 (* abs and rep functions from the typedef *) |
125 (* abs and rep functions from the typedef *) |
139 val rep_name = Binding.prefix_name "rep_" qty_name |
139 val rep_name = Binding.prefix_name "rep_" qty_name |
140 |
140 |
141 val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 |
141 val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 |
142 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 |
142 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 |
143 |
143 |
144 (* quot_type theorem - needed below *) |
144 (* quot_type theorem *) |
145 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 |
145 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 |
146 |
146 |
147 (* quotient theorem *) |
147 (* quotient theorem *) |
148 val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 |
148 val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 |
149 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
149 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
171 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
171 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
172 val rel_tfrees = map fst (Term.add_tfrees rel []) |
172 val rel_tfrees = map fst (Term.add_tfrees rel []) |
173 val rel_frees = map fst (Term.add_frees rel []) |
173 val rel_frees = map fst (Term.add_frees rel []) |
174 val rel_vars = Term.add_vars rel [] |
174 val rel_vars = Term.add_vars rel [] |
175 val rel_tvars = Term.add_tvars rel [] |
175 val rel_tvars = Term.add_tvars rel [] |
176 val qty_str = (Binding.str_of qty_name) ^ ": " |
176 val qty_str = Binding.str_of qty_name ^ ": " |
177 |
177 |
178 val illegal_rel_vars = |
178 val illegal_rel_vars = |
179 if null rel_vars andalso null rel_tvars then [] |
179 if null rel_vars andalso null rel_tvars then [] |
180 else [qty_str ^ "illegal schematic variable(s) in the relation."] |
180 else [qty_str ^ "illegal schematic variable(s) in the relation."] |
181 |
181 |
210 val thy = ProofContext.theory_of ctxt |
210 val thy = ProofContext.theory_of ctxt |
211 |
211 |
212 fun map_check_aux rty warns = |
212 fun map_check_aux rty warns = |
213 case rty of |
213 case rty of |
214 Type (_, []) => warns |
214 Type (_, []) => warns |
215 | Type (s, _) => if (maps_defined thy s) then warns else s::warns |
215 | Type (s, _) => if maps_defined thy s then warns else s::warns |
216 | _ => warns |
216 | _ => warns |
217 |
217 |
218 val warns = map_check_aux rty [] |
218 val warns = map_check_aux rty [] |
219 in |
219 in |
220 if null warns then () |
220 if null warns then () |
253 end |
253 end |
254 |
254 |
255 val goals = map (mk_goal o snd) quot_list |
255 val goals = map (mk_goal o snd) quot_list |
256 |
256 |
257 fun after_qed thms lthy = |
257 fun after_qed thms lthy = |
258 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
258 fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd |
259 in |
259 in |
260 theorem after_qed goals lthy |
260 theorem after_qed goals lthy |
261 end |
261 end |
262 |
262 |
263 fun quotient_type_cmd specs lthy = |
263 fun quotient_type_cmd specs lthy = |