35 fun get_relator_eq ctxt = |
33 fun get_relator_eq ctxt = |
36 map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt) |
34 map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt) |
37 |
35 |
38 (** Conversions **) |
36 (** Conversions **) |
39 |
37 |
40 val App_rule = Thm.symmetric @{thm App_def} |
|
41 val Abs_rule = Thm.symmetric @{thm Abs_def} |
|
42 val Rel_rule = Thm.symmetric @{thm Rel_def} |
38 val Rel_rule = Thm.symmetric @{thm Rel_def} |
43 |
39 |
44 fun dest_funcT cT = |
40 fun dest_funcT cT = |
45 (case Thm.dest_ctyp cT of [T, U] => (T, U) |
41 (case Thm.dest_ctyp cT of [T, U] => (T, U) |
46 | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) |
42 | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) |
47 |
|
48 fun App_conv ct = |
|
49 let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) |
|
50 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end |
|
51 |
|
52 fun Abs_conv ct = |
|
53 let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) |
|
54 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end |
|
55 |
43 |
56 fun Rel_conv ct = |
44 fun Rel_conv ct = |
57 let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) |
45 let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) |
58 val (cU, _) = dest_funcT cT' |
46 val (cU, _) = dest_funcT cT' |
59 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end |
47 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end |
60 |
48 |
61 fun Trueprop_conv cv ct = |
49 fun Trueprop_conv cv ct = |
62 (case Thm.term_of ct of |
50 (case Thm.term_of ct of |
63 Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
51 Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
64 | _ => raise CTERM ("Trueprop_conv", [ct])) |
52 | _ => raise CTERM ("Trueprop_conv", [ct])) |
65 |
|
66 (* Conversion to insert tags on every application and abstraction. *) |
|
67 fun fo_conv ctxt ct = ( |
|
68 Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt) |
|
69 else_conv |
|
70 Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv |
|
71 else_conv |
|
72 Conv.all_conv) ct |
|
73 |
53 |
74 (* Conversion to preprocess a transfer rule *) |
54 (* Conversion to preprocess a transfer rule *) |
75 fun prep_conv ct = ( |
55 fun prep_conv ct = ( |
76 Conv.implies_conv Conv.all_conv prep_conv |
56 Conv.implies_conv Conv.all_conv prep_conv |
77 else_conv |
57 else_conv |
78 Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) |
58 Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) |
79 else_conv |
59 else_conv |
80 Conv.all_conv) ct |
60 Conv.all_conv) ct |
81 |
61 |
82 (* Conversion to prep a proof goal containing a transfer rule *) |
|
83 fun transfer_goal_conv ctxt ct = ( |
|
84 Conv.forall_conv (transfer_goal_conv o snd) ctxt |
|
85 else_conv |
|
86 Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt) |
|
87 else_conv |
|
88 Trueprop_conv |
|
89 (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt)) |
|
90 else_conv |
|
91 Conv.all_conv) ct |
|
92 |
|
93 |
|
94 (** Transfer proof method **) |
62 (** Transfer proof method **) |
95 |
63 |
96 fun dest_Rel (Const (@{const_name Rel}, _) $ r $ x $ y) = (r, x, y) |
|
97 | dest_Rel t = raise TERM ("dest_Rel", [t]) |
|
98 |
|
99 fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y |
64 fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y |
|
65 | RelT t = raise TERM ("RelT", [t]) |
100 |
66 |
101 (* Tactic to correspond a value to itself *) |
67 (* Tactic to correspond a value to itself *) |
102 fun eq_tac ctxt = SUBGOAL (fn (t, i) => |
68 fun eq_tac ctxt = SUBGOAL (fn (t, i) => |
103 let |
69 let |
104 val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t)) |
70 val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t)) |
109 in |
75 in |
110 rtac thm2 i |
76 rtac thm2 i |
111 end handle Match => no_tac | TERM _ => no_tac) |
77 end handle Match => no_tac | TERM _ => no_tac) |
112 |
78 |
113 val post_simps = |
79 val post_simps = |
114 @{thms App_def Abs_def transfer_forall_eq [symmetric] |
80 @{thms transfer_forall_eq [symmetric] |
115 transfer_implies_eq [symmetric] transfer_bforall_unfold} |
81 transfer_implies_eq [symmetric] transfer_bforall_unfold} |
116 |
82 |
117 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => |
83 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => |
118 let |
84 let |
119 val vs = rev (Term.add_frees t []) |
85 val vs = rev (Term.add_frees t []) |
120 val vs' = filter_out (member (op =) keepers) vs |
86 val vs' = filter_out (member (op =) keepers) vs |
121 in |
87 in |
122 Induct.arbitrary_tac ctxt 0 vs' i |
88 Induct.arbitrary_tac ctxt 0 vs' i |
123 end) |
89 end) |
124 |
90 |
125 (* Apply rule Rel_Abs with appropriate bound variable name *) |
91 (* create a lambda term of the same shape as the given term *) |
126 val abs_tac = SUBGOAL (fn (t, i) => |
92 fun skeleton (Bound i) ctxt = (Bound i, ctxt) |
127 let |
93 | skeleton (Abs (x, _, t)) ctxt = |
128 val pat = (#2 o dest_Rel o HOLogic.dest_Trueprop o Thm.concl_of) @{thm Rel_Abs} |
94 let |
129 val obj = (#3 o dest_Rel o HOLogic.dest_Trueprop o Logic.strip_assums_concl) t |
95 val (t', ctxt) = skeleton t ctxt |
130 val rule = Thm.rename_boundvars pat obj @{thm Rel_Abs} |
96 in |
131 in |
97 (Abs (x, dummyT, t'), ctxt) |
132 rtac rule i |
98 end |
133 end handle TERM _ => no_tac) |
99 | skeleton (t $ u) ctxt = |
134 |
100 let |
135 fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) => |
101 val (t', ctxt) = skeleton t ctxt |
136 let |
102 val (u', ctxt) = skeleton u ctxt |
|
103 in |
|
104 (t' $ u', ctxt) |
|
105 end |
|
106 | skeleton _ ctxt = |
|
107 let |
|
108 val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt |
|
109 in |
|
110 (Free (c, dummyT), ctxt) |
|
111 end |
|
112 |
|
113 fun mk_relT (T, U) = T --> U --> HOLogic.boolT |
|
114 |
|
115 fun mk_Rel t = |
|
116 let val T = fastype_of t |
|
117 in Const (@{const_name Transfer.Rel}, T --> T) $ t end |
|
118 |
|
119 fun transfer_rule_of_terms ctxt tab t u = |
|
120 let |
|
121 val thy = Proof_Context.theory_of ctxt |
|
122 (* precondition: T must consist of only TFrees and function space *) |
|
123 fun rel (T as TFree (a, _)) U = |
|
124 Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) |
|
125 | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = |
|
126 let |
|
127 val r1 = rel T1 U1 |
|
128 val r2 = rel T2 U2 |
|
129 val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U) |
|
130 in |
|
131 Const (@{const_name fun_rel}, rT) $ r1 $ r2 |
|
132 end |
|
133 | rel T U = raise TYPE ("rel", [T, U], []) |
|
134 fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) |
|
135 | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = |
|
136 let |
|
137 val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt |
|
138 val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U) |
|
139 val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) |
|
140 val thm0 = Thm.assume cprop |
|
141 val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u |
|
142 val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop)) |
|
143 val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1)) |
|
144 val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1)) |
|
145 val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2)) |
|
146 val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2] |
|
147 val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)] |
|
148 val rule = Drule.instantiate' tinsts insts @{thm Rel_abs} |
|
149 val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1)) |
|
150 in |
|
151 (thm2 COMP rule, hyps) |
|
152 end |
|
153 | zip ctxt thms (f $ t) (g $ u) = |
|
154 let |
|
155 val (thm1, hyps1) = zip ctxt thms f g |
|
156 val (thm2, hyps2) = zip ctxt thms t u |
|
157 in |
|
158 (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) |
|
159 end |
|
160 | zip _ _ (t as Free (_, T)) u = |
|
161 let |
|
162 val U = fastype_of u |
|
163 val prop = mk_Rel (rel T U) $ t $ u |
|
164 val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) |
|
165 in |
|
166 (Thm.assume cprop, [cprop]) |
|
167 end |
|
168 | zip _ _ t u = raise TERM ("zip_relterm", [t, u]) |
|
169 val r = mk_Rel (rel (fastype_of t) (fastype_of u)) |
|
170 val goal = HOLogic.mk_Trueprop (r $ t $ u) |
|
171 val rename = Thm.trivial (cterm_of thy goal) |
|
172 val (thm, hyps) = zip ctxt [] t u |
|
173 in |
|
174 Drule.implies_intr_list hyps (thm RS rename) |
|
175 end |
|
176 |
|
177 fun transfer_rule_of_term ctxt t = |
|
178 let |
|
179 val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |> |
|
180 map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS))) |
|
181 val frees = map fst (Term.add_frees s []) |
|
182 val tfrees = map fst (Term.add_tfrees s []) |
|
183 fun prep a = "R" ^ Library.unprefix "'" a |
|
184 val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt |
|
185 val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t |
|
186 in |
|
187 Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm |
|
188 end |
|
189 |
|
190 fun transfer_tac equiv ctxt i = |
|
191 let |
|
192 val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} |
|
193 val start_rule = |
|
194 if equiv then @{thm transfer_start} else @{thm transfer_start'} |
137 val rules = Data.get ctxt |
195 val rules = Data.get ctxt |
138 val app_tac = rtac @{thm Rel_App} |
|
139 val start_rule = |
|
140 if equiv then @{thm transfer_start} else @{thm transfer_start'} |
|
141 in |
196 in |
142 EVERY |
197 EVERY |
143 [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i, |
198 [rewrite_goal_tac pre_simps i THEN |
144 CONVERSION (Trueprop_conv (fo_conv ctxt)) i, |
199 SUBGOAL (fn (t, i) => |
145 rtac start_rule i, |
200 rtac start_rule i THEN |
146 SOLVED' (REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac |
201 (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) |
147 ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) |
202 THEN_ALL_NEW |
148 ORELSE' eq_tac ctxt)) (i + 1), |
203 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) |
|
204 ORELSE' eq_tac ctxt)) (i + 1)) i, |
149 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) |
205 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) |
150 rewrite_goal_tac post_simps i, |
206 rewrite_goal_tac post_simps i, |
151 rtac @{thm _} i] |
207 rtac @{thm _} i] |
|
208 end |
|
209 |
|
210 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => |
|
211 let |
|
212 val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t |
|
213 val rule1 = transfer_rule_of_term ctxt rhs |
|
214 val rules = Data.get ctxt |
|
215 in |
|
216 EVERY |
|
217 [CONVERSION prep_conv i, |
|
218 rtac @{thm transfer_prover_start} i, |
|
219 (rtac rule1 THEN_ALL_NEW |
|
220 REPEAT_ALL_NEW |
|
221 (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1), |
|
222 rtac @{thm refl} i] |
152 end) |
223 end) |
153 |
224 |
154 fun transfer_prover_tac ctxt i = |
225 (** Methods and attributes **) |
155 let |
|
156 val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt |
|
157 in |
|
158 EVERY |
|
159 [CONVERSION (transfer_goal_conv ctxt) i, |
|
160 rtac @{thm transfer_prover_start} i, |
|
161 REPEAT_ALL_NEW |
|
162 (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1), |
|
163 rewrite_goal_tac @{thms App_def Abs_def} i, |
|
164 rtac @{thm refl} i] |
|
165 end |
|
166 |
226 |
167 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
227 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
168 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) |
228 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) |
169 |
229 |
170 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |
230 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |