equal
deleted
inserted
replaced
54 val thms_falseE = weaken_right RS (thms.DN RS thms.MP); |
54 val thms_falseE = weaken_right RS (thms.DN RS thms.MP); |
55 |
55 |
56 (* [| H |- p->false; H |- p; q: pl |] ==> H |- q *) |
56 (* [| H |- p->false; H |- p; q: pl |] ==> H |- q *) |
57 bind_thm ("thms_notE", (thms.MP RS thms_falseE)); |
57 bind_thm ("thms_notE", (thms.MP RS thms_falseE)); |
58 |
58 |
59 (** The function eval **) |
|
60 |
|
61 Goalw [eval_def] "tt[[false]] = False"; |
|
62 by (Simp_tac 1); |
|
63 qed "eval_false"; |
|
64 |
|
65 Goalw [eval_def] "tt[[#v]] = (v:tt)"; |
|
66 by (Simp_tac 1); |
|
67 qed "eval_var"; |
|
68 |
|
69 Goalw [eval_def] "tt[[p->q]] = (tt[[p]]-->tt[[q]])"; |
|
70 by (Simp_tac 1); |
|
71 qed "eval_imp"; |
|
72 |
|
73 Addsimps [eval_false, eval_var, eval_imp]; |
|
74 |
59 |
75 (*Soundness of the rules wrt truth-table semantics*) |
60 (*Soundness of the rules wrt truth-table semantics*) |
76 Goalw [sat_def] "H |- p ==> H |= p"; |
61 Goalw [sat_def] "H |- p ==> H |= p"; |
77 by (etac thms.induct 1); |
62 by (etac thms.induct 1); |
78 by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5); |
63 by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5); |