|
1 theory Rsp |
|
2 imports Abs |
|
3 begin |
|
4 |
|
5 ML {* |
|
6 fun define_quotient_type args tac ctxt = |
|
7 let |
|
8 val mthd = Method.SIMPLE_METHOD tac |
|
9 val mthdt = Method.Basic (fn _ => mthd) |
|
10 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
11 in |
|
12 bymt (Quotient_Type.quotient_type args ctxt) |
|
13 end |
|
14 *} |
|
15 |
|
16 ML {* |
|
17 fun const_rsp const lthy = |
|
18 let |
|
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); |
|
21 in |
|
22 HOLogic.mk_Trueprop (rel $ const $ const) |
|
23 end |
|
24 *} |
|
25 |
|
26 ML {* |
|
27 fun remove_alls trm = |
|
28 let |
|
29 val vars = strip_all_vars trm |
|
30 val fs = rev (map Free vars) |
|
31 in |
|
32 ((map fst vars), subst_bounds (fs, (strip_all_body trm))) |
|
33 end |
|
34 *} |
|
35 |
|
36 ML {* |
|
37 fun get_rsp_goal thy trm = |
|
38 let |
|
39 val goalstate = Goal.init (cterm_of thy trm); |
|
40 val tac = REPEAT o rtac @{thm fun_rel_id}; |
|
41 in |
|
42 case (SINGLE (tac 1) goalstate) of |
|
43 NONE => error "rsp_goal failed" |
|
44 | SOME th => remove_alls (term_of (cprem_of th 1)) |
|
45 end |
|
46 *} |
|
47 |
|
48 ML {* |
|
49 fun prove_const_rsp bind const tac ctxt = |
|
50 let |
|
51 val rsp_goal = const_rsp const ctxt |
|
52 val thy = ProofContext.theory_of ctxt |
|
53 val (fixed, user_goal) = get_rsp_goal thy rsp_goal |
|
54 val user_thm = Goal.prove ctxt fixed [] user_goal tac |
|
55 fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' rtac user_thm THEN_ALL_NEW atac) 1 |
|
56 val rsp_thm = Goal.prove ctxt [] [] rsp_goal tac |
|
57 in |
|
58 ctxt |
|
59 |> snd o Local_Theory.note |
|
60 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), [rsp_thm]) |
|
61 |> snd o Local_Theory.note ((bind, []), [user_thm]) |
|
62 end |
|
63 *} |
|
64 |
|
65 ML {* |
|
66 fun fv_rsp_tac induct fv_simps = |
|
67 eresolve_tac induct THEN_ALL_NEW |
|
68 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fv_simps)) |
|
69 *} |
|
70 |
|
71 ML {* |
|
72 fun constr_rsp_tac inj rsp equivps = |
|
73 let |
|
74 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
|
75 in |
|
76 REPEAT o rtac @{thm fun_rel_id} THEN' |
|
77 simp_tac (HOL_ss addsimps inj) THEN' |
|
78 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
|
79 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
|
80 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
81 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
|
82 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
83 )) |
|
84 end |
|
85 *} |
|
86 |
|
87 |
|
88 end |