26 * theory |
26 * theory |
27 |
27 |
28 val domain_isomorphism_cmd : |
28 val domain_isomorphism_cmd : |
29 (string list * binding * mixfix * string * (binding * binding) option) list |
29 (string list * binding * mixfix * string * (binding * binding) option) list |
30 -> theory -> theory |
30 -> theory -> theory |
31 |
|
32 val setup : theory -> theory |
|
33 end |
31 end |
34 |
32 |
35 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
33 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
36 struct |
34 struct |
37 |
35 |
38 val beta_ss = |
36 val beta_ss = |
39 simpset_of (put_simpset HOL_basic_ss @{context} |
37 simpset_of (put_simpset HOL_basic_ss @{context} |
40 addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]) |
38 addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]) |
41 |
39 |
42 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}) |
40 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}) |
43 |
|
44 (******************************************************************************) |
|
45 (******************************** theory data *********************************) |
|
46 (******************************************************************************) |
|
47 |
|
48 structure RepData = Named_Thms |
|
49 ( |
|
50 val name = @{binding domain_defl_simps} |
|
51 val description = "theorems like DEFL('a t) = t_defl$DEFL('a)" |
|
52 ) |
|
53 |
|
54 structure IsodeflData = Named_Thms |
|
55 ( |
|
56 val name = @{binding domain_isodefl} |
|
57 val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" |
|
58 ) |
|
59 |
|
60 val setup = RepData.setup #> IsodeflData.setup |
|
61 |
41 |
62 |
42 |
63 (******************************************************************************) |
43 (******************************************************************************) |
64 (************************** building types and terms **************************) |
44 (************************** building types and terms **************************) |
65 (******************************************************************************) |
45 (******************************************************************************) |
168 val tuple_fixdef_thm = foldr1 pair_equalI proj_thms |
148 val tuple_fixdef_thm = foldr1 pair_equalI proj_thms |
169 |
149 |
170 val cont_thm = |
150 val cont_thm = |
171 let |
151 let |
172 val prop = mk_trp (mk_cont functional) |
152 val prop = mk_trp (mk_cont functional) |
173 val rules = Cont2ContData.get (Proof_Context.init_global thy) |
153 val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont} |
174 val tac = REPEAT_ALL_NEW (match_tac rules) 1 |
154 val tac = REPEAT_ALL_NEW (match_tac rules) 1 |
175 in |
155 in |
176 Goal.prove_global thy [] [] prop (K tac) |
156 Goal.prove_global thy [] [] prop (K tac) |
177 end |
157 end |
178 |
158 |
205 (thy : theory) |
185 (thy : theory) |
206 (tab1 : (typ * term) list) |
186 (tab1 : (typ * term) list) |
207 (tab2 : (typ * term) list) |
187 (tab2 : (typ * term) list) |
208 (T : typ) : term = |
188 (T : typ) : term = |
209 let |
189 let |
210 val defl_simps = RepData.get (Proof_Context.init_global thy) |
190 val defl_simps = |
|
191 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps} |
211 val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps |
192 val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps |
212 val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2 |
193 val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2 |
213 fun proc1 t = |
194 fun proc1 t = |
214 (case dest_DEFL t of |
195 (case dest_DEFL t of |
215 TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT)) |
196 TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT)) |
520 let |
501 let |
521 val spec = (tbind, map (rpair dummyS) vs, mx) |
502 val spec = (tbind, map (rpair dummyS) vs, mx) |
522 val ((_, _, _, {DEFL, ...}), thy) = |
503 val ((_, _, _, {DEFL, ...}), thy) = |
523 Domaindef.add_domaindef spec defl NONE thy |
504 Domaindef.add_domaindef spec defl NONE thy |
524 (* declare domain_defl_simps rules *) |
505 (* declare domain_defl_simps rules *) |
525 val thy = Context.theory_map (RepData.add_thm DEFL) thy |
506 val thy = |
|
507 Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy |
526 in |
508 in |
527 (DEFL, thy) |
509 (DEFL, thy) |
528 end |
510 end |
529 val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy |
511 val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy |
530 |
512 |
531 (* prove DEFL equations *) |
513 (* prove DEFL equations *) |
532 fun mk_DEFL_eq_thm (lhsT, rhsT) = |
514 fun mk_DEFL_eq_thm (lhsT, rhsT) = |
533 let |
515 let |
534 val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) |
516 val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) |
535 val DEFL_simps = RepData.get (Proof_Context.init_global thy) |
517 val DEFL_simps = |
|
518 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps} |
536 fun tac ctxt = |
519 fun tac ctxt = |
537 rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps) |
520 rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps) |
538 THEN TRY (resolve_tac defl_unfold_thms 1) |
521 THEN TRY (resolve_tac defl_unfold_thms 1) |
539 in |
522 in |
540 Goal.prove_global thy [] [] goal (tac o #context) |
523 Goal.prove_global thy [] [] goal (tac o #context) |
635 val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy |
618 val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy |
636 val map_ID_simps = map (fn th => th RS sym) map_ID_thms |
619 val map_ID_simps = map (fn th => th RS sym) map_ID_thms |
637 val isodefl_rules = |
620 val isodefl_rules = |
638 @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} |
621 @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} |
639 @ isodefl_abs_rep_thms |
622 @ isodefl_abs_rep_thms |
640 @ IsodeflData.get (Proof_Context.init_global thy) |
623 @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl} |
641 in |
624 in |
642 Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => |
625 Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => |
643 EVERY |
626 EVERY |
644 [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms), |
627 [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms), |
645 rtac (@{thm cont_parallel_fix_ind} |
628 rtac (@{thm cont_parallel_fix_ind} |
659 val thmR = thm RS @{thm conjunct2} |
642 val thmR = thm RS @{thm conjunct2} |
660 in (n, thmL):: conjuncts ns thmR end |
643 in (n, thmL):: conjuncts ns thmR end |
661 val (isodefl_thms, thy) = thy |> |
644 val (isodefl_thms, thy) = thy |> |
662 (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
645 (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
663 (conjuncts isodefl_binds isodefl_thm) |
646 (conjuncts isodefl_binds isodefl_thm) |
664 val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy |
647 val thy = |
|
648 fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl}) |
|
649 isodefl_thms thy |
665 |
650 |
666 (* prove map_ID theorems *) |
651 (* prove map_ID theorems *) |
667 fun prove_map_ID_thm |
652 fun prove_map_ID_thm |
668 (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) = |
653 (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) = |
669 let |
654 let |