47325
|
1 |
(* Title: HOL/Tools/transfer.ML
|
|
2 |
Author: Brian Huffman, TU Muenchen
|
|
3 |
|
|
4 |
Generic theorem transfer method.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature TRANSFER =
|
|
8 |
sig
|
|
9 |
val fo_conv: Proof.context -> conv
|
|
10 |
val prep_conv: conv
|
|
11 |
val transfer_add: attribute
|
|
12 |
val transfer_del: attribute
|
|
13 |
val transfer_tac: Proof.context -> int -> tactic
|
|
14 |
val correspondence_tac: Proof.context -> int -> tactic
|
|
15 |
val setup: theory -> theory
|
|
16 |
end
|
|
17 |
|
|
18 |
structure Transfer : TRANSFER =
|
|
19 |
struct
|
|
20 |
|
|
21 |
structure Data = Named_Thms
|
|
22 |
(
|
|
23 |
val name = @{binding transfer_raw}
|
|
24 |
val description = "raw correspondence rule for transfer method"
|
|
25 |
)
|
|
26 |
|
|
27 |
(** Conversions **)
|
|
28 |
|
|
29 |
val App_rule = Thm.symmetric @{thm App_def}
|
|
30 |
val Abs_rule = Thm.symmetric @{thm Abs_def}
|
|
31 |
val Rel_rule = Thm.symmetric @{thm Rel_def}
|
|
32 |
|
|
33 |
fun dest_funcT cT =
|
|
34 |
(case Thm.dest_ctyp cT of [T, U] => (T, U)
|
|
35 |
| _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
|
|
36 |
|
|
37 |
fun App_conv ct =
|
|
38 |
let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
|
|
39 |
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end
|
|
40 |
|
|
41 |
fun Abs_conv ct =
|
|
42 |
let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
|
|
43 |
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end
|
|
44 |
|
|
45 |
fun Rel_conv ct =
|
|
46 |
let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
|
|
47 |
val (cU, _) = dest_funcT cT'
|
|
48 |
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
|
|
49 |
|
|
50 |
fun Trueprop_conv cv ct =
|
|
51 |
(case Thm.term_of ct of
|
|
52 |
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
|
|
53 |
| _ => raise CTERM ("Trueprop_conv", [ct]))
|
|
54 |
|
|
55 |
(* Conversion to insert tags on every application and abstraction. *)
|
|
56 |
fun fo_conv ctxt ct = (
|
|
57 |
Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt)
|
|
58 |
else_conv
|
|
59 |
Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv
|
|
60 |
else_conv
|
|
61 |
Conv.all_conv) ct
|
|
62 |
|
|
63 |
(* Conversion to preprocess a correspondence rule *)
|
|
64 |
fun prep_conv ct = (
|
|
65 |
Conv.implies_conv Conv.all_conv prep_conv
|
|
66 |
else_conv
|
|
67 |
Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
|
|
68 |
else_conv
|
|
69 |
Conv.all_conv) ct
|
|
70 |
|
|
71 |
(* Conversion to prep a proof goal containing a correspondence rule *)
|
|
72 |
fun correspond_conv ctxt ct = (
|
|
73 |
Conv.forall_conv (correspond_conv o snd) ctxt
|
|
74 |
else_conv
|
|
75 |
Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
|
|
76 |
else_conv
|
|
77 |
Trueprop_conv
|
|
78 |
(Conv.combination_conv
|
|
79 |
(Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt))
|
|
80 |
else_conv
|
|
81 |
Conv.all_conv) ct
|
|
82 |
|
|
83 |
|
|
84 |
(** Transfer proof method **)
|
|
85 |
|
|
86 |
fun bnames (t $ u) = bnames t @ bnames u
|
|
87 |
| bnames (Abs (x,_,t)) = x :: bnames t
|
|
88 |
| bnames _ = []
|
|
89 |
|
|
90 |
fun rename [] t = (t, [])
|
|
91 |
| rename (x::xs) ((c as Const (@{const_name Abs}, _)) $ Abs (_, T, t)) =
|
|
92 |
let val (t', xs') = rename xs t
|
|
93 |
in (c $ Abs (x, T, t'), xs') end
|
|
94 |
| rename xs0 (t $ u) =
|
|
95 |
let val (t', xs1) = rename xs0 t
|
|
96 |
val (u', xs2) = rename xs1 u
|
|
97 |
in (t' $ u', xs2) end
|
|
98 |
| rename xs t = (t, xs)
|
|
99 |
|
|
100 |
fun cert ctxt t = cterm_of (Proof_Context.theory_of ctxt) t
|
|
101 |
|
|
102 |
fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
|
|
103 |
|
|
104 |
(* Tactic to correspond a value to itself *)
|
|
105 |
fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
|
|
106 |
let
|
|
107 |
val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
|
|
108 |
val cT = ctyp_of (Proof_Context.theory_of ctxt) T
|
|
109 |
val rews = [@{thm fun_rel_eq [symmetric, THEN eq_reflection]}]
|
|
110 |
val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
|
|
111 |
val thm2 = Raw_Simplifier.rewrite_rule rews thm1
|
|
112 |
in
|
|
113 |
rtac thm2 i
|
|
114 |
end handle Match => no_tac | TERM _ => no_tac)
|
|
115 |
|
|
116 |
fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
|
|
117 |
let
|
|
118 |
val bs = bnames t
|
|
119 |
val rules = Data.get ctxt
|
|
120 |
in
|
|
121 |
EVERY
|
|
122 |
[rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
|
|
123 |
CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
|
|
124 |
rtac @{thm transfer_start [rotated]} i,
|
|
125 |
REPEAT_ALL_NEW (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i + 1),
|
|
126 |
(* Alpha-rename bound variables in goal *)
|
|
127 |
SUBGOAL (fn (u, i) =>
|
|
128 |
rtac @{thm equal_elim_rule1} i THEN
|
|
129 |
rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i,
|
|
130 |
(* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
|
|
131 |
rewrite_goal_tac @{thms App_def Abs_def} i,
|
|
132 |
rewrite_goal_tac @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric]} i,
|
|
133 |
rtac @{thm _} i]
|
|
134 |
end)
|
|
135 |
|
|
136 |
fun correspondence_tac ctxt i =
|
|
137 |
let
|
|
138 |
val rules = Data.get ctxt
|
|
139 |
in
|
|
140 |
EVERY
|
|
141 |
[CONVERSION (correspond_conv ctxt) i,
|
|
142 |
REPEAT_ALL_NEW
|
|
143 |
(resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
|
|
144 |
end
|
|
145 |
|
|
146 |
val transfer_method =
|
|
147 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
|
|
148 |
|
|
149 |
val correspondence_method =
|
|
150 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
|
|
151 |
|
|
152 |
(* Attribute for correspondence rules *)
|
|
153 |
|
|
154 |
val prep_rule = Conv.fconv_rule prep_conv
|
|
155 |
|
|
156 |
val transfer_add =
|
|
157 |
Thm.declaration_attribute (Data.add_thm o prep_rule)
|
|
158 |
|
|
159 |
val transfer_del =
|
|
160 |
Thm.declaration_attribute (Data.del_thm o prep_rule)
|
|
161 |
|
|
162 |
val transfer_attribute =
|
|
163 |
Attrib.add_del transfer_add transfer_del
|
|
164 |
|
|
165 |
(* Theory setup *)
|
|
166 |
|
|
167 |
val setup =
|
|
168 |
Data.setup
|
|
169 |
#> Attrib.setup @{binding transfer_rule} transfer_attribute
|
|
170 |
"correspondence rule for transfer method"
|
|
171 |
#> Method.setup @{binding transfer} transfer_method
|
|
172 |
"generic theorem transfer method"
|
|
173 |
#> Method.setup @{binding correspondence} correspondence_method
|
|
174 |
"for proving correspondence rules"
|
|
175 |
|
|
176 |
end
|