equal
deleted
inserted
replaced
73 R ... /\ P ...; split_conj picks out |
73 R ... /\ P ...; split_conj picks out |
74 the part P ... |
74 the part P ... |
75 *) |
75 *) |
76 fun transform_prem ctxt names thm = |
76 fun transform_prem ctxt names thm = |
77 let |
77 let |
78 fun split_conj names (Const ("op &", _) $ p $ q) = |
78 fun split_conj names (Const ("op &", _) $ f1 $ f2) = |
79 (case head_of p of |
79 (case head_of f1 of |
80 Const (name, _) => if name mem names then SOME q else NONE |
80 Const (name, _) => if name mem names then SOME f2 else NONE |
81 | _ => NONE) |
81 | _ => NONE) |
82 | split_conj _ _ = NONE; |
82 | split_conj _ _ = NONE; |
83 in |
83 in |
84 map_thm ctxt (split_conj names) (etac conjunct2 1) thm |
84 map_thm ctxt (split_conj names) (etac conjunct2 1) thm |
85 end |
85 end |
100 in |
100 in |
101 eqvt_strict_tac ctxt [] pred_names THEN' |
101 eqvt_strict_tac ctxt [] pred_names THEN' |
102 SUBPROOF (fn {prems, context as ctxt, ...} => |
102 SUBPROOF (fn {prems, context as ctxt, ...} => |
103 let |
103 let |
104 val prems' = map (transform_prem ctxt pred_names) prems |
104 val prems' = map (transform_prem ctxt pred_names) prems |
|
105 |
105 val tac1 = resolve_tac prems' |
106 val tac1 = resolve_tac prems' |
106 val tac2 = EVERY' [ rtac pi_intro_rule, |
107 val tac2 = EVERY' [ rtac pi_intro_rule, |
107 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
108 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
108 val tac3 = EVERY' [ rtac pi_intro_rule, |
109 val tac3 = EVERY' [ rtac pi_intro_rule, |
109 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems'] |
110 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems'] |