src/HOL/Isar_examples/W_correct.thy
changeset 8103 86f94a8116a9
parent 7982 d534b897ce39
child 8109 aca11f954993
     1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Wed Jan 05 11:58:18 2000 +0100
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Wed Jan 05 12:01:14 2000 +0100
     1.3 @@ -47,14 +47,14 @@
     1.4    thus ?thesis (is "?P a e t");
     1.5    proof (rule has_type.induct);     (* FIXME induct method *)
     1.6      fix a n;
     1.7 -    assume "n < length a";
     1.8 +    assume "n < length (a::typ list)";
     1.9      hence "n < length (map ($ s) a)"; by simp;
    1.10      hence "map ($ s) a |- Var n :: map ($ s) a ! n";
    1.11        by (rule has_type.VarI);
    1.12      also; have "map ($ s) a ! n = $ s (a ! n)";
    1.13        by (rule nth_map);
    1.14      also; have "map ($ s) a = $ s a";
    1.15 -      by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
    1.16 +      by (simp only: app_subst_list);
    1.17      finally; show "?P a (Var n) (a ! n)"; .;
    1.18    next;
    1.19      fix a e t1 t2;
    1.20 @@ -112,31 +112,25 @@
    1.21      proof (intro allI impI);
    1.22        fix a s t m n;
    1.23        assume "Ok (s, t, m) = W (Abs e) a n";
    1.24 -      hence "EX t'. t = s n -> t' &
    1.25 -          Ok (s, t', m) = W e (TVar n # a) (Suc n)";
    1.26 -        by (rule rev_mp) simp;
    1.27 -      with hyp; show "$ s a |- Abs e :: t";
    1.28 -        by (force intro: has_type.AbsI);
    1.29 +      thus "$ s a |- Abs e :: t";
    1.30 +	obtain t' in "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
    1.31 +	  by (rule rev_mp) simp;
    1.32 +	with hyp; show ?thesis; by (force intro: has_type.AbsI);
    1.33 +      qed;
    1.34      qed;
    1.35    next;
    1.36      fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2";
    1.37      show "?P (App e1 e2)";
    1.38      proof (intro allI impI);
    1.39        fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
    1.40 -      hence "EX s1 t1 n1 s2 t2 n2 u.
    1.41 -          s = $ u o $ s2 o s1 & t = u n2 &
    1.42 -          mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
    1.43 -             W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
    1.44 -             W e1 a n = Ok (s1, t1, n1)";
    1.45 -        by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
    1.46        thus "$ s a |- App e1 e2 :: t";
    1.47 -      proof (elim exE conjE);
    1.48 -        fix s1 t1 n1 s2 t2 n2 u;
    1.49 -        assume s: "s = $ u o $ s2 o s1"
    1.50 +	obtain s1 t1 n1 s2 t2 n2 u in
    1.51 +          s: "s = $ u o $ s2 o s1"
    1.52            and t: "t = u n2"
    1.53            and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
    1.54            and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
    1.55            and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
    1.56 +	    by (rule rev_mp) simp;
    1.57          show ?thesis;
    1.58          proof (rule has_type.AppI);
    1.59            from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";