improved: 'induct' handle non-atomic goals;
authorwenzelm
Mon Nov 06 22:56:07 2000 +0100 (2000-11-06)
changeset 10408d8b3613158b1
parent 10407 998778f8d63b
child 10409 10a1b95ce642
improved: 'induct' handle non-atomic goals;
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Mon Nov 06 22:54:13 2000 +0100
     1.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Nov 06 22:56:07 2000 +0100
     1.3 @@ -126,28 +126,34 @@
     1.4  
     1.5  lemma gcd_fib_mod:
     1.6    "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
     1.7 -proof (induct n rule: nat_less_induct)
     1.8 -  fix n
     1.9 +proof -
    1.10    assume m: "0 < m"
    1.11 -  and hyp: "ALL ma. ma < n
    1.12 -           --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
    1.13 -  have "n mod m = (if n < m then n else (n - m) mod m)"
    1.14 -    by (rule mod_if)
    1.15 -  also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
    1.16 -  proof cases
    1.17 -    assume "n < m" thus ?thesis by simp
    1.18 -  next
    1.19 -    assume not_lt: "~ n < m" hence le: "m <= n" by simp
    1.20 -    have "n - m < n" by (simp! add: diff_less)
    1.21 -    with hyp have "gcd (fib m, fib ((n - m) mod m))
    1.22 -       = gcd (fib m, fib (n - m))" by simp
    1.23 -    also from le have "... = gcd (fib m, fib n)"
    1.24 -      by (rule gcd_fib_diff)
    1.25 -    finally have "gcd (fib m, fib ((n - m) mod m)) =
    1.26 -      gcd (fib m, fib n)" .
    1.27 -    with not_lt show ?thesis by simp
    1.28 +  show ?thesis
    1.29 +  proof (induct n rule: nat_less_induct)
    1.30 +    fix n
    1.31 +    assume hyp: "ALL ma. ma < n
    1.32 +      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
    1.33 +    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    1.34 +    proof -
    1.35 +      have "n mod m = (if n < m then n else (n - m) mod m)"
    1.36 +	by (rule mod_if)
    1.37 +      also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
    1.38 +      proof cases
    1.39 +	assume "n < m" thus ?thesis by simp
    1.40 +      next
    1.41 +	assume not_lt: "~ n < m" hence le: "m <= n" by simp
    1.42 +	have "n - m < n" by (simp! add: diff_less)
    1.43 +	with hyp have "gcd (fib m, fib ((n - m) mod m))
    1.44 +	  = gcd (fib m, fib (n - m))" by simp
    1.45 +	also from le have "... = gcd (fib m, fib n)"
    1.46 +	  by (rule gcd_fib_diff)
    1.47 +	finally have "gcd (fib m, fib ((n - m) mod m)) =
    1.48 +	  gcd (fib m, fib n)" .
    1.49 +	with not_lt show ?thesis by simp
    1.50 +      qed
    1.51 +      finally show ?thesis .
    1.52 +    qed
    1.53    qed
    1.54 -  finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
    1.55  qed
    1.56  
    1.57  
     2.1 --- a/src/HOL/Isar_examples/Hoare.thy	Mon Nov 06 22:54:13 2000 +0100
     2.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Mon Nov 06 22:56:07 2000 +0100
     2.3 @@ -166,28 +166,26 @@
     2.4    fix s s' assume s: "s : P"
     2.5    assume "Sem (While b X c) s s'"
     2.6    then obtain n where iter: "iter n b (Sem c) s s'" by auto
     2.7 -  show "s' : P Int -b"
     2.8 -  proof -
     2.9 -    have "ALL s s'. iter n b (Sem c) s s' --> s : P --> s' : P Int -b"
    2.10 -      (is "?P n")
    2.11 -    proof (induct (stripped) n)
    2.12 -      fix s s' assume s: "s : P"
    2.13 -      {
    2.14 -        assume "iter 0 b (Sem c) s s'"
    2.15 -        with s show "s' : P Int -b" by auto
    2.16 -      next
    2.17 -        fix n assume hyp: "?P n"
    2.18 -        assume "iter (Suc n) b (Sem c) s s'"
    2.19 -        then obtain s'' where b: "s : b" and sem: "Sem c s s''"
    2.20 -            and iter: "iter n b (Sem c) s'' s'"
    2.21 -          by auto
    2.22 -        from s b have "s : P Int b" by simp
    2.23 -        with body sem have "s'' : P" ..
    2.24 -        with hyp iter show "s' : P Int -b" by simp
    2.25 -      }
    2.26 -    qed
    2.27 -    with iter s show ?thesis by simp
    2.28 +
    2.29 +  have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
    2.30 +    (is "PROP ?P n")
    2.31 +  proof (induct n)
    2.32 +    fix s assume s: "s : P"
    2.33 +    {
    2.34 +      assume "iter 0 b (Sem c) s s'"
    2.35 +      with s show "?thesis s" by auto
    2.36 +    next
    2.37 +      fix n assume hyp: "PROP ?P n"
    2.38 +      assume "iter (Suc n) b (Sem c) s s'"
    2.39 +      then obtain s'' where b: "s : b" and sem: "Sem c s s''"
    2.40 +        and iter: "iter n b (Sem c) s'' s'"
    2.41 +        by auto
    2.42 +      from s b have "s : P Int b" by simp
    2.43 +      with body sem have "s'' : P" ..
    2.44 +      with iter show "?thesis s" by (rule hyp)
    2.45 +    }
    2.46    qed
    2.47 +  from this iter s show "s' : P Int -b" .
    2.48  qed
    2.49  
    2.50  
     3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Nov 06 22:54:13 2000 +0100
     3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Nov 06 22:56:07 2000 +0100
     3.3 @@ -23,31 +23,38 @@
     3.4  inductive "tiling A"
     3.5    intros
     3.6      empty: "{} : tiling A"
     3.7 -    Un:    "a : A ==> t : tiling A ==> a <= - t
     3.8 -              ==> a Un t : tiling A"
     3.9 +    Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
    3.10  
    3.11  
    3.12  text "The union of two disjoint tilings is a tiling."
    3.13  
    3.14  lemma tiling_Un:
    3.15 -  "t : tiling A --> u : tiling A --> t Int u = {}
    3.16 -    --> t Un u : tiling A"
    3.17 -proof
    3.18 -  assume "t : tiling A" (is "_ : ?T")
    3.19 -  thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t")
    3.20 -  proof (induct (stripped) t)
    3.21 -    assume "u : ?T" "{} Int u = {}"
    3.22 -    thus "{} Un u : ?T" by simp
    3.23 +  "t : tiling A ==> u : tiling A ==> t Int u = {}
    3.24 +    ==> t Un u : tiling A"
    3.25 +proof -
    3.26 +  let ?T = "tiling A"
    3.27 +  assume u: "u : ?T"
    3.28 +  assume "t : ?T"
    3.29 +  thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
    3.30 +  proof (induct t)
    3.31 +    from u show "{} Un u : ?T" by simp
    3.32    next
    3.33      fix a t
    3.34 -    assume "a : A" "t : ?T" "?P t" "a <= - t"
    3.35 -    assume "u : ?T" "(a Un t) Int u = {}"
    3.36 -    have hyp: "t Un u: ?T" by (blast!)
    3.37 -    have "a <= - (t Un u)" by (blast!)
    3.38 -    with _ hyp have "a Un (t Un u) : ?T" by (rule tiling.Un)
    3.39 -    also have "a Un (t Un u) = (a Un t) Un u"
    3.40 -      by (simp only: Un_assoc)
    3.41 -    finally show "... : ?T" .
    3.42 +    assume "a : A" and hyp: "PROP ?P t"
    3.43 +      and at: "a <= - t" and atu: "(a Un t) Int u = {}"
    3.44 +    show "(a Un t) Un u : ?T"
    3.45 +    proof -
    3.46 +      have "a Un (t Un u) : ?T"
    3.47 +      proof (rule tiling.Un)
    3.48 +        show "a : A" .
    3.49 +        from atu have "t Int u = {}" by blast
    3.50 +        thus "t Un u: ?T" by (rule hyp)
    3.51 +        from at atu show "a <= - (t Un u)" by blast
    3.52 +      qed
    3.53 +      also have "a Un (t Un u) = (a Un t) Un u"
    3.54 +        by (simp only: Un_assoc)
    3.55 +      finally show ?thesis .
    3.56 +    qed
    3.57    qed
    3.58  qed
    3.59  
    3.60 @@ -112,13 +119,13 @@
    3.61  
    3.62  subsection {* Dominoes *}
    3.63  
    3.64 -consts 
    3.65 +consts
    3.66    domino :: "(nat * nat) set set"
    3.67  
    3.68  inductive domino
    3.69    intros
    3.70 -    horiz:  "{(i, j), (i, j + 1)} : domino"
    3.71 -    vertl:  "{(i, j), (i + 1, j)} : domino"
    3.72 +    horiz: "{(i, j), (i, j + 1)} : domino"
    3.73 +    vertl: "{(i, j), (i + 1, j)} : domino"
    3.74  
    3.75  lemma dominoes_tile_row:
    3.76    "{i} <*> below (2 * n) : tiling domino"
    3.77 @@ -154,7 +161,7 @@
    3.78  
    3.79    have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
    3.80    also have "... : ?T"
    3.81 -  proof (rule tiling_Un [rule_format])
    3.82 +  proof (rule tiling_Un)
    3.83      show "?t : ?T" by (rule dominoes_tile_row)
    3.84      from hyp show "?B m : ?T" .
    3.85      show "?t Int ?B m = {}" by blast
    3.86 @@ -178,10 +185,14 @@
    3.87  qed
    3.88  
    3.89  lemma domino_finite: "d: domino ==> finite d"
    3.90 -proof (induct set: domino)
    3.91 -  fix i j :: nat
    3.92 -  show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
    3.93 -  show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
    3.94 +proof -
    3.95 +  assume "d: domino"
    3.96 +  thus ?thesis
    3.97 +  proof induct
    3.98 +    fix i j :: nat
    3.99 +    show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
   3.100 +    show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
   3.101 +  qed
   3.102  qed
   3.103  
   3.104  
   3.105 @@ -211,27 +222,27 @@
   3.106  
   3.107      fix a t
   3.108      let ?e = evnodd
   3.109 -    assume "a : domino" "t : ?T"
   3.110 +    assume "a : domino" and "t : ?T"
   3.111        and hyp: "card (?e t 0) = card (?e t 1)"
   3.112 -      and "a <= - t"
   3.113 +      and at: "a <= - t"
   3.114  
   3.115      have card_suc:
   3.116        "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   3.117      proof -
   3.118        fix b assume "b < 2"
   3.119        have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
   3.120 -      also obtain i j where "?e a b = {(i, j)}"
   3.121 +      also obtain i j where e: "?e a b = {(i, j)}"
   3.122        proof -
   3.123 -	have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
   3.124 -	thus ?thesis by (blast intro: that)
   3.125 +        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
   3.126 +        thus ?thesis by (blast intro: that)
   3.127        qed
   3.128        also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
   3.129        also have "card ... = Suc (card (?e t b))"
   3.130        proof (rule card_insert_disjoint)
   3.131 -	show "finite (?e t b)"
   3.132 +        show "finite (?e t b)"
   3.133            by (rule evnodd_finite, rule tiling_domino_finite)
   3.134 -	have "(i, j) : ?e a b" by (simp!)
   3.135 -	thus "(i, j) ~: ?e t b" by (blast! dest: evnoddD)
   3.136 +        from e have "(i, j) : ?e a b" by simp
   3.137 +        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
   3.138        qed
   3.139        finally show "?thesis b" .
   3.140      qed
   3.141 @@ -274,9 +285,9 @@
   3.142        have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
   3.143          < card (?e ?t' 0)"
   3.144        proof (rule card_Diff1_less)
   3.145 -	from _ fin show "finite (?e ?t' 0)"
   3.146 +        from _ fin show "finite (?e ?t' 0)"
   3.147            by (rule finite_subset) auto
   3.148 -	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
   3.149 +        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
   3.150        qed
   3.151        thus ?thesis by simp
   3.152      qed
     4.1 --- a/src/HOL/Isar_examples/W_correct.thy	Mon Nov 06 22:54:13 2000 +0100
     4.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Mon Nov 06 22:56:07 2000 +0100
     4.3 @@ -27,7 +27,7 @@
     4.4    has_type :: "(typ list * expr * typ) set"
     4.5  
     4.6  syntax
     4.7 -  "_has_type" :: "[typ list, expr, typ] => bool"
     4.8 +  "_has_type" :: "typ list => expr => typ => bool"
     4.9      ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
    4.10  translations
    4.11    "a |- e :: t" == "(a, e, t) : has_type"
    4.12 @@ -74,7 +74,7 @@
    4.13  subsection {* Type inference algorithm W *}
    4.14  
    4.15  consts
    4.16 -  W :: "[expr, typ list, nat] => (subst * typ * nat) maybe"
    4.17 +  W :: "expr => typ list => nat => (subst * typ * nat) maybe"
    4.18  
    4.19  primrec
    4.20    "W (Var i) a n =
    4.21 @@ -91,59 +91,52 @@
    4.22  
    4.23  subsection {* Correctness theorem *}
    4.24  
    4.25 -theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"
    4.26 -proof -
    4.27 -  assume W_ok: "W e a n = Ok (s, t, m)"
    4.28 -  have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t"
    4.29 -    (is "?P e")
    4.30 -  proof (induct (stripped) e)
    4.31 -    fix a s t m n
    4.32 -    {
    4.33 -      fix i
    4.34 -      assume "Ok (s, t, m) = W (Var i) a n"
    4.35 -      thus "$ s a |- Var i :: t" by (simp split: if_splits)
    4.36 -    next
    4.37 -      fix e assume hyp: "?P e"
    4.38 -      assume "Ok (s, t, m) = W (Abs e) a n"
    4.39 -      then obtain t' where "t = s n -> t'"
    4.40 -	  and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
    4.41 -	by (auto split: bind_splits)
    4.42 -      with hyp show "$ s a |- Abs e :: t"
    4.43 -	by (force intro: has_type.Abs)
    4.44 -    next
    4.45 -      fix e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
    4.46 -      assume "Ok (s, t, m) = W (App e1 e2) a n"
    4.47 -      then obtain s1 t1 n1 s2 t2 n2 u where
    4.48 +theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t"
    4.49 +  (is "PROP ?P e")
    4.50 +proof (induct e)
    4.51 +  fix a s t m n
    4.52 +  {
    4.53 +    fix i
    4.54 +    assume "Ok (s, t, m) = W (Var i) a n"
    4.55 +    thus "$ s a |- Var i :: t" by (simp split: if_splits)
    4.56 +  next
    4.57 +    fix e assume hyp: "PROP ?P e"
    4.58 +    assume "Ok (s, t, m) = W (Abs e) a n"
    4.59 +    then obtain t' where "t = s n -> t'"
    4.60 +        and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
    4.61 +      by (auto split: bind_splits)
    4.62 +    with hyp show "$ s a |- Abs e :: t"
    4.63 +      by (force intro: has_type.Abs)
    4.64 +  next
    4.65 +    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
    4.66 +    assume "Ok (s, t, m) = W (App e1 e2) a n"
    4.67 +    then obtain s1 t1 n1 s2 t2 n2 u where
    4.68            s: "s = $ u o $ s2 o s1"
    4.69 -          and t: "t = u n2"
    4.70 -          and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
    4.71 -          and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
    4.72 -          and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"
    4.73 -	by (auto split: bind_splits simp: that)
    4.74 -      show "$ s a |- App e1 e2 :: t"
    4.75 -      proof (rule has_type.App)
    4.76 -        from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
    4.77 -          by (simp add: subst_comp_tel o_def)
    4.78 -        show "$s a |- e1 :: $ u t2 -> t"
    4.79 -        proof -
    4.80 -          from hyp1 W1_ok [symmetric] have "$ s1 a |- e1 :: t1"
    4.81 -            by blast
    4.82 -          hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
    4.83 -            by (intro has_type_subst_closed)
    4.84 -          with s' t mgu_ok show ?thesis by simp
    4.85 -        qed
    4.86 -        show "$ s a |- e2 :: $ u t2"
    4.87 -        proof -
    4.88 -          from hyp2 W2_ok [symmetric]
    4.89 -          have "$ s2 ($ s1 a) |- e2 :: t2" by blast
    4.90 -          hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
    4.91 -            by (rule has_type_subst_closed)
    4.92 -          with s' show ?thesis by simp
    4.93 -        qed
    4.94 +        and t: "t = u n2"
    4.95 +        and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
    4.96 +        and W1_ok: "Ok (s1, t1, n1) = W e1 a n"
    4.97 +        and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1"
    4.98 +      by (auto split: bind_splits simp: that)
    4.99 +    show "$ s a |- App e1 e2 :: t"
   4.100 +    proof (rule has_type.App)
   4.101 +      from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
   4.102 +        by (simp add: subst_comp_tel o_def)
   4.103 +      show "$s a |- e1 :: $ u t2 -> t"
   4.104 +      proof -
   4.105 +        from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1)
   4.106 +        hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
   4.107 +          by (intro has_type_subst_closed)
   4.108 +        with s' t mgu_ok show ?thesis by simp
   4.109        qed
   4.110 -    }
   4.111 -  qed
   4.112 -  with W_ok [symmetric] show ?thesis by blast
   4.113 +      show "$ s a |- e2 :: $ u t2"
   4.114 +      proof -
   4.115 +        from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2)
   4.116 +        hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
   4.117 +          by (rule has_type_subst_closed)
   4.118 +        with s' show ?thesis by simp
   4.119 +      qed
   4.120 +    qed
   4.121 +  }
   4.122  qed
   4.123  
   4.124  end
     5.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:54:13 2000 +0100
     5.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:56:07 2000 +0100
     5.3 @@ -137,49 +137,44 @@
     5.4  
     5.5  theorem parallel_decomp:
     5.6    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
     5.7 -  (concl is "?E xs")
     5.8 -proof -
     5.9 -  assume "xs \<parallel> ys"
    5.10 -  have "?this --> ?E xs" (is "?P xs")
    5.11 -  proof (induct (stripped) xs rule: rev_induct)
    5.12 -    assume "[] \<parallel> ys" hence False by auto
    5.13 -    thus "?E []" ..
    5.14 -  next
    5.15 -    fix x xs
    5.16 -    assume hyp: "?P xs"
    5.17 -    assume asm: "xs @ [x] \<parallel> ys"
    5.18 -    show "?E (xs @ [x])"
    5.19 -    proof (rule prefix_cases)
    5.20 -      assume le: "xs \<le> ys"
    5.21 -      then obtain ys' where ys: "ys = xs @ ys'" ..
    5.22 -      show ?thesis
    5.23 -      proof (cases ys')
    5.24 -        assume "ys' = []" with ys have "xs = ys" by simp
    5.25 -        with asm have "[x] \<parallel> []" by auto
    5.26 -        hence False by blast
    5.27 -        thus ?thesis ..
    5.28 -      next
    5.29 -        fix c cs assume ys': "ys' = c # cs"
    5.30 -        with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    5.31 -        hence "x \<noteq> c" by auto
    5.32 -        moreover have "xs @ [x] = xs @ x # []" by simp
    5.33 -        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    5.34 -        ultimately show ?thesis by blast
    5.35 -      qed
    5.36 -    next
    5.37 -      assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    5.38 -      with asm have False by blast
    5.39 +  (is "PROP ?P xs" concl is "?E xs")
    5.40 +proof (induct xs rule: rev_induct)
    5.41 +  assume "[] \<parallel> ys" hence False by auto
    5.42 +  thus "?E []" ..
    5.43 +next
    5.44 +  fix x xs
    5.45 +  assume hyp: "PROP ?P xs"
    5.46 +  assume asm: "xs @ [x] \<parallel> ys"
    5.47 +  show "?E (xs @ [x])"
    5.48 +  proof (rule prefix_cases)
    5.49 +    assume le: "xs \<le> ys"
    5.50 +    then obtain ys' where ys: "ys = xs @ ys'" ..
    5.51 +    show ?thesis
    5.52 +    proof (cases ys')
    5.53 +      assume "ys' = []" with ys have "xs = ys" by simp
    5.54 +      with asm have "[x] \<parallel> []" by auto
    5.55 +      hence False by blast
    5.56        thus ?thesis ..
    5.57      next
    5.58 -      assume "xs \<parallel> ys"
    5.59 -      with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    5.60 -          and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    5.61 -	by blast
    5.62 -      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
    5.63 -      with neq ys show ?thesis by blast
    5.64 +      fix c cs assume ys': "ys' = c # cs"
    5.65 +      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    5.66 +      hence "x \<noteq> c" by auto
    5.67 +      moreover have "xs @ [x] = xs @ x # []" by simp
    5.68 +      moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    5.69 +      ultimately show ?thesis by blast
    5.70      qed
    5.71 +  next
    5.72 +    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    5.73 +    with asm have False by blast
    5.74 +    thus ?thesis ..
    5.75 +  next
    5.76 +    assume "xs \<parallel> ys"
    5.77 +    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    5.78 +      and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    5.79 +      by blast
    5.80 +    from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
    5.81 +    with neq ys show ?thesis by blast
    5.82    qed
    5.83 -  thus ?thesis ..
    5.84  qed
    5.85  
    5.86  end