equal
deleted
inserted
replaced
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 **) |
59 (** The function eval **) |
60 |
60 |
61 Goalw [eval_def] "tt[false] = False"; |
61 Goalw [eval_def] "tt[[false]] = False"; |
62 by (Simp_tac 1); |
62 by (Simp_tac 1); |
63 qed "eval_false"; |
63 qed "eval_false"; |
64 |
64 |
65 Goalw [eval_def] "tt[#v] = (v:tt)"; |
65 Goalw [eval_def] "tt[[#v]] = (v:tt)"; |
66 by (Simp_tac 1); |
66 by (Simp_tac 1); |
67 qed "eval_var"; |
67 qed "eval_var"; |
68 |
68 |
69 Goalw [eval_def] "tt[p->q] = (tt[p]-->tt[q])"; |
69 Goalw [eval_def] "tt[[p->q]] = (tt[[p]]-->tt[[q]])"; |
70 by (Simp_tac 1); |
70 by (Simp_tac 1); |
71 qed "eval_imp"; |
71 qed "eval_imp"; |
72 |
72 |
73 Addsimps [eval_false, eval_var, eval_imp]; |
73 Addsimps [eval_false, eval_var, eval_imp]; |
74 |
74 |
96 by (rtac insertI1 1); |
96 by (rtac insertI1 1); |
97 by (rtac (premp RS weaken_left_insert) 1); |
97 by (rtac (premp RS weaken_left_insert) 1); |
98 qed "imp_false"; |
98 qed "imp_false"; |
99 |
99 |
100 (*This formulation is required for strong induction hypotheses*) |
100 (*This formulation is required for strong induction hypotheses*) |
101 Goal "hyps p tt |- (if tt[p] then p else p->false)"; |
101 Goal "hyps p tt |- (if tt[[p]] then p else p->false)"; |
102 by (rtac (split_if RS iffD2) 1); |
102 by (rtac (split_if RS iffD2) 1); |
103 by (induct_tac "p" 1); |
103 by (induct_tac "p" 1); |
104 by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H]))); |
104 by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H]))); |
105 by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, |
105 by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, |
106 weaken_right, imp_false] |
106 weaken_right, imp_false] |