src/HOL/Imperative_HOL/ex/List_Sublist.thy
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62058
1cfd5d604937 updated headers;
wenzelm
parents: 61702
diff changeset
     1
(*  Title:      HOL/Imperative_HOL/ex/List_Sublist.thy
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 32960
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 32960
diff changeset
     3
*)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
     4
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62058
diff changeset
     5
section \<open>Slices of lists\<close>
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
     6
61702
2e89bc578935 misc. changes to Imperative-HOL from Peter Gammie
Lars Hupel <lars.hupel@mytum.de>
parents: 60515
diff changeset
     7
theory List_Sublist
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 65956
diff changeset
     8
imports "HOL-Library.Multiset"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
     9
begin
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    10
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    11
lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" 
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    12
apply (induct xs arbitrary: i j k)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    13
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    14
apply (simp only: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    15
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    16
apply safe
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    17
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    18
apply (erule_tac x="0" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    19
apply (erule_tac x="j - 1" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    20
apply (erule_tac x="k - 1" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    21
apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    22
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    23
apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    24
apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    25
apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    26
apply simp
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    27
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    28
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    29
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    30
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    31
apply (erule_tac x="i - 1" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    32
apply (erule_tac x="j - 1" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    33
apply (erule_tac x="k - 1" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    34
apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    35
apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    36
apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    37
apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    38
apply simp
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    39
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    40
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    41
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
    42
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    43
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    44
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    45
lemma nths_update1: "i \<notin> inds \<Longrightarrow> nths (xs[i := v]) inds = nths xs inds"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    46
apply (induct xs arbitrary: i inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    47
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    48
apply (case_tac i)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    49
apply (simp add: nths_Cons)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    50
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    51
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    52
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    53
lemma nths_update2: "i \<in> inds \<Longrightarrow> nths (xs[i := v]) inds = (nths xs inds)[(card {k \<in> inds. k < i}):= v]"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    54
proof (induct xs arbitrary: i inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    55
  case Nil thus ?case by simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    56
next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    57
  case (Cons x xs)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    58
  thus ?case
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    59
  proof (cases i)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    60
    case 0 with Cons show ?thesis by (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    61
  next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    62
    case (Suc i')
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    63
    with Cons show ?thesis
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    64
      apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    65
      apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    66
      apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    67
      apply (auto simp add: nat.split)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    68
      apply (simp add: card_less_Suc[symmetric])
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    69
      apply (simp add: card_less_Suc2)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    70
      done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    71
  qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    72
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    73
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    74
lemma nths_update: "nths (xs[i := v]) inds = (if i \<in> inds then (nths xs inds)[(card {k \<in> inds. k < i}) := v] else nths xs inds)"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    75
by (simp add: nths_update1 nths_update2)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    76
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    77
lemma nths_take: "nths xs {j. j < m} = take m xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    78
apply (induct xs arbitrary: m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    79
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    80
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    81
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    82
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    83
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    84
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    85
lemma nths_take': "nths xs {0..<m} = take m xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    86
apply (induct xs arbitrary: m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    87
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    88
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    89
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    90
apply (simp add: nths_Cons nths_take)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    91
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    92
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    93
lemma nths_all[simp]: "nths xs {j. j < length xs} = xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    94
apply (induct xs)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    95
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    96
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    97
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
    98
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
    99
lemma nths_all'[simp]: "nths xs {0..<length xs} = xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   100
apply (induct xs)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   101
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   102
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   103
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   104
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   105
lemma nths_single: "a < length xs \<Longrightarrow> nths xs {a} = [xs ! a]"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   106
apply (induct xs arbitrary: a)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   107
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   108
apply(case_tac aa)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   109
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   110
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   111
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   112
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   113
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   114
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   115
lemma nths_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> nths xs inds = []" 
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   116
apply (induct xs arbitrary: inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   117
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   118
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   119
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   120
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   121
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   122
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   123
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   124
lemma nths_Nil': "nths xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   125
apply (induct xs arbitrary: inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   126
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   127
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   128
apply (auto split: if_splits)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   129
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   130
apply (case_tac x, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   131
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   132
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   133
lemma nths_Nil[simp]: "(nths xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   134
apply (induct xs arbitrary: inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   135
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   136
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   137
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   138
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   139
apply (case_tac x, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   140
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   141
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   142
lemma nths_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; nths xs inds = nths ys inds \<rbrakk> \<Longrightarrow> nths xs inds' = nths ys inds'"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   143
apply (induct xs arbitrary: ys inds inds')
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   144
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   145
apply (drule sym, rule sym)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   146
apply (simp add: nths_Nil, fastforce)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   147
apply (case_tac ys)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   148
apply (simp add: nths_Nil, fastforce)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   149
apply (auto simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   150
apply (erule_tac x="list" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   151
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   152
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
   153
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   154
apply (erule_tac x="list" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   155
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   156
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
   157
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   158
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   159
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   160
lemma nths_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> nths xs inds = nths ys inds"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   161
apply (induct xs arbitrary: ys inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   162
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   163
apply (rule sym, simp add: nths_Nil)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   164
apply (case_tac ys)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   165
apply (simp add: nths_Nil)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   166
apply (auto simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   167
apply (erule_tac x="list" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   168
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
   169
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   170
apply (erule_tac x="list" in meta_allE)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   171
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
   172
apply fastforce
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   173
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   174
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   175
lemma nths_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> nths xs inds = nths ys inds"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   176
by (rule nths_eq, auto)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   177
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   178
lemma nths_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (nths xs inds = nths ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   179
apply (induct xs arbitrary: ys inds)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   180
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   181
apply (rule sym, simp add: nths_Nil)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   182
apply (case_tac ys)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   183
apply (simp add: nths_Nil)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   184
apply (auto simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   185
apply (case_tac i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   186
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   187
apply (case_tac i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   188
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   189
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   190
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   191
section \<open>Another nths function\<close>
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   192
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   193
function nths' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   194
where
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   195
  "nths' n m [] = []"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   196
| "nths' n 0 xs = []"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   197
| "nths' 0 (Suc m) (x#xs) = (x#nths' 0 m xs)"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   198
| "nths' (Suc n) (Suc m) (x#xs) = nths' n m xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   199
by pat_completeness auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   200
termination by lexicographic_order
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   201
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   202
subsection \<open>Proving equivalence to the other nths command\<close>
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   203
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   204
lemma nths'_nths: "nths' n m xs = nths xs {j. n \<le> j \<and> j < m}"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   205
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   206
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   207
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   208
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   209
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   210
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   211
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   212
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   213
apply (simp add: nths_Cons)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   214
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   215
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   216
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   217
lemma "nths' n m xs = nths xs {n..<m}"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   218
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   219
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   220
apply (case_tac n, case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   221
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   222
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   223
apply (simp add: nths_take')
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   224
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   225
apply simp
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   226
apply (simp add: nths_Cons nths'_nths)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   227
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   228
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   229
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62058
diff changeset
   230
subsection \<open>Showing equivalence to use of drop and take for definition\<close>
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   231
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   232
lemma "nths' n m xs = take (m - n) (drop n xs)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   233
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   234
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   235
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   236
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   237
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   238
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   239
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   240
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   241
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   242
subsection \<open>General lemma about nths\<close>
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   243
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   244
lemma nths'_Nil[simp]: "nths' i j [] = []"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   245
by simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   246
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   247
lemma nths'_Cons[simp]: "nths' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # nths' 0 j xs) | Suc i' \<Rightarrow>  nths' i' j xs)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   248
by (cases i) auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   249
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   250
lemma nths'_Cons2[simp]: "nths' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ nths' (i - 1) (j - 1) xs))"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   251
apply (cases j)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   252
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   253
apply (cases i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   254
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   255
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   256
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   257
lemma nths_n_0: "nths' n 0 xs = []"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   258
by (induct xs, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   259
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   260
lemma nths'_Nil': "n \<ge> m \<Longrightarrow> nths' n m xs = []"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   261
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   262
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   263
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   264
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   265
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   266
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   267
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   268
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   269
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   270
lemma nths'_Nil2: "n \<ge> length xs \<Longrightarrow> nths' n m xs = []"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   271
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   272
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   273
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   274
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   275
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   276
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   277
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   278
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   279
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   280
lemma nths'_Nil3: "(nths' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   281
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   282
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   283
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   284
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   285
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   286
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   287
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   288
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   289
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   290
lemma nths'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> nths' n m xs \<noteq> []"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   291
apply (induct xs arbitrary: n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   292
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   293
apply (case_tac m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   294
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   295
apply (case_tac n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   296
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   297
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   298
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   299
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   300
lemma nths'_single: "n < length xs \<Longrightarrow> nths' n (Suc n) xs = [xs ! n]"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   301
apply (induct xs arbitrary: n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   302
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   303
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   304
apply (case_tac n)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   305
apply (simp add: nths_n_0)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   306
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   307
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   308
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   309
lemma nths'_update1: "i \<ge> m \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   310
apply (induct xs arbitrary: n m i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   311
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   312
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   313
apply (case_tac i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   314
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   315
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   316
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   317
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   318
lemma nths'_update2: "i < n \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   319
apply (induct xs arbitrary: n m i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   320
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   321
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   322
apply (case_tac i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   323
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   324
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   325
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   326
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   327
lemma nths'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> nths' n m (xs[i := v]) = (nths' n m xs)[i - n := v]"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   328
proof (induct xs arbitrary: n m i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   329
  case Nil thus ?case by auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   330
next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   331
  case (Cons x xs)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   332
  thus ?case
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   333
    apply -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   334
    apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   335
    apply (cases i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   336
    apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   337
    apply (cases i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   338
    apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   339
    done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   340
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   341
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   342
lemma "\<lbrakk> nths' i j xs = nths' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> nths' n m xs = nths' n m ys"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   343
proof (induct xs arbitrary: i j ys n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   344
  case Nil
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   345
  thus ?case
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   346
    apply -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   347
    apply (rule sym, drule sym)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   348
    apply (simp add: nths'_Nil)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   349
    apply (simp add: nths'_Nil3)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   350
    apply arith
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   351
    done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   352
next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   353
  case (Cons x xs i j ys n m)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   354
  note c = this
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   355
  thus ?case
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   356
  proof (cases m)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   357
    case 0 thus ?thesis by (simp add: nths_n_0)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   358
  next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   359
    case (Suc m')
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   360
    note a = this
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   361
    thus ?thesis
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   362
    proof (cases n)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   363
      case 0 note b = this
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   364
      show ?thesis
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   365
      proof (cases ys)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   366
        case Nil  with a b Cons.prems show ?thesis by (simp add: nths'_Nil3)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   367
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   368
        case (Cons y ys)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   369
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   370
        proof (cases j)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   371
          case 0 with a b Cons.prems show ?thesis by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   372
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   373
          case (Suc j') with a b Cons.prems Cons show ?thesis 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   374
            apply -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   375
            apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   376
            done
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   377
        qed
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   378
      qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   379
    next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   380
      case (Suc n')
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   381
      show ?thesis
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   382
      proof (cases ys)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   383
        case Nil with Suc a Cons.prems show ?thesis by (auto simp add: nths'_Nil3)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   384
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   385
        case (Cons y ys) with Suc a Cons.prems show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   386
          apply -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   387
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   388
          apply (cases j)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   389
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   390
          apply (cases i)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   391
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   392
          apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   393
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   394
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   395
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   396
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   397
          apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   398
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   399
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   400
          apply simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32580
diff changeset
   401
          done
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   402
      qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   403
    qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   404
  qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   405
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   406
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   407
lemma length_nths': "j \<le> length xs \<Longrightarrow> length (nths' i j xs) = j - i"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   408
by (induct xs arbitrary: i j, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   409
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   410
lemma nths'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> nths' i j xs = xs ! i # nths' (Suc i) j xs"
45129
1fce03e3e8ad tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents: 44890
diff changeset
   411
apply (induct xs arbitrary: i j)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   412
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   413
apply (case_tac j)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   414
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   415
apply (case_tac i)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   416
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   417
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   418
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   419
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   420
lemma nths'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> nths' i j xs = nths' i (j - 1) xs @ [xs ! (j - 1)]"
45129
1fce03e3e8ad tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents: 44890
diff changeset
   421
apply (induct xs arbitrary: i j)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   422
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   423
apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   424
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   425
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   426
(* suffices that j \<le> length xs and length ys *) 
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   427
lemma nths'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (nths' i j xs  = nths' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   428
proof (induct xs arbitrary: ys i j)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   429
  case Nil thus ?case by simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   430
next
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   431
  case (Cons x xs)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   432
  thus ?case
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   433
    apply -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   434
    apply (cases ys)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   435
    apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   436
    apply simp
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   437
    apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   438
    apply (case_tac i', auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   439
    apply (erule_tac x="Suc i'" in allE, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   440
    apply (erule_tac x="i' - 1" in allE, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   441
    apply (erule_tac x="Suc i'" in allE, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   442
    done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   443
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   444
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   445
lemma nths'_all[simp]: "nths' 0 (length xs) xs = xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   446
by (induct xs, auto)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   447
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   448
lemma nths'_nths': "nths' n m (nths' i j xs) = nths' (i + n) (min (i + m) j) xs" 
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   449
by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   450
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   451
lemma nths'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(nths' i j xs) @ (nths' j k xs) = nths' i k xs"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   452
by (induct xs arbitrary: i j k) auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   453
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   454
lemma nth_nths': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (nths' i j xs) ! k = xs ! (i + k)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   455
apply (induct xs arbitrary: i j k)
41842
d8f76db6a207 added simp lemma nth_Cons_pos to List
nipkow
parents: 41413
diff changeset
   456
apply simp
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   457
apply (case_tac k)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   458
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   459
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   460
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   461
lemma set_nths': "set (nths' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   462
apply (simp add: nths'_nths)
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   463
apply (simp add: set_nths)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   464
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   465
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   466
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   467
lemma all_in_set_nths'_conv: "(\<forall>j. j \<in> set (nths' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   468
unfolding set_nths' by blast
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   469
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   470
lemma ball_in_set_nths'_conv: "(\<forall>j \<in> set (nths' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   471
unfolding set_nths' by blast
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   472
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   473
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   474
lemma mset_nths:
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   475
assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   476
assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   477
assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 58889
diff changeset
   478
assumes multiset: "mset xs = mset ys"
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   479
  shows "mset (nths' l r xs) = mset (nths' l r ys)"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   480
proof -
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   481
  from l_r have xs_def: "xs = (nths' 0 l xs) @ (nths' l r xs) @ (nths' r (List.length xs) xs)" (is "_ = ?xs_long") 
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   482
    by (simp add: nths'_append)
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 58889
diff changeset
   483
  from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   484
  with l_r have ys_def: "ys = (nths' 0 l ys) @ (nths' l r ys) @ (nths' r (List.length ys) ys)" (is "_ = ?ys_long") 
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   485
    by (simp add: nths'_append)
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 58889
diff changeset
   486
  from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   487
  moreover
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   488
  from left l_r length_eq have "nths' 0 l xs = nths' 0 l ys"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   489
    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   490
  moreover
65956
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   491
  from right l_r length_eq have "nths' r (List.length xs) xs = nths' r (List.length ys) ys"
639eb3617a86 reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents: 63167
diff changeset
   492
    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 58889
diff changeset
   493
  ultimately show ?thesis by (simp add: mset_append)
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   494
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   495
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   496
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff changeset
   497
end