author | Christian Urban <urbanc@in.tum.de> |
Thu, 25 Feb 2010 07:48:33 +0100 | |
changeset 1258 | 7d8949da7d99 |
parent 1230 | Quot/Nominal/Rsp.thy@a41c3a105104 |
child 1268 | d1999540d23a |
permissions | -rw-r--r-- |
1227 | 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 {* |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
17 |
fun const_rsp lthy const = |
1227 | 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 |
||
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
26 |
(* Replaces bounds by frees and meta implications by implications *) |
1227 | 27 |
ML {* |
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
28 |
fun prepare_goal trm = |
1227 | 29 |
let |
30 |
val vars = strip_all_vars trm |
|
31 |
val fs = rev (map Free vars) |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
32 |
val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm))) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
33 |
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
34 |
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls) |
1227 | 35 |
in |
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
36 |
(fixes, fold (curry HOLogic.mk_imp) prems concl) |
1227 | 37 |
end |
38 |
*} |
|
39 |
||
40 |
ML {* |
|
41 |
fun get_rsp_goal thy trm = |
|
42 |
let |
|
43 |
val goalstate = Goal.init (cterm_of thy trm); |
|
44 |
val tac = REPEAT o rtac @{thm fun_rel_id}; |
|
45 |
in |
|
46 |
case (SINGLE (tac 1) goalstate) of |
|
47 |
NONE => error "rsp_goal failed" |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
48 |
| SOME th => prepare_goal (term_of (cprem_of th 1)) |
1227 | 49 |
end |
50 |
*} |
|
51 |
||
52 |
ML {* |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
53 |
fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
54 |
*} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
55 |
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
56 |
ML {* |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
57 |
fun prove_const_rsp bind consts tac ctxt = |
1227 | 58 |
let |
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
59 |
val rsp_goals = map (const_rsp ctxt) consts |
1227 | 60 |
val thy = ProofContext.theory_of ctxt |
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
61 |
val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
62 |
val fixed' = distinct (op =) (flat fixed) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
63 |
val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
64 |
val user_thm = Goal.prove ctxt fixed' [] user_goal tac |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
65 |
val user_thms = map repeat_mp (HOLogic.conj_elims user_thm) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
66 |
fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1 |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
67 |
val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals |
1227 | 68 |
in |
69 |
ctxt |
|
70 |
|> snd o Local_Theory.note |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
71 |
((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
72 |
|> snd o Local_Theory.note ((bind, []), user_thms) |
1227 | 73 |
end |
74 |
*} |
|
75 |
||
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
76 |
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
77 |
|
1227 | 78 |
ML {* |
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
79 |
fun fvbv_rsp_tac induct fvbv_simps = |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
80 |
((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
81 |
(TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
82 |
(HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) |
1227 | 83 |
*} |
84 |
||
85 |
ML {* |
|
86 |
fun constr_rsp_tac inj rsp equivps = |
|
87 |
let |
|
88 |
val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
|
89 |
in |
|
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
90 |
REPEAT o rtac impI THEN' |
1227 | 91 |
simp_tac (HOL_ss addsimps inj) THEN' |
92 |
(TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
|
93 |
(asm_simp_tac HOL_ss THEN_ALL_NEW ( |
|
94 |
rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
95 |
asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
|
96 |
@{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
97 |
)) |
|
98 |
end |
|
99 |
*} |
|
100 |
||
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
101 |
(* Testing code |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
102 |
local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
103 |
(fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
104 |
|
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
105 |
(*ML {* |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
106 |
val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
107 |
val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
108 |
val fixed' = distinct (op =) (flat fixed) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
109 |
val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
110 |
*} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
111 |
prove ug: {* user_goal *} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
112 |
ML_prf {* |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
113 |
val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
114 |
val fv_simps = @{thms rbv2.simps} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
115 |
*} |
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1227
diff
changeset
|
116 |
*) |
1227 | 117 |
|
118 |
end |