|
1 theory LetElim |
|
2 imports Main Data_slot |
|
3 begin |
|
4 |
|
5 ML {* |
|
6 val _ = print_depth 100 |
|
7 *} |
|
8 |
|
9 ML {* |
|
10 val trace_elim = Attrib.setup_config_bool @{binding trace_elim} (K false) |
|
11 *} |
|
12 |
|
13 ML {* (* aux functions *) |
|
14 val tracing = (fn ctxt => fn str => |
|
15 if (Config.get ctxt trace_elim) then tracing str else ()) |
|
16 |
|
17 val empty_env = (Vartab.empty, Vartab.empty) |
|
18 |
|
19 fun match_env ctxt pat trm env = |
|
20 Pattern.match (ctxt |> Proof_Context.theory_of) (pat, trm) env |
|
21 |
|
22 fun match ctxt pat trm = match_env ctxt pat trm empty_env; |
|
23 |
|
24 val inst = Envir.subst_term; |
|
25 |
|
26 fun term_of_thm thm = thm |> prop_of |> HOLogic.dest_Trueprop |
|
27 |
|
28 fun last [a] = a | |
|
29 last (a::b) = last b |
|
30 |
|
31 fun but_last [a] = [] | |
|
32 but_last (a::b) = a::(but_last b) |
|
33 |
|
34 fun foldr f [] = (fn x => x) | |
|
35 foldr f (x :: xs) = (f x) o (foldr f xs) |
|
36 |
|
37 fun concat [] = [] | |
|
38 concat (x :: xs) = x @ concat xs |
|
39 |
|
40 fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of |
|
41 fun string_of_cterm ctxt ct = ct |> term_of |> string_of_term ctxt |
|
42 fun pterm ctxt t = |
|
43 t |> string_of_term ctxt |> tracing ctxt |
|
44 fun pcterm ctxt ct = ct |> string_of_cterm ctxt |> tracing ctxt |
|
45 fun pthm ctxt thm = thm |> prop_of |> pterm ctxt |
|
46 fun string_for_term ctxt t = |
|
47 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
|
48 (print_mode_value ())) (Syntax.string_of_term ctxt) t |
|
49 |> String.translate (fn c => if Char.isPrint c then str c else "") |
|
50 |> Sledgehammer_Util.simplify_spaces |
|
51 fun string_for_cterm ctxt ct = ct |> term_of |> string_for_term ctxt |
|
52 fun attemp tac = fn i => fn st => (tac i st) handle exn => Seq.empty |
|
53 fun try_tac tac = fn i => fn st => (tac i st) handle exn => (Seq.single st) |
|
54 fun ctxt_show ctxt = ctxt |> Config.put Proof_Context.verbose true |> |
|
55 Config.put Proof_Context.debug true |> |
|
56 Config.put Display.show_hyps true |> |
|
57 Config.put Display.show_tags true |
|
58 fun swf f = (fn x => fn y => f y x) |
|
59 *} (* aux end *) |
|
60 |
|
61 ML {* |
|
62 fun close_form_over vars trm = |
|
63 fold Logic.all (map Free vars) trm |
|
64 fun try_star f g = (try_star f (g |> f)) handle _ => g |
|
65 |
|
66 fun bind_judgment ctxt name = |
|
67 let |
|
68 val thy = Proof_Context.theory_of ctxt; |
|
69 val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt; |
|
70 val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x; |
|
71 in ((v, t), ctxt') end; |
|
72 |
|
73 fun let_trm_of ctxt mjp = let |
|
74 fun is_let_trm (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = true |
|
75 | is_let_trm _ = false |
|
76 in |
|
77 ZipperSearch.all_td_lr (mjp |> Zipper.mktop) |
|
78 |> Seq.filter (fn z => is_let_trm (Zipper.trm z)) |
|
79 |> Seq.hd |> Zipper.trm |
|
80 end |
|
81 |
|
82 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME |
|
83 | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body) |
|
84 | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u) |
|
85 | decr _ _ = raise Same.SAME |
|
86 and decrh lev t = (decr lev t handle Same.SAME => t); |
|
87 |
|
88 (* A new version of [result], copied from [obtain.ML] *) |
|
89 fun eliminate_term ctxt xs tm = |
|
90 let |
|
91 val vs = map (dest_Free o Thm.term_of) xs; |
|
92 val bads = Term.fold_aterms (fn t as Free v => |
|
93 if member (op =) vs v then insert (op aconv) t else I | _ => I) tm []; |
|
94 val _ = null bads orelse |
|
95 error ("Result contains obtained parameters: " ^ |
|
96 space_implode " " (map (Syntax.string_of_term ctxt) bads)); |
|
97 in tm end; |
|
98 |
|
99 fun eliminate fix_ctxt rule xs As thm = |
|
100 let |
|
101 val thy = Proof_Context.theory_of fix_ctxt; |
|
102 |
|
103 val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm); |
|
104 val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse |
|
105 error "Conclusion in obtained context must be object-logic judgment"; |
|
106 |
|
107 val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt; |
|
108 val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm')); |
|
109 in |
|
110 ((Drule.implies_elim_list thm' (map Thm.assume prems) |
|
111 |> Drule.implies_intr_list (map Drule.norm_hhf_cterm As) |
|
112 |> Drule.forall_intr_list xs) |
|
113 COMP rule) |
|
114 |> Drule.implies_intr_list prems |
|
115 |> singleton (Variable.export ctxt' fix_ctxt) |
|
116 end; |
|
117 |
|
118 fun obtain_export ctxt rule xs _ As = |
|
119 (eliminate ctxt rule xs As, eliminate_term ctxt xs); |
|
120 |
|
121 fun check_result ctxt thesis th = |
|
122 (case Thm.prems_of th of |
|
123 [prem] => |
|
124 if Thm.concl_of th aconv thesis andalso |
|
125 Logic.strip_assums_concl prem aconv thesis then th |
|
126 else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th) |
|
127 | [] => error "Goal solved -- nothing guessed" |
|
128 | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th)); |
|
129 |
|
130 fun result tac facts ctxt = |
|
131 let |
|
132 val thy = Proof_Context.theory_of ctxt; |
|
133 val cert = Thm.cterm_of thy; |
|
134 |
|
135 val ([thesisN], _) = Variable.variant_fixes [Auto_Bind.thesisN] ctxt |
|
136 |
|
137 val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt thesisN; |
|
138 val rule = |
|
139 (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of |
|
140 NONE => raise THM ("Obtain.result: tactic failed", 0, facts) |
|
141 | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th))); |
|
142 |
|
143 val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; |
|
144 val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; |
|
145 val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; |
|
146 val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt'; |
|
147 val (prems, ctxt'') = |
|
148 Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) |
|
149 (Drule.strip_imp_prems stmt) fix_ctxt; |
|
150 in ((params, prems), ctxt'') end; |
|
151 *} |
|
152 |
|
153 ML {* |
|
154 local |
|
155 fun let_lhs ctxt vars let_rest = |
|
156 case let_rest of |
|
157 Const (@{const_name prod_case}, _) $ let_rest => |
|
158 let |
|
159 val (exp1, rest1) = let_lhs ctxt vars let_rest |
|
160 val vars = Term.add_frees exp1 vars |
|
161 val (exp2, rest2) = let_lhs ctxt vars rest1 |
|
162 in ((Const (@{const_name Pair}, dummyT) $ exp1 $ exp2), rest2) end |
|
163 | Abs (var, var_typ, rest) => let |
|
164 val (vars', _) = Variable.variant_fixes ((map fst vars)@[var]) ctxt |
|
165 val (_, var') = vars' |> split_last |
|
166 val [(var, var_typ)] = Variable.variant_frees ctxt (map Free vars) [(var, var_typ)] in |
|
167 (Free (var', var_typ), rest) end |
|
168 |
|
169 fun sg_lhs_f ctxt (vars, eqns, let_trm) = let |
|
170 val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm |
|
171 val let_rest = case let_rest of |
|
172 Abs ("", _, let_rest$Bound 0) => decrh 0 let_rest |
|
173 | _ => let_rest |
|
174 val (lhs, let_trm) = let_rest |> let_lhs ctxt vars |
|
175 val lhs = lhs|> Syntax.check_term ctxt |
|
176 val let_expr = let_expr |> Syntax.check_term ctxt |
|
177 val eqn = HOLogic.mk_eq (lhs, let_expr) |> Syntax.check_term ctxt |
|
178 val eqns = (eqn::eqns) |
|
179 val vars = Term.add_frees lhs vars |
|
180 val let_trm = Term.subst_bounds ((map Free vars), let_trm) |
|
181 in (vars, eqns, let_trm) end |
|
182 fun dest_let ctxt let_trm = let |
|
183 val (vars, eqns, lrest) = try_star (sg_lhs_f ctxt) ([], [], let_trm) |
|
184 in (vars, eqns, lrest) end |
|
185 |
|
186 in |
|
187 |
|
188 fun let_elim_rule ctxt mjp = let |
|
189 val ctxt = ctxt |> Variable.set_body false |
|
190 val thy = Proof_Context.theory_of ctxt |
|
191 val cterm = cterm_of thy |
|
192 val tracing = tracing ctxt |
|
193 val pthm = pthm ctxt |
|
194 val pterm = pterm ctxt |
|
195 val pcterm = pcterm ctxt |
|
196 |
|
197 val let_trm = let_trm_of ctxt mjp |
|
198 val ([pname], _) = Variable.variant_fixes ["P"] ctxt |
|
199 val P = Free (pname, dummyT) |
|
200 val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm)) |
|
201 |> Syntax.check_term ctxt |
|
202 val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp |
|
203 val (vars, eqns, lrest) = dest_let ctxt let_trm |
|
204 |
|
205 val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt |
|
206 val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop |
|
207 val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop) |
|
208 val that_prems = (P $ lrest) :: (rev eqns) |> map (HOLogic.mk_Trueprop) |
|
209 val that_prop = Logic.list_implies (that_prems, thesis_p) |
|
210 val that_prop = close_form_over vars that_prop |
|
211 fun exists_on_lhs eq = let |
|
212 val (lhs, rhs) = eq |> HOLogic.dest_eq |
|
213 fun exists_on vars trm = let |
|
214 fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm) |
|
215 in fold sg_exists_on vars trm end |
|
216 in exists_on (Term.add_frees lhs []) eq end |
|
217 fun prove_eqn ctxt0 eqn = let |
|
218 val (lhs, let_expr) = eqn |> HOLogic.dest_eq |
|
219 val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop |
|
220 fun case_rule_of ctxt let_expr = let |
|
221 val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd |
|
222 val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of |
|
223 |> Induct.vars_of |> hd |> cterm |
|
224 val mt = Thm.match (case_var, let_expr |> cterm) |
|
225 val case_rule = Thm.instantiate mt case_rule |
|
226 in case_rule end |
|
227 val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE |
|
228 val my_case_tac = case case_rule of |
|
229 SOME case_rule => (rtac case_rule 1) |
|
230 | _ => all_tac |
|
231 val eq_e = Goal.prove ctxt0 [] [] eq_e_prop |
|
232 (K (my_case_tac THEN (auto_tac ctxt0))) |
|
233 in eq_e end |
|
234 val peqns = eqns |> map (prove_eqn ctxt) |
|
235 fun add_result thm (facts, ctxt) = let |
|
236 val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt) |
|
237 in (fact::facts, ctxt1) end |
|
238 val add_results = fold add_result |
|
239 val (facts, ctxt1) = add_results (rev peqns) ([], ctxt) |
|
240 (* val facts = rev facts *) |
|
241 val ([mjp_p, that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [mjp, that_prop]) |
|
242 val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts |
|
243 fun rsn eq that_p = eq RSN (2, that_p) |
|
244 val rule1 = fold rsn (rev facts) that_p |
|
245 val tac = (Method.insert_tac ([mjp_p]@sym_facts) 1) THEN (auto_tac ctxt2) |
|
246 val next_pp = Goal.prove ctxt [] [] next_p (K tac) |
|
247 val result = next_pp RS rule1 |
|
248 val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) |
|
249 [mjp, thesis_p] ctxt2 |
|
250 val [let_elim_rule] = Proof_Context.export ctxt3 ctxt [result] |
|
251 in let_elim_rule end |
|
252 |
|
253 fun let_intro_rule ctxt mjp = let |
|
254 val ctxt = ctxt |> Variable.set_body false |
|
255 val thy = Proof_Context.theory_of ctxt |
|
256 val cterm = cterm_of thy |
|
257 val tracing = tracing ctxt |
|
258 val pthm = pthm ctxt |
|
259 val pterm = pterm ctxt |
|
260 val pcterm = pcterm ctxt |
|
261 |
|
262 val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt |
|
263 val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop |
|
264 val let_trm = let_trm_of ctxt mjp |
|
265 val ([pname], _) = Variable.variant_fixes ["P"] ctxt |
|
266 val P = Free (pname, dummyT) |
|
267 val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm)) |
|
268 |> Syntax.check_term ctxt |
|
269 val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp |
|
270 val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm |
|
271 val (vars, eqns, lrest) = dest_let ctxt let_trm |
|
272 |
|
273 val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop) |
|
274 val that_prems = (rev eqns) |> map (HOLogic.mk_Trueprop) |
|
275 val that_prop = Logic.list_implies (that_prems, next_p) |
|
276 val that_prop = close_form_over vars that_prop |> Syntax.check_term ctxt |
|
277 fun exists_on_lhs eq = let |
|
278 val (lhs, rhs) = eq |> HOLogic.dest_eq |
|
279 fun exists_on vars trm = let |
|
280 fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm) |
|
281 in fold sg_exists_on vars trm end |
|
282 in exists_on (Term.add_frees lhs []) eq end |
|
283 fun prove_eqn ctxt0 eqn = let |
|
284 val (lhs, let_expr) = eqn |> HOLogic.dest_eq |
|
285 val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop |
|
286 fun case_rule_of ctxt let_expr = let |
|
287 val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd |
|
288 val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of |
|
289 |> Induct.vars_of |> hd |> cterm |
|
290 val mt = Thm.match (case_var, let_expr |> cterm) |
|
291 val case_rule = Thm.instantiate mt case_rule |
|
292 in case_rule end |
|
293 val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE |
|
294 val my_case_tac = case case_rule of |
|
295 SOME case_rule => (rtac case_rule 1) |
|
296 | _ => all_tac |
|
297 val eq_e = Goal.prove ctxt0 [] [] eq_e_prop |
|
298 (K (my_case_tac THEN (auto_tac ctxt0))) |
|
299 in eq_e end |
|
300 val peqns = eqns |> map (prove_eqn ctxt) |
|
301 fun add_result thm (facts, ctxt) = let |
|
302 val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt) |
|
303 in (fact::facts, ctxt1) end |
|
304 val add_results = fold add_result |
|
305 val (facts, ctxt1) = add_results (rev peqns) ([], ctxt) |
|
306 val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts |
|
307 val ([that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [that_prop]) |
|
308 fun rsn eq that_p = eq RSN (1, that_p) |
|
309 val rule1 = fold rsn (rev facts) that_p |
|
310 val tac = (Method.insert_tac (rule1::sym_facts) 1) THEN (auto_tac ctxt2) |
|
311 val result = Goal.prove ctxt [] [] mjp (K tac) |
|
312 val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) |
|
313 [mjp, thesis_p] ctxt2 |
|
314 val [let_intro_rule] = Proof_Context.export ctxt3 ctxt [result] |
|
315 in let_intro_rule end |
|
316 |
|
317 end |
|
318 *} |
|
319 |
|
320 ML {* |
|
321 fun let_elim_tac ctxt i st = let |
|
322 val thy = Proof_Context.theory_of ctxt |
|
323 val cterm = cterm_of thy |
|
324 val goal = nth (Thm.prems_of st) (i - 1) |> cterm |
|
325 val mjp = goal |> Drule.strip_imp_prems |> swf nth 0 |> term_of |
|
326 val rule = let_elim_rule ctxt mjp |
|
327 val tac = (etac rule i st) |
|
328 in tac end |
|
329 *} |
|
330 |
|
331 ML {* |
|
332 local |
|
333 val case_names_tagN = "case_names"; |
|
334 |
|
335 val implode_args = space_implode ";"; |
|
336 val explode_args = space_explode ";"; |
|
337 |
|
338 fun add_case_names NONE = I |
|
339 | add_case_names (SOME names) = |
|
340 Thm.untag_rule case_names_tagN |
|
341 #> Thm.tag_rule (case_names_tagN, implode_args names); |
|
342 in |
|
343 fun let_elim_cases_tac ctxt facts = let |
|
344 val tracing = tracing ctxt |
|
345 val pthm = pthm ctxt |
|
346 val pterm = pterm ctxt |
|
347 val pcterm = pcterm ctxt |
|
348 val mjp = facts |> swf nth 0 |> prop_of |
|
349 val _ = tracing "let_elim_cases_tac: elim rule derived is:" |
|
350 val rule = (let_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1) |
|
351 |> add_case_names (SOME ["LetE"]) |
|
352 val _ = rule |> pthm |
|
353 in |
|
354 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts |
|
355 end |
|
356 end |
|
357 *} |
|
358 |
|
359 ML {* |
|
360 val ctxt = @{context} |
|
361 val thy = Proof_Context.theory_of ctxt |
|
362 val cterm = cterm_of thy |
|
363 val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 |
|
364 in f w x1 y1 u)"} |
|
365 *} |
|
366 |
|
367 ML {* |
|
368 val mjp1 = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = e2 in (w +x1 *y1 +u))"} |
|
369 val mjp2 = @{prop "P (let ((x, y), (z, u)) = e; (u, v) = e1 in |
|
370 (case u of (Some t) \<Rightarrow> f t x y z | |
|
371 None \<Rightarrow> g x y z))"} |
|
372 val mjp3 = @{prop "P (let x = e1; ((x1, y1), u) = e2 in f x w x1 y1 u)"} |
|
373 val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 |
|
374 in f w x1 y1 u)"} |
|
375 val mjps = [mjp1, mjp2, mjp3, mjp] |
|
376 val t = mjps |> map (let_elim_rule ctxt) |
|
377 val t2 = mjps |> map (let_intro_rule ctxt) |
|
378 *} |
|
379 |
|
380 ML {* |
|
381 val let_elim_setup = |
|
382 Method.setup @{binding let_elim} |
|
383 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
384 (fn no_simp => fn ctxt => |
|
385 METHOD_CASES (fn facts => (HEADGOAL |
|
386 (let_elim_cases_tac ctxt facts))))) |
|
387 "elimination of prems containing lets "; |
|
388 *} |
|
389 |
|
390 setup {* let_elim_setup *} |
|
391 |
|
392 ML {* |
|
393 val ctxt = @{context} |
|
394 val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1 |
|
395 in f w x1 y1 u)"} |
|
396 *} |
|
397 |
|
398 ML {* |
|
399 fun focus_params t ctxt = |
|
400 let |
|
401 val (xs, Ts) = |
|
402 split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :-*) |
|
403 (* val (xs', ctxt') = variant_fixes xs ctxt; *) |
|
404 (* val ps = xs' ~~ Ts; *) |
|
405 val ps = xs ~~ Ts |
|
406 val (_, ctxt'') = ctxt |> Variable.add_fixes xs |
|
407 in ((xs, ps), ctxt'') end |
|
408 |
|
409 fun focus_concl ctxt t = |
|
410 let |
|
411 val ((xs, ps), ctxt') = focus_params t ctxt |
|
412 val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); |
|
413 in (t' |> Logic.strip_imp_concl, ctxt') end |
|
414 *} |
|
415 |
|
416 ML {* |
|
417 local |
|
418 val case_names_tagN = "case_names"; |
|
419 |
|
420 val implode_args = space_implode ";"; |
|
421 val explode_args = space_explode ";"; |
|
422 |
|
423 fun add_case_names NONE = I |
|
424 | add_case_names (SOME names) = |
|
425 Thm.untag_rule case_names_tagN |
|
426 #> Thm.tag_rule (case_names_tagN, implode_args names); |
|
427 |
|
428 in |
|
429 fun let_intro_cases_tac ctxt facts i st = let |
|
430 val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt |
|
431 val rule = (let_intro_rule ctxt mjp) |> add_case_names (SOME ["LetI"]) |
|
432 in |
|
433 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st |
|
434 end |
|
435 end |
|
436 *} |
|
437 |
|
438 ML {* |
|
439 val let_intro_setup = |
|
440 Method.setup @{binding let_intro} |
|
441 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
442 (fn no_simp => fn ctxt => |
|
443 METHOD_CASES (fn facts => (HEADGOAL |
|
444 (let_intro_cases_tac ctxt facts))))) |
|
445 "introduction rule for goals containing lets "; |
|
446 *} |
|
447 |
|
448 setup {* let_intro_setup *} |
|
449 |
|
450 lemma assumes "Q xxx" "W uuuu" |
|
451 shows "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1 |
|
452 in f w x1 y1 u) = www" |
|
453 using assms |
|
454 proof(let_intro) |
|
455 case (LetI x y w ww x1 y1 u x2 y2) |
|
456 thus ?case |
|
457 oops |
|
458 |
|
459 lemma |
|
460 assumes "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1 |
|
461 in f w x1 y1 u)" |
|
462 and "Q xxx" "W uuuu" |
|
463 shows "thesis" using assms |
|
464 proof(let_elim) |
|
465 case (LetE x y w ww x1 y1 u x2 y2) |
|
466 thus ?case |
|
467 oops |
|
468 |
|
469 |
|
470 ML {* |
|
471 val mjp = @{prop "P ( case (u@v) of |
|
472 Nil \<Rightarrow> f u v |
|
473 | x#xs \<Rightarrow> g u v x xs |
|
474 )"} |
|
475 val mjp1 = @{term "( case (h u v) of |
|
476 None \<Rightarrow> g u v x |
|
477 | Some x \<Rightarrow> (case v of |
|
478 Nil \<Rightarrow> f u v | |
|
479 x#xs \<Rightarrow> h x xs |
|
480 ) |
|
481 )"} |
|
482 *} |
|
483 |
|
484 |
|
485 ML {* |
|
486 fun case_trm_of ctxt mjp = |
|
487 ZipperSearch.all_td_lr (mjp |> Zipper.mktop) |
|
488 |> Seq.filter (fn z => ((Case_Translation.strip_case ctxt true (Zipper.trm z)) <> NONE)) |
|
489 |> Seq.hd |> Zipper.trm |
|
490 *} |
|
491 |
|
492 ML {* |
|
493 fun case_elim_rule ctxt mjp = let |
|
494 val ctxt = ctxt |> Variable.set_body false |
|
495 val thy = Proof_Context.theory_of ctxt; |
|
496 val cterm = cterm_of thy |
|
497 val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt |
|
498 val ((_, thesis_p), _) = bind_judgment ctxt thesisN |
|
499 val case_trm = case_trm_of ctxt mjp |
|
500 val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the |
|
501 val ([pname], _) = Variable.variant_fixes ["P"] ctxt |
|
502 val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool}) |
|
503 val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop |
|
504 val ctxt0 = Proof_Context.init_global thy |
|
505 val thats = case_eqns |> map (fn (lhs, rhs) => let |
|
506 val vars = Term.add_frees lhs [] |
|
507 in |
|
508 Logic.list_implies ([(P$rhs)|>HOLogic.mk_Trueprop, |
|
509 HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop], thesis_p) |> |
|
510 close_form_over vars |
|
511 end) |> |
|
512 map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |> |
|
513 map (Syntax.check_term ctxt0) |
|
514 val (mjp_p::that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (mjp_p::thats)) |
|
515 fun case_rule_of ctxt let_expr = let |
|
516 val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd |
|
517 val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of |
|
518 |> Induct.vars_of |> hd |> cterm |
|
519 val mt = Thm.match (case_var, let_expr |> cterm) |
|
520 val case_rule = Thm.instantiate mt case_rule |
|
521 in case_rule end |
|
522 val case_rule = case_rule_of ctxt case_expr |
|
523 val my_case_tac = (rtac case_rule) |
|
524 val my_tac = ((Method.insert_tac (mjp_p::that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1 |
|
525 val result = Goal.prove ctxt1 [] [] thesis_p (K my_tac) |
|
526 val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) |
|
527 [P, thesis_p, mjp] ctxt1 |
|
528 val [case_elim_rule] = Proof_Context.export ctxt2 ctxt [result] |
|
529 val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd |
|
530 fun get_case_names rule = |
|
531 AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the |
|
532 fun put_case_names names rule = |
|
533 Thm.tag_rule ("case_names", names) rule |
|
534 val case_elim_rule = put_case_names (get_case_names ocase_rule) case_elim_rule |
|
535 in case_elim_rule end |
|
536 *} |
|
537 |
|
538 ML {* |
|
539 fun case_elim_cases_tac ctxt facts = let |
|
540 val mjp = facts |> swf nth 0 |> prop_of |
|
541 val rule = (case_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1) |
|
542 in |
|
543 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts |
|
544 end |
|
545 *} |
|
546 |
|
547 |
|
548 ML {* |
|
549 val case_elim_setup = |
|
550 Method.setup @{binding case_elim} |
|
551 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
552 (fn no_simp => fn ctxt => |
|
553 METHOD_CASES (fn facts => (HEADGOAL |
|
554 (case_elim_cases_tac ctxt facts))))) |
|
555 "elimination of prems containing case "; |
|
556 *} |
|
557 |
|
558 setup {* case_elim_setup *} |
|
559 |
|
560 lemma assumes |
|
561 "P (case h u v of None \<Rightarrow> g u v x | Some x \<Rightarrow> case v of [] \<Rightarrow> f u v | x # xs \<Rightarrow> h x xs)" |
|
562 "GG u v" "PP w x" |
|
563 shows "thesis" using assms |
|
564 proof(case_elim) (* ccc *) |
|
565 case None |
|
566 thus ?case oops |
|
567 (* |
|
568 next |
|
569 case (Some x) |
|
570 thus ?case |
|
571 proof(case_elim) |
|
572 case Nil |
|
573 thus ?case sorry |
|
574 next |
|
575 case (Cons y ys) |
|
576 thus ?case sorry |
|
577 qed |
|
578 qed |
|
579 *) |
|
580 |
|
581 ML {* |
|
582 fun case_intro_rule ctxt mjp = let |
|
583 val ctxt = ctxt |> Variable.set_body false |
|
584 val tracing = tracing ctxt |
|
585 val pthm = pthm ctxt |
|
586 val pterm = pterm ctxt |
|
587 val pcterm = pcterm ctxt |
|
588 val thy = Proof_Context.theory_of ctxt |
|
589 val cterm = cterm_of thy |
|
590 val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt |
|
591 val ((_, thesis_p), _) = bind_judgment ctxt thesisN |
|
592 val case_trm = case_trm_of ctxt mjp |
|
593 val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the |
|
594 val ([pname], _) = Variable.variant_fixes ["P"] ctxt |
|
595 val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool}) |
|
596 val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop |
|
597 val ctxt0 = Proof_Context.init_global thy |
|
598 val thats = case_eqns |> map (fn (lhs, rhs) => let |
|
599 val vars = Term.add_frees lhs [] |
|
600 in |
|
601 Logic.list_implies ([HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop], |
|
602 (P$rhs)|>HOLogic.mk_Trueprop) |> |
|
603 close_form_over vars |
|
604 end) |> |
|
605 map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |> |
|
606 map (Syntax.check_term ctxt0) |
|
607 val (that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (thats)) |
|
608 fun case_rule_of ctxt let_expr = let |
|
609 val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd |
|
610 val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of |
|
611 |> Induct.vars_of |> hd |> cterm |
|
612 val mt = Thm.match (case_var, let_expr |> cterm) |
|
613 val case_rule = Thm.instantiate mt case_rule |
|
614 in case_rule end |
|
615 |
|
616 val case_rule = case_rule_of ctxt case_expr |
|
617 val my_case_tac = (rtac case_rule) |
|
618 val my_tac = ((Method.insert_tac (that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1 |
|
619 val result = Goal.prove ctxt1 [] [] mjp_p (K my_tac) |
|
620 val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) |
|
621 [P, thesis_p, mjp] ctxt1 |
|
622 val [case_intro_rule] = Proof_Context.export ctxt2 ctxt [result] |
|
623 val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd |
|
624 fun get_case_names rule = |
|
625 AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the |
|
626 fun put_case_names names rule = |
|
627 Thm.tag_rule ("case_names", names) rule |
|
628 val case_intro_rule = put_case_names (get_case_names ocase_rule) case_intro_rule |
|
629 in case_intro_rule end |
|
630 *} |
|
631 |
|
632 ML {* |
|
633 val t = [mjp, mjp1] |> map (case_intro_rule ctxt) |
|
634 *} |
|
635 |
|
636 ML {* |
|
637 fun case_intro_cases_tac ctxt facts i st = let |
|
638 val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt |
|
639 val rule = (case_intro_rule ctxt mjp) |
|
640 in |
|
641 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st |
|
642 end |
|
643 *} |
|
644 |
|
645 ML {* |
|
646 val case_intro_setup = |
|
647 Method.setup @{binding case_intro} |
|
648 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
649 (fn no_simp => fn ctxt => |
|
650 METHOD_CASES (fn facts => (HEADGOAL |
|
651 (case_intro_cases_tac ctxt facts))))) |
|
652 "introduction rule for goals containing case"; |
|
653 *} |
|
654 |
|
655 setup {* case_intro_setup *} |
|
656 |
|
657 |
|
658 lemma assumes "QQ (let u = e1; (j, k) = e1; (b, a) = qq j k in TT j k b a)" |
|
659 shows "P (hhh y ys)" using assms |
|
660 proof(let_elim) |
|
661 oops |
|
662 |
|
663 lemma assumes |
|
664 "QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)" |
|
665 "PP w x" |
|
666 shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)" |
|
667 using assms |
|
668 proof(case_intro) |
|
669 case None |
|
670 from None(2) |
|
671 show ?case |
|
672 proof(let_elim) |
|
673 case (LetE j k a b) |
|
674 with None |
|
675 show ?case oops |
|
676 (* |
|
677 sorry |
|
678 qed |
|
679 next |
|
680 case (Some x1) |
|
681 thus ?case |
|
682 proof(case_intro) |
|
683 case Nil |
|
684 from Nil(3) |
|
685 show ?case |
|
686 proof(let_elim) |
|
687 case (LetE j k a b) |
|
688 with Nil show ?case sorry |
|
689 qed |
|
690 next |
|
691 case (Cons y ys) |
|
692 from Cons(3) |
|
693 show ?case |
|
694 proof (let_elim) |
|
695 case (LetE j k u v) |
|
696 with Cons |
|
697 show ?case sorry |
|
698 qed |
|
699 qed |
|
700 qed |
|
701 *) |
|
702 |
|
703 lemma assumes |
|
704 "QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)" |
|
705 "PP w uux" |
|
706 shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)" |
|
707 using assms |
|
708 proof(let_elim) |
|
709 case (LetE j k m n) |
|
710 thus ?case |
|
711 proof(case_intro) |
|
712 case None |
|
713 thus ?case oops (* |
|
714 next |
|
715 case (Some x) |
|
716 thus ?case |
|
717 proof(case_intro) |
|
718 case Nil |
|
719 thus ?case sorry |
|
720 next |
|
721 case (Cons y ys) |
|
722 thus ?case sorry |
|
723 qed |
|
724 qed |
|
725 qed |
|
726 *) |
|
727 |
|
728 lemma ifE [consumes 1, case_names If_true If_false]: |
|
729 assumes "P (if b then e1 else e2)" |
|
730 "\<lbrakk>b; P e1\<rbrakk> \<Longrightarrow> thesis" |
|
731 "\<lbrakk>\<not> b; P e2\<rbrakk> \<Longrightarrow> thesis" |
|
732 shows "thesis" using assms |
|
733 by (auto split:if_splits) |
|
734 |
|
735 lemma ifI [case_names If_true If_false]: |
|
736 assumes "b \<Longrightarrow> P e1" "\<not> b \<Longrightarrow> P e2" |
|
737 shows "P (if b then e1 else e2)" using assms |
|
738 by auto |
|
739 |
|
740 ML {* |
|
741 fun if_elim_cases_tac ctxt facts = let |
|
742 val rule = @{thm ifE} |
|
743 in |
|
744 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts |
|
745 end |
|
746 *} |
|
747 |
|
748 ML {* |
|
749 val if_elim_setup = |
|
750 Method.setup @{binding if_elim} |
|
751 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
752 (fn no_simp => fn ctxt => |
|
753 METHOD_CASES (fn facts => (HEADGOAL |
|
754 (if_elim_cases_tac ctxt facts))))) |
|
755 "elimination of prems containing if "; |
|
756 *} |
|
757 |
|
758 setup {* if_elim_setup *} |
|
759 |
|
760 ML {* |
|
761 fun if_intro_cases_tac ctxt facts i st = let |
|
762 val rule = @{thm ifI} |
|
763 in |
|
764 Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st |
|
765 end |
|
766 *} |
|
767 |
|
768 ML {* |
|
769 val if_intro_setup = |
|
770 Method.setup @{binding if_intro} |
|
771 (Scan.lift (Args.mode Induct.no_simpN) >> |
|
772 (fn no_simp => fn ctxt => |
|
773 METHOD_CASES (fn facts => (HEADGOAL |
|
774 (if_intro_cases_tac ctxt facts))))) |
|
775 "introduction rule for goals containing if"; |
|
776 *} |
|
777 |
|
778 setup {* if_intro_setup *} |
|
779 |
|
780 lemma assumes "(if (B x y) then f x y else g y x) = (t, p)" |
|
781 "P1 xxx" "P2 yyy" |
|
782 shows "that" using assms |
|
783 proof(if_elim) |
|
784 case If_true |
|
785 thus ?case oops |
|
786 (* |
|
787 next |
|
788 case If_false |
|
789 thus ?case oops |
|
790 *) |
|
791 |
|
792 lemma assumes "P1 xx" "P2 yy" |
|
793 shows "P (if b then e1 else e2)" using assms |
|
794 proof(if_intro) |
|
795 case If_true |
|
796 thus ?case oops |
|
797 (* |
|
798 next |
|
799 case If_false |
|
800 thus ?case sorry |
|
801 qed |
|
802 *) |
|
803 |
|
804 end |