equal
deleted
inserted
replaced
80 ML_setup {* Addsplits [split_bind]; *}; |
80 ML_setup {* Addsplits [split_bind]; *}; |
81 |
81 |
82 theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"; |
82 theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"; |
83 proof -; |
83 proof -; |
84 assume W_ok: "W e a n = Ok (s, t, m)"; |
84 assume W_ok: "W e a n = Ok (s, t, m)"; |
85 let ?P = "%e. ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t"; |
85 have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e"); |
86 (* FIXME (is ...) fails!? *) |
|
87 have "?P e"; |
|
88 proof (induct e); |
86 proof (induct e); |
89 fix n; show "?P (Var n)"; by simp; |
87 fix n; show "?P (Var n)"; by simp; |
90 next; |
88 next; |
91 fix e; assume hyp: "?P e"; |
89 fix e; assume hyp: "?P e"; |
92 show "?P (Abs e)"; |
90 show "?P (Abs e)"; |