author wenzelm Mon Nov 06 22:56:07 2000 +0100 (2000-11-06) changeset 10408 d8b3613158b1 parent 10407 998778f8d63b child 10409 10a1b95ce642
improved: 'induct' handle non-atomic goals;
 src/HOL/Isar_examples/Fibonacci.thy file | annotate | diff | revisions src/HOL/Isar_examples/Hoare.thy file | annotate | diff | revisions src/HOL/Isar_examples/MutilatedCheckerboard.thy file | annotate | diff | revisions src/HOL/Isar_examples/W_correct.thy file | annotate | diff | revisions src/HOL/Library/List_Prefix.thy file | annotate | diff | revisions
```     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
```