35 |
35 |
36 |
36 |
37 (** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
37 (** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
38 |
38 |
39 qed_goal "allL_thin" LK.thy |
39 qed_goal "allL_thin" LK.thy |
40 "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E" |
40 "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E" |
41 (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]); |
41 (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]); |
42 |
42 |
43 qed_goal "exR_thin" LK.thy |
43 qed_goal "exR_thin" LK.thy |
44 "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F" |
44 "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F" |
45 (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]); |
45 (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]); |
46 |
46 |
47 (* Symmetry of equality in hypotheses *) |
47 (* Symmetry of equality in hypotheses *) |
48 qed_goal "symL" LK.thy |
48 qed_goal "symL" LK.thy |
49 "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" |
49 "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" |