src/HOL/Isar_examples/W_correct.thy
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8103 86f94a8116a9
     1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Sat Oct 30 20:13:16 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Sat Oct 30 20:20:48 1999 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4      AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
     1.5                ==> a |- App e1 e2 :: t1";
     1.6  
     1.7 -text {* Type assigment is close wrt.\ substitution. *};
     1.8 +text {* Type assigment is closed wrt.\ substitution. *};
     1.9  
    1.10  lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
    1.11  proof -;
    1.12 @@ -79,10 +79,10 @@
    1.13  
    1.14  primrec
    1.15    "W (Var i) a n =
    1.16 -      (if i < length a then Ok(id_subst, a ! i, n) else Fail)"
    1.17 +      (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
    1.18    "W (Abs e) a n =
    1.19        ((s, t, m) := W e (TVar n # a) (Suc n);
    1.20 -       Ok(s, (s n) -> t, m))"
    1.21 +       Ok (s, (s n) -> t, m))"
    1.22    "W (App e1 e2) a n =
    1.23        ((s1, t1, m1) := W e1 a n;
    1.24         (s2, t2, m2) := W e2 ($s1 a) m1;
    1.25 @@ -92,9 +92,13 @@
    1.26  
    1.27  subsection {* Correctness theorem *};
    1.28  
    1.29 +text_raw {* \begin{comment} *};
    1.30 +
    1.31  (* FIXME proper split att/mod *)
    1.32  ML_setup {* Addsplits [split_bind]; *};
    1.33  
    1.34 +text_raw {* \end{comment} *};
    1.35 +
    1.36  theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
    1.37  proof -;
    1.38    assume W_ok: "W e a n = Ok (s, t, m)";