# HG changeset patch # User wenzelm # Date 947070074 -3600 # Node ID 86f94a8116a9e556ee08c87eacb6a84158db2d70 # Parent 424f6e663977a46ebc1978d7539937fa47b4a184 obtain; diff -r 424f6e663977 -r 86f94a8116a9 src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Wed Jan 05 11:58:18 2000 +0100 +++ b/src/HOL/Isar_examples/W_correct.thy Wed Jan 05 12:01:14 2000 +0100 @@ -47,14 +47,14 @@ thus ?thesis (is "?P a e t"); proof (rule has_type.induct); (* FIXME induct method *) fix a n; - assume "n < length a"; + assume "n < length (a::typ list)"; hence "n < length (map ($ s) a)"; by simp; hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI); also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map); also; have "map ($ s) a = $ s a"; - by (simp only: app_subst_list); (* FIXME unfold fails!? *) + by (simp only: app_subst_list); finally; show "?P a (Var n) (a ! n)"; .; next; fix a e t1 t2; @@ -112,31 +112,25 @@ proof (intro allI impI); fix a s t m n; assume "Ok (s, t, m) = W (Abs e) a n"; - hence "EX t'. t = s n -> t' & - Ok (s, t', m) = W e (TVar n # a) (Suc n)"; - by (rule rev_mp) simp; - with hyp; show "$ s a |- Abs e :: t"; - by (force intro: has_type.AbsI); + thus "$ s a |- Abs e :: t"; + obtain t' in "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)"; + by (rule rev_mp) simp; + with hyp; show ?thesis; by (force intro: has_type.AbsI); + qed; qed; next; fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; show "?P (App e1 e2)"; proof (intro allI impI); fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; - hence "EX s1 t1 n1 s2 t2 n2 u. - s = $ u o $ s2 o s1 & t = u n2 & - mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & - W e2 ($ s1 a) n1 = Ok (s2, t2, n2) & - W e1 a n = Ok (s1, t1, n1)"; - by (rule rev_mp) (simp, force); (* FIXME force fails !??*) thus "$ s a |- App e1 e2 :: t"; - proof (elim exE conjE); - fix s1 t1 n1 s2 t2 n2 u; - assume s: "s = $ u o $ s2 o s1" + obtain s1 t1 n1 s2 t2 n2 u in + s: "s = $ u o $ s2 o s1" and t: "t = u n2" and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" and W1_ok: "W e1 a n = Ok (s1, t1, n1)" and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; + by (rule rev_mp) simp; show ?thesis; proof (rule has_type.AppI); from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";