22 |
22 |
23 fun mk_cplus p q = Thm.capply (Thm.capply @{cterm "plus :: perm => perm => perm"} p) q |
23 fun mk_cplus p q = Thm.capply (Thm.capply @{cterm "plus :: perm => perm => perm"} p) q |
24 |
24 |
25 fun mk_cminus p = Thm.capply @{cterm "uminus :: perm => perm"} p |
25 fun mk_cminus p = Thm.capply @{cterm "uminus :: perm => perm"} p |
26 |
26 |
27 |
|
28 fun minus_permute_intro_tac p = |
27 fun minus_permute_intro_tac p = |
29 rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}) |
28 rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}) |
30 |
29 |
31 fun minus_permute_elim p thm = |
30 fun minus_permute_elim p thm = |
32 thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) |
31 thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) |
33 |
32 |
|
33 (* fixme: move to nominal_library *) |
34 fun real_head_of (@{term Trueprop} $ t) = real_head_of t |
34 fun real_head_of (@{term Trueprop} $ t) = real_head_of t |
35 | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t |
35 | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t |
36 | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t |
36 | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t |
37 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t |
37 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t |
38 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t |
38 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t |
54 |> (curry list_all_free) params |
54 |> (curry list_all_free) params |
55 in |
55 in |
56 if null avoid then [] else [vc_goal, finite_goal] |
56 if null avoid then [] else [vc_goal, finite_goal] |
57 end |
57 end |
58 |
58 |
|
59 (* fixme: move to nominal_library *) |
59 fun map_term prop f trm = |
60 fun map_term prop f trm = |
60 if prop trm |
61 if prop trm |
61 then f trm |
62 then f trm |
62 else case trm of |
63 else case trm of |
63 (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 |
64 (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 |
118 |> add_c_prop false Ps (Bound 0, c_name, c_ty) |
119 |> add_c_prop false Ps (Bound 0, c_name, c_ty) |
119 in |
120 in |
120 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
121 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
121 end |
122 end |
122 |
123 |
|
124 (* fixme: move to nominal_library *) |
123 fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) |
125 fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) |
124 | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) |
126 | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) |
125 | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) |
127 | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) |
126 | same_name _ = false |
128 | same_name _ = false |
127 |
129 |
|
130 (* fixme: move to nominal_library *) |
128 fun map7 _ [] [] [] [] [] [] [] = [] |
131 fun map7 _ [] [] [] [] [] [] [] = [] |
129 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = |
132 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = |
130 f x y z u v r s :: map7 f xs ys zs us vs rs ss |
133 f x y z u v r s :: map7 f xs ys zs us vs rs ss |
131 |
134 |
132 (* local abbreviations *) |
135 (* local abbreviations *) |
148 |> map (eqvt_srule context) |
151 |> map (eqvt_srule context) |
149 |
152 |
150 val prm' = (prems' MRS prm) |
153 val prm' = (prems' MRS prm) |
151 |> flag ? (all_elims [p]) |
154 |> flag ? (all_elims [p]) |
152 |> flag ? (eqvt_srule context) |
155 |> flag ? (eqvt_srule context) |
153 |
|
154 val _ = tracing ("prm':" ^ @{make_string} prm') |
|
155 in |
156 in |
156 print_tac "start helper" |
157 asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1 |
157 THEN asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1 |
|
158 THEN print_tac "final helper" |
|
159 end) ctxt |
158 end) ctxt |
160 |
159 |
161 fun non_binder_tac prem intr_cvars Ps ctxt = |
160 fun non_binder_tac prem intr_cvars Ps ctxt = |
162 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
161 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
163 let |
162 let |
250 helper_tac false prm (mk_cplus q p) ctxt' ] |
249 helper_tac false prm (mk_cplus q p) ctxt' ] |
251 |
250 |
252 fun select prm (t, i) = |
251 fun select prm (t, i) = |
253 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
252 (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i |
254 |
253 |
255 val _ = tracing ("fthm:\n" ^ @{make_string} fthm) |
|
256 val _ = tracing ("fr_eqs:\n" ^ cat_lines (map @{make_string} fresh_eqs)) |
|
257 val _ = tracing ("fprop:\n" ^ @{make_string} fprop) |
|
258 val _ = tracing ("fprop':\n" ^ @{make_string} fprop') |
|
259 val _ = tracing ("fperm:\n" ^ @{make_string} q) |
|
260 val _ = tracing ("prem':\n" ^ @{make_string} prem') |
|
261 |
|
262 val side_thm = Goal.prove ctxt' [] [] (term_of concl) |
254 val side_thm = Goal.prove ctxt' [] [] (term_of concl) |
263 (fn {context, ...} => |
255 (fn {context, ...} => |
264 EVERY1 [ CONVERSION (expand_conv_bot context), |
256 EVERY1 [ CONVERSION (expand_conv_bot context), |
265 eqvt_stac context, |
257 eqvt_stac context, |
266 rtac prem', |
258 rtac prem', |
267 RANGE (tac_fresh :: map (SUBGOAL o select) prems), |
259 RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |
268 K (print_tac "GOAL") ]) |
|
269 |> singleton (ProofContext.export ctxt' ctxt) |
260 |> singleton (ProofContext.export ctxt' ctxt) |
270 in |
261 in |
271 rtac side_thm 1 |
262 rtac side_thm 1 |
272 end) ctxt |
263 end) ctxt |
273 |
264 |
362 |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) |
353 |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) |
363 |
354 |
364 val attrs = |
355 val attrs = |
365 [ Attrib.internal (K (Rule_Cases.consumes 1)), |
356 [ Attrib.internal (K (Rule_Cases.consumes 1)), |
366 Attrib.internal (K (Rule_Cases.case_names rule_names)) ] |
357 Attrib.internal (K (Rule_Cases.case_names rule_names)) ] |
367 val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) strong_ind_thms)) |
|
368 val _ = tracing ("rule_names: " ^ commas rule_names) |
|
369 val _ = tracing ("pred_names: " ^ commas pred_names) |
|
370 in |
358 in |
371 ctxt |
359 ctxt |
372 |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |
360 |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |
373 |> snd |
361 |> snd |
374 end |
362 end |