12 bymt (Quotient_Type.quotient_type args ctxt) |
12 bymt (Quotient_Type.quotient_type args ctxt) |
13 end |
13 end |
14 *} |
14 *} |
15 |
15 |
16 ML {* |
16 ML {* |
17 fun const_rsp const lthy = |
17 fun const_rsp lthy const = |
18 let |
18 let |
19 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
19 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
20 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
20 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
21 in |
21 in |
22 HOLogic.mk_Trueprop (rel $ const $ const) |
22 HOLogic.mk_Trueprop (rel $ const $ const) |
23 end |
23 end |
24 *} |
24 *} |
25 |
25 |
|
26 (* Replaces bounds by frees and meta implications by implications *) |
26 ML {* |
27 ML {* |
27 fun remove_alls trm = |
28 fun prepare_goal trm = |
28 let |
29 let |
29 val vars = strip_all_vars trm |
30 val vars = strip_all_vars trm |
30 val fs = rev (map Free vars) |
31 val fs = rev (map Free vars) |
|
32 val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm))) |
|
33 val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls) |
|
34 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls) |
31 in |
35 in |
32 ((map fst vars), subst_bounds (fs, (strip_all_body trm))) |
36 (fixes, fold (curry HOLogic.mk_imp) prems concl) |
33 end |
37 end |
34 *} |
38 *} |
35 |
39 |
36 ML {* |
40 ML {* |
37 fun get_rsp_goal thy trm = |
41 fun get_rsp_goal thy trm = |
39 val goalstate = Goal.init (cterm_of thy trm); |
43 val goalstate = Goal.init (cterm_of thy trm); |
40 val tac = REPEAT o rtac @{thm fun_rel_id}; |
44 val tac = REPEAT o rtac @{thm fun_rel_id}; |
41 in |
45 in |
42 case (SINGLE (tac 1) goalstate) of |
46 case (SINGLE (tac 1) goalstate) of |
43 NONE => error "rsp_goal failed" |
47 NONE => error "rsp_goal failed" |
44 | SOME th => remove_alls (term_of (cprem_of th 1)) |
48 | SOME th => prepare_goal (term_of (cprem_of th 1)) |
45 end |
49 end |
46 *} |
50 *} |
47 |
51 |
48 ML {* |
52 ML {* |
49 fun prove_const_rsp bind const tac ctxt = |
53 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm |
|
54 *} |
|
55 |
|
56 ML {* |
|
57 fun prove_const_rsp bind consts tac ctxt = |
50 let |
58 let |
51 val rsp_goal = const_rsp const ctxt |
59 val rsp_goals = map (const_rsp ctxt) consts |
52 val thy = ProofContext.theory_of ctxt |
60 val thy = ProofContext.theory_of ctxt |
53 val (fixed, user_goal) = get_rsp_goal thy rsp_goal |
61 val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals) |
54 val user_thm = Goal.prove ctxt fixed [] user_goal tac |
62 val fixed' = distinct (op =) (flat fixed) |
55 fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' rtac user_thm THEN_ALL_NEW atac) 1 |
63 val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
56 val rsp_thm = Goal.prove ctxt [] [] rsp_goal tac |
64 val user_thm = Goal.prove ctxt fixed' [] user_goal tac |
|
65 val user_thms = map repeat_mp (HOLogic.conj_elims user_thm) |
|
66 fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1 |
|
67 val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals |
57 in |
68 in |
58 ctxt |
69 ctxt |
59 |> snd o Local_Theory.note |
70 |> snd o Local_Theory.note |
60 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), [rsp_thm]) |
71 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
61 |> snd o Local_Theory.note ((bind, []), [user_thm]) |
72 |> snd o Local_Theory.note ((bind, []), user_thms) |
62 end |
73 end |
63 *} |
74 *} |
64 |
75 |
|
76 |
|
77 |
65 ML {* |
78 ML {* |
66 fun fv_rsp_tac induct fv_simps = |
79 fun fvbv_rsp_tac induct fvbv_simps = |
67 eresolve_tac induct THEN_ALL_NEW |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
68 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fv_simps)) |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac |
|
82 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) |
69 *} |
83 *} |
70 |
84 |
71 ML {* |
85 ML {* |
72 fun constr_rsp_tac inj rsp equivps = |
86 fun constr_rsp_tac inj rsp equivps = |
73 let |
87 let |
74 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
88 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
75 in |
89 in |
76 REPEAT o rtac @{thm fun_rel_id} THEN' |
90 REPEAT o rtac impI THEN' |
77 simp_tac (HOL_ss addsimps inj) THEN' |
91 simp_tac (HOL_ss addsimps inj) THEN' |
78 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
92 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
79 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
93 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
80 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
94 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
81 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
95 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
82 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
96 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
83 )) |
97 )) |
84 end |
98 end |
85 *} |
99 *} |
86 |
100 |
|
101 (* Testing code |
|
102 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
|
103 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
|
104 |
|
105 (*ML {* |
|
106 val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] |
|
107 val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) |
|
108 val fixed' = distinct (op =) (flat fixed) |
|
109 val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
|
110 *} |
|
111 prove ug: {* user_goal *} |
|
112 ML_prf {* |
|
113 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
|
114 val fv_simps = @{thms rbv2.simps} |
|
115 *} |
|
116 *) |
87 |
117 |
88 end |
118 end |