1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 begin |
3 begin |
4 |
|
5 (* |
|
6 prove {* @{prop "True"} *} |
|
7 apply(rule TrueI) |
|
8 done |
|
9 *) |
|
10 |
4 |
11 locale QUOT_TYPE = |
5 locale QUOT_TYPE = |
12 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
6 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
13 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
7 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
14 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
8 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
88 end |
82 end |
89 |
83 |
90 section {* type definition for the quotient type *} |
84 section {* type definition for the quotient type *} |
91 |
85 |
92 ML {* |
86 ML {* |
93 Variable.variant_frees |
|
94 *} |
|
95 |
|
96 |
|
97 ML {* |
|
98 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *) |
87 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *) |
99 fun typedef_term rel ty lthy = |
88 fun typedef_term rel ty lthy = |
100 let |
89 let |
101 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
90 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
102 |> Variable.variant_frees lthy [rel] |
91 |> Variable.variant_frees lthy [rel] |
198 in |
187 in |
199 ((trm, thm), lthy') |
188 ((trm, thm), lthy') |
200 end |
189 end |
201 *} |
190 *} |
202 |
191 |
203 (* |
|
204 locale foo = fixes x :: nat |
|
205 begin |
|
206 |
|
207 ML {* make_def (@{binding foo}, NoSyn, @{term "x + x"}) @{context} *} |
|
208 *) |
|
209 |
|
210 ML {* |
192 ML {* |
211 fun reg_thm (name, thm) lthy = |
193 fun reg_thm (name, thm) lthy = |
212 let |
194 let |
213 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
195 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
214 in |
196 in |
215 (thm',lthy') |
197 (thm', lthy') |
216 end |
198 end |
217 *} |
199 *} |
218 |
200 |
219 ML {* |
201 ML {* |
220 val no_vars = Thm.rule_attribute (fn context => fn th => |
202 val no_vars = Thm.rule_attribute (fn context => fn th => |
222 val ctxt = Variable.set_body false (Context.proof_of context); |
204 val ctxt = Variable.set_body false (Context.proof_of context); |
223 val ((_, [th']), _) = Variable.import true [th] ctxt; |
205 val ((_, [th']), _) = Variable.import true [th] ctxt; |
224 in th' end); |
206 in th' end); |
225 *} |
207 *} |
226 |
208 |
227 ML ProofContext.theory_of |
|
228 |
|
229 ML Expression.interpretation |
|
230 |
|
231 ML {* |
|
232 fun my_print_tac ctxt thm = |
|
233 let |
|
234 val _ = tracing (Display.string_of_thm ctxt thm) |
|
235 in |
|
236 Seq.single thm |
|
237 end *} |
|
238 |
|
239 ML LocalTheory.theory_result |
|
240 |
|
241 |
|
242 ML {* Binding.str_of @{binding foo} *} |
|
243 |
|
244 ML {* |
209 ML {* |
245 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy = |
210 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy = |
246 let |
211 let |
247 (* generates typedef *) |
212 (* generates typedef *) |
248 val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy |
213 val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy |
249 |
214 |
250 (* abs and rep functions *) |
215 (* abs and rep functions *) |
251 val abs_ty = #abs_type typedef_info |
216 val abs_ty = #abs_type typedef_info |
252 val rep_ty = #rep_type typedef_info |
217 val rep_ty = #rep_type typedef_info |
253 val abs_name = #Abs_name typedef_info |
218 val abs_name = #Abs_name typedef_info |
264 val REP_name = Binding.prefix_name "REP_" qty_name |
229 val REP_name = Binding.prefix_name "REP_" qty_name |
265 val (((ABS, ABS_def), (REP, REP_def)), lthy'') = |
230 val (((ABS, ABS_def), (REP, REP_def)), lthy'') = |
266 lthy' |> make_def (ABS_name, NoSyn, ABS_trm) |
231 lthy' |> make_def (ABS_name, NoSyn, ABS_trm) |
267 ||>> make_def (REP_name, NoSyn, REP_trm) |
232 ||>> make_def (REP_name, NoSyn, REP_trm) |
268 |
233 |
269 (* REMOVE VARIFY *) |
|
270 val _ = tracing (Syntax.string_of_typ lthy' (type_of ABS_trm)) |
|
271 val _ = tracing (Syntax.string_of_typ lthy' (type_of REP_trm)) |
|
272 val _ = tracing (Syntax.string_of_typ lthy' (type_of rel)) |
|
273 |
|
274 (* quot_type theorem *) |
234 (* quot_type theorem *) |
275 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy'' |
235 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy'' |
276 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
236 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
277 |
237 |
278 (* quotient theorem *) |
238 (* quotient theorem *) |
289 val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy'''')); |
249 val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy'''')); |
290 val exp_term = Morphism.term exp_morphism; |
250 val exp_term = Morphism.term exp_morphism; |
291 val exp = Morphism.thm exp_morphism; |
251 val exp = Morphism.thm exp_morphism; |
292 |
252 |
293 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
253 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
294 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])) |
254 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
295 (*THEN print_tac "Hello"*)) |
|
296 val mthdt = Method.Basic (fn _ => mthd) |
255 val mthdt = Method.Basic (fn _ => mthd) |
297 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
256 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
298 val exp_i = [(@{const_name QUOT_TYPE},((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
257 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
299 Expression.Named [ |
258 Expression.Named [ |
300 ("R", rel), |
259 ("R", rel), |
301 ("Abs", abs), |
260 ("Abs", abs), |
302 ("Rep", rep) |
261 ("Rep", rep) |
303 ]))] |
262 ]))] |
306 |> reg_thm (quot_thm_name, quot_thm) |
265 |> reg_thm (quot_thm_name, quot_thm) |
307 ||>> reg_thm (quotient_thm_name, quotient_thm) |
266 ||>> reg_thm (quotient_thm_name, quotient_thm) |
308 ||> LocalTheory.theory (fn thy => |
267 ||> LocalTheory.theory (fn thy => |
309 let |
268 let |
310 val global_eqns = map exp_term [eqn2i, eqn1i]; |
269 val global_eqns = map exp_term [eqn2i, eqn1i]; |
|
270 (* Not sure if the following context should not be used *) |
311 val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy''''; |
271 val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy''''; |
312 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
272 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
313 (* val _ = tracing (Syntax.string_of_typ lthy'''' (type_of (fst (Logic.dest_equals (exp_term eqn1i)))));*) |
|
314 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
273 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
315 end |
274 end |
316 *} |
275 *} |
317 |
|
318 |
276 |
319 section {* various tests for quotient types*} |
277 section {* various tests for quotient types*} |
320 datatype trm = |
278 datatype trm = |
321 var "nat" |
279 var "nat" |
322 | app "trm" "trm" |
280 | app "trm" "trm" |
327 |
285 |
328 ML {* |
286 ML {* |
329 typedef_main |
287 typedef_main |
330 *} |
288 *} |
331 |
289 |
332 (*ML {* |
290 local_setup {* |
333 val lthy = @{context}; |
291 typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd |
334 val qty_name = @{binding "qtrm"} |
292 *} |
335 val rel = @{term "RR"} |
|
336 val ty = @{typ trm} |
|
337 val equiv_thm = @{thm r_eq} |
|
338 *}*) |
|
339 |
|
340 local_setup {* |
|
341 fn lthy => |
|
342 Toplevel.program (fn () => |
|
343 exception_trace ( |
|
344 fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy) |
|
345 ) |
|
346 ) |
|
347 *} |
|
348 print_theorems |
|
349 |
|
350 (*thm QUOT_TYPE_I_qtrm.thm11*) |
|
351 |
|
352 |
293 |
353 term Rep_qtrm |
294 term Rep_qtrm |
354 term REP_qtrm |
295 term REP_qtrm |
355 term Abs_qtrm |
296 term Abs_qtrm |
356 term ABS_qtrm |
297 term ABS_qtrm |
357 thm QUOT_TYPE_qtrm |
298 thm QUOT_TYPE_qtrm |
358 thm QUOTIENT_qtrm |
299 thm QUOTIENT_qtrm |
359 |
300 |
|
301 (* Test interpretation *) |
|
302 thm QUOT_TYPE_I_qtrm.thm11 |
|
303 |
360 thm Rep_qtrm |
304 thm Rep_qtrm |
361 |
305 |
362 text {* another test *} |
306 text {* another test *} |
363 datatype 'a my = Foo |
307 datatype 'a my = Foo |
364 consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool" |
308 consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool" |
780 if type_of t = lifted_type then mk_rep_abs t else t |
722 if type_of t = lifted_type then mk_rep_abs t else t |
781 end |
723 end |
782 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
724 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
783 | build_aux (f $ a) = |
725 | build_aux (f $ a) = |
784 let |
726 let |
785 val (f,args) = strip_comb (f $ a) |
727 val (f, args) = strip_comb (f $ a) |
786 val _ = writeln (Syntax.string_of_term @{context} f) |
728 val _ = writeln (Syntax.string_of_term @{context} f) |
787 in |
729 in |
788 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
730 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
789 else list_comb ((build_aux f), (map build_aux args))) |
731 else list_comb ((build_aux f), (map build_aux args))) |
790 end |
732 end |
793 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
735 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
794 in |
736 in |
795 HOLogic.mk_eq ((build_aux concl), concl) |
737 HOLogic.mk_eq ((build_aux concl), concl) |
796 end *} |
738 end *} |
797 |
739 |
|
740 ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *} |
|
741 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
|
742 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
|
743 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
|
744 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
798 |
745 |
799 ML {* |
746 ML {* |
800 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
747 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
801 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
748 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
802 val cgoal = cterm_of @{theory} goal |
749 val cgoal = cterm_of @{theory} goal |
803 *} |
750 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal) |
804 |
751 *} |
805 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
752 |
806 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
753 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
807 |
|
808 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
|
809 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
|
810 |
|
811 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
|
812 |
|
813 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
|
814 apply(rule_tac f="(op =)" in arg_cong2) |
754 apply(rule_tac f="(op =)" in arg_cong2) |
815 unfolding IN_def EMPTY_def |
755 unfolding IN_def EMPTY_def |
816 apply (rule_tac mem_respects) |
756 apply (rule_tac mem_respects) |
817 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
757 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
818 apply (simp_all) |
758 apply (simp_all) |
822 thm length_append (* Not true but worth checking that the goal is correct *) |
762 thm length_append (* Not true but worth checking that the goal is correct *) |
823 ML {* |
763 ML {* |
824 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
764 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
825 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
765 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
826 val cgoal = cterm_of @{theory} goal |
766 val cgoal = cterm_of @{theory} goal |
827 *} |
767 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal) |
828 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
768 *} |
829 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
|
830 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
|
831 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *} |
|
832 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *} |
|
833 |
769 |
834 thm m2 |
770 thm m2 |
835 ML {* |
771 ML {* |
836 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
772 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
837 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
773 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
838 val cgoal = cterm_of @{theory} goal |
774 val cgoal = cterm_of @{theory} goal |
839 *} |
775 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal) |
840 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *} |
776 *} |
841 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *} |
777 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
842 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
|
843 apply(rule_tac f="(op =)" in arg_cong2) |
778 apply(rule_tac f="(op =)" in arg_cong2) |
844 unfolding IN_def |
779 unfolding IN_def |
845 apply (rule_tac mem_respects) |
780 apply (rule_tac mem_respects) |
846 unfolding INSERT_def |
781 unfolding INSERT_def |
847 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
782 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |