src/HOL/MicroJava/BV/Kildall.thy
author paulson
Tue, 27 Jan 2004 15:39:51 +0100
changeset 14365 3d4df8c166ae
parent 14191 2014eac694d2
child 16417 9bc16273c2d4
permissions -rw-r--r--
replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
     1
(*  Title:      HOL/MicroJava/BV/Kildall.thy
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     2
    ID:         $Id$
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
     3
    Author:     Tobias Nipkow, Gerwin Klein
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     4
    Copyright   2000 TUM
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     5
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     6
Kildall's algorithm
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     7
*)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     8
12911
704713ca07ea new document
kleing
parents: 12516
diff changeset
     9
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    10
13062
4b1edf2f6bd2 small refactoring for lbv with semilattices
kleing
parents: 13006
diff changeset
    11
theory Kildall = SemilatAlg + While_Combinator:
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    12
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    13
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    14
consts
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    15
 iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
11298
acd83fa66e92 simplified defs and proofs a little
nipkow
parents: 11229
diff changeset
    16
          's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
    17
 propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    18
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    19
primrec
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    20
"propa f []      ss w = (ss,w)"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    21
"propa f (q'#qs) ss w = (let (q,t) = q';
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    22
                             u = t +_f ss!q;
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    23
                             w' = (if u = ss!q then w else insert q w)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    24
                         in propa f qs (ss[q := u]) w')"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    25
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
    26
defs iter_def:
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    27
"iter f step ss w ==
11298
acd83fa66e92 simplified defs and proofs a little
nipkow
parents: 11229
diff changeset
    28
 while (%(ss,w). w \<noteq> {})
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    29
       (%(ss,w). let p = SOME p. p \<in> w
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    30
                 in propa f (step p (ss!p)) ss (w-{p}))
11298
acd83fa66e92 simplified defs and proofs a little
nipkow
parents: 11229
diff changeset
    31
       (ss,w)"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    32
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    33
constdefs
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
    34
 unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    35
"unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    36
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
    37
 kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    38
"kildall r f step ss == fst(iter f step ss (unstables r step ss))"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    39
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
    40
consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    41
primrec
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    42
"merges f []      ss = ss"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    43
"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    44
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    45
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    46
lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    47
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    48
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    49
lemma (in semilat) nth_merges:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    50
 "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    51
  (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    52
  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    53
proof (induct ps)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    54
  show "\<And>ss. ?P ss []" by simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    55
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    56
  fix ss p' ps'
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    57
  assume ss: "ss \<in> list n A"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    58
  assume l:  "p < length ss"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    59
  assume "?steptype (p'#ps')"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    60
  then obtain a b where
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    61
    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?steptype ps'"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    62
    by (cases p', auto)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    63
  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    64
  hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    65
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    66
  from ss ab
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    67
  have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    68
  moreover
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    69
  from calculation
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    70
  have "p < length (ss[a := b +_f ss!a])" by simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    71
  ultimately
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    72
  have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    73
  with p' l
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    74
  show "?P ss (p'#ps')" by simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    75
qed
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    76
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    77
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    78
(** merges **)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    79
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    80
lemma length_merges [rule_format, simp]:
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    81
  "\<forall>ss. size(merges f ps ss) = size ss"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    82
  by (induct_tac ps, auto)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    83
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
    84
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    85
lemma (in semilat) merges_preserves_type_lemma:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    86
shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    87
          \<longrightarrow> merges f ps xs \<in> list n A"
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    88
apply (insert closedI)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    89
apply (unfold closed_def)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    90
apply (induct_tac ps)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    91
 apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    92
apply clarsimp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    93
done
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    94
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    95
lemma (in semilat) merges_preserves_type [simp]:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    96
 "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
    97
  \<Longrightarrow> merges f ps xs \<in> list n A"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    98
by (simp add: merges_preserves_type_lemma)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
    99
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   100
lemma (in semilat) merges_incr_lemma:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   101
 "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   102
apply (induct_tac ps)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   103
 apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   104
apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   105
apply clarify
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   106
apply (rule order_trans)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   107
  apply simp
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   108
 apply (erule list_update_incr)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   109
  apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   110
 apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   111
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   112
done
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   113
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   114
lemma (in semilat) merges_incr:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   115
 "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   116
  \<Longrightarrow> xs <=[r] merges f ps xs"
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   117
  by (simp add: merges_incr_lemma)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   118
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   119
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   120
lemma (in semilat) merges_same_conv [rule_format]:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   121
 "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   122
     (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   123
  apply (induct_tac ps)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   124
   apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   125
  apply clarsimp
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   126
  apply (rename_tac p x ps xs)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   127
  apply (rule iffI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   128
   apply (rule context_conjI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   129
    apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   130
     apply (force dest!: le_listD simp add: nth_list_update)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   131
    apply (erule subst, rule merges_incr)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   132
       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   133
      apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   134
      apply (rule conjI)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   135
       apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   136
       apply (blast dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   137
      apply blast
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   138
   apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   139
   apply (erule allE)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   140
   apply (erule impE)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   141
    apply assumption
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   142
   apply (drule bspec)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   143
    apply assumption
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   144
   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   145
   apply blast
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   146
  apply clarify 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   147
  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   148
  done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   149
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   150
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   151
lemma (in semilat) list_update_le_listI [rule_format]:
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   152
  "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   153
   x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   154
  apply(insert semilat)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   155
  apply (unfold Listn.le_def lesub_def semilat_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   156
  apply (simp add: list_all2_conv_all_nth nth_list_update)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   157
  done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   158
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   159
lemma (in semilat) merges_pres_le_ub:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   160
shows "\<lbrakk> set ts <= A; set ss <= A;
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   161
         \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   162
  \<Longrightarrow> merges f ps ss <=[r] ts"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   163
proof -
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   164
  { fix t ts ps
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   165
    have
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   166
    "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   167
    set qs <= set ps  \<longrightarrow> 
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   168
    (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   169
    apply (induct_tac qs)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   170
     apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   171
    apply (simp (no_asm_simp))
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   172
    apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   173
    apply (rotate_tac -2)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   174
    apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   175
    apply (erule allE, erule impE, erule_tac [2] mp)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   176
     apply (drule bspec, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   177
     apply (simp add: closedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   178
    apply (drule bspec, assumption)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   179
    apply (simp add: list_update_le_listI)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   180
    done 
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   181
  } note this [dest]
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   182
  
11549
e7265e70fd7c renamed "antecedent" case to "rule_context";
wenzelm
parents: 11299
diff changeset
   183
  case rule_context
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   184
  thus ?thesis by blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   185
qed
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   186
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   187
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   188
(** propa **)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   189
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   190
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   191
lemma decomp_propa:
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   192
  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   193
   propa f qs ss w = 
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   194
   (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   195
  apply (induct qs)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   196
   apply simp   
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   197
  apply (simp (no_asm))
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   198
  apply clarify  
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   199
  apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   200
  apply (rule conjI) 
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   201
   apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   202
  apply (simp add: nth_list_update)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   203
  apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   204
  done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   205
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   206
(** iter **)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   207
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   208
lemma (in semilat) stable_pres_lemma:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   209
shows "\<lbrakk>pres_type step n A; bounded step n; 
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   210
     ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   211
     \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   212
     \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   213
     q \<notin> w \<or> q = p \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   214
  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   215
  apply (unfold stable_def)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   216
  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   217
   prefer 2
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   218
   apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   219
   apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   220
    prefer 3 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   221
    apply (rule listE_nth_in)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   222
     apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   223
    apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   224
   apply simp
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   225
  apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   226
  apply clarify
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   227
  apply (subst nth_merges)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   228
       apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   229
       apply (blast dest: boundedD)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   230
      apply assumption
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   231
     apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   232
     apply (rule conjI)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   233
      apply (blast dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   234
     apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   235
       prefer 3 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   236
      apply simp
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   237
     apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   238
apply(subgoal_tac "q < length ss")
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   239
prefer 2 apply simp
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   240
  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   241
apply assumption
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   242
  apply clarify
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   243
  apply (rule conjI)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   244
   apply (blast dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   245
  apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   246
     prefer 3 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   247
    apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   248
   apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   249
  apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   250
   apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   251
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   252
 apply (simp add: plusplus_empty)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   253
 apply (cases "q \<in> w")
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   254
  apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   255
  apply (rule ub1')
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   256
     apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   257
    apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   258
    apply (rule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   259
       apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   260
      prefer 3 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   261
     apply (blast intro: listE_nth_in dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   262
    apply (blast intro: pres_typeD dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   263
   apply (blast intro: listE_nth_in dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   264
  apply assumption
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   265
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   266
 apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   267
 apply (erule allE, erule impE, assumption, erule impE, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   268
 apply (rule order_trans)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   269
   apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   270
  defer
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   271
 apply (rule pp_ub2)(*
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   272
    apply assumption*)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   273
   apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   274
   apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   275
   apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   276
   apply (rule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   277
      apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   278
     prefer 3 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   279
    apply (blast intro: listE_nth_in dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   280
   apply (blast intro: pres_typeD dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   281
  apply (blast intro: listE_nth_in dest: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   282
 apply blast
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   283
 done
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   284
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   285
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   286
lemma (in semilat) merges_bounded_lemma:
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   287
 "\<lbrakk> mono r step n A; bounded step n; 
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   288
    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   289
    ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
13066
b57d926d1de2 cleanup + simpler monotonicity
kleing
parents: 13062
diff changeset
   290
  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" 
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   291
  apply (unfold stable_def)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   292
  apply (rule merges_pres_le_ub)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   293
     apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   294
    apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   295
   prefer 2 apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   296
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   297
  apply clarsimp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   298
  apply (drule boundedD, assumption+)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   299
  apply (erule allE, erule impE, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   300
  apply (drule bspec, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   301
  apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   302
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   303
  apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   304
     apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   305
    apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   306
   apply (simp add: le_listD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   307
  
13066
b57d926d1de2 cleanup + simpler monotonicity
kleing
parents: 13062
diff changeset
   308
  apply (drule lesub_step_typeD, assumption) 
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   309
  apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   310
  apply (drule bspec, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   311
  apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   312
  apply (blast intro: order_trans)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   313
  done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   314
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   315
lemma termination_lemma: includes semilat
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   316
shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   317
      ss <[r] merges f qs ss \<or> 
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   318
  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   319
apply(insert semilat)
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   320
  apply (unfold lesssub_def)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   321
  apply (simp (no_asm_simp) add: merges_incr)
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   322
  apply (rule impI)
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   323
  apply (rule merges_same_conv [THEN iffD1, elim_format]) 
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   324
  apply assumption+
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   325
    defer
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   326
    apply (rule sym, assumption)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   327
   defer apply simp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   328
   apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   329
   apply (blast intro!: psubsetI elim: equalityE)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   330
   apply clarsimp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   331
   apply (drule bspec, assumption) 
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   332
   apply (drule bspec, assumption)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   333
   apply clarsimp
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   334
  done 
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   335
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   336
lemma iter_properties[rule_format]: includes semilat
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   337
shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   338
     bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   339
     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   340
   iter f step ss0 w0 = (ss',w')
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   341
   \<longrightarrow>
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   342
   ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   343
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   344
apply(insert semilat)
11298
acd83fa66e92 simplified defs and proofs a little
nipkow
parents: 11229
diff changeset
   345
apply (unfold iter_def stables_def)
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   346
apply (rule_tac P = "%(ss,w).
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   347
 ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   348
 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   349
 (\<forall>p\<in>w. p < n)" and
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   350
 r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   351
       in while_rule)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   352
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   353
-- "Invariant holds initially:"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   354
apply (simp add:stables_def)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   355
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   356
-- "Invariant is preserved:"
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   357
apply(simp add: stables_def split_paired_all)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   358
apply(rename_tac ss w)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   359
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   360
 prefer 2; apply (fast intro: someI)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   361
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   362
 prefer 2
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   363
 apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   364
 apply (rule conjI)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   365
  apply(clarsimp, blast dest!: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   366
 apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   367
  prefer 3
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   368
  apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   369
  apply (erule listE_nth_in)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14191
diff changeset
   370
  apply simp
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14191
diff changeset
   371
 apply simp
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   372
apply (subst decomp_propa)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14191
diff changeset
   373
 apply fast
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   374
apply simp
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   375
apply (rule conjI)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   376
 apply (rule merges_preserves_type)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   377
 apply blast
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   378
 apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   379
 apply (rule conjI)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14191
diff changeset
   380
  apply(clarsimp, fast dest!: boundedD)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   381
 apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   382
  prefer 3
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   383
  apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   384
  apply (erule listE_nth_in)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   385
  apply blast
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   386
 apply blast
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   387
apply (rule conjI)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   388
 apply clarify
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   389
 apply (blast intro!: stable_pres_lemma)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   390
apply (rule conjI)
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   391
 apply (blast intro!: merges_incr intro: le_list_trans)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   392
apply (rule conjI)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   393
 apply clarsimp
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   394
 apply (blast intro!: merges_bounded_lemma)
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   395
apply (blast dest!: boundedD)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   396
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   397
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   398
-- "Postcondition holds upon termination:"
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   399
apply(clarsimp simp add: stables_def split_paired_all)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   400
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   401
-- "Well-foundedness of the termination relation:"
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   402
apply (rule wf_lex_prod)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   403
 apply (insert orderI [THEN acc_le_listI])
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   404
 apply (simp only: acc_def lesssub_def)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   405
apply (rule wf_finite_psubset) 
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   406
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   407
-- "Loop decreases along termination relation:"
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   408
apply(simp add: stables_def split_paired_all)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   409
apply(rename_tac ss w)
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   410
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   411
 prefer 2; apply (fast intro: someI)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   412
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   413
 prefer 2
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   414
 apply clarify
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   415
 apply (rule conjI)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   416
  apply(clarsimp, blast dest!: boundedD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   417
 apply (erule pres_typeD)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   418
  prefer 3
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   419
  apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   420
  apply (erule listE_nth_in)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   421
  apply blast
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   422
 apply blast
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   423
apply (subst decomp_propa)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   424
 apply blast
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   425
apply clarify
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   426
apply (simp del: listE_length
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   427
    add: lex_prod_def finite_psubset_def 
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   428
         bounded_nat_set_is_finite)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   429
apply (rule termination_lemma)
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   430
apply assumption+
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   431
defer
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   432
apply assumption
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   433
apply clarsimp
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   434
done
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   435
11175
56ab6a5ba351 recoded function iter with the help of the while-combinator.
nipkow
parents: 10774
diff changeset
   436
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   437
lemma kildall_properties: includes semilat
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   438
shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   439
     bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   440
  kildall r f step ss0 \<in> list n A \<and>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   441
  stables r step (kildall r f step ss0) \<and>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   442
  ss0 <=[r] kildall r f step ss0 \<and>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   443
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   444
                 kildall r f step ss0 <=[r] ts)"
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   445
apply (unfold kildall_def)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   446
apply(case_tac "iter f step ss0 (unstables r step ss0)")
11298
acd83fa66e92 simplified defs and proofs a little
nipkow
parents: 11229
diff changeset
   447
apply(simp)
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   448
apply (rule iter_properties)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   449
by (simp_all add: unstables_def stable_def)
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   450
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   451
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   452
lemma is_bcv_kildall: includes semilat
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   453
shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
13006
51c5f3f11d16 symbolized
kleing
parents: 12911
diff changeset
   454
  \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
11299
1d3d110c456e welltyping -> wt_step
nipkow
parents: 11298
diff changeset
   455
apply(unfold is_bcv_def wt_step_def)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   456
apply(insert semilat kildall_properties[of A])
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   457
apply(simp add:stables_def)
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   458
apply clarify
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   459
apply(subgoal_tac "kildall r f step ss \<in> list n A")
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   460
 prefer 2 apply (simp(no_asm_simp))
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   461
apply (rule iffI)
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   462
 apply (rule_tac x = "kildall r f step ss" in bexI) 
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   463
  apply (rule conjI)
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   464
   apply (blast)
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   465
  apply (simp  (no_asm_simp))
13074
96bf406fd3e5 Started to convert to locales
nipkow
parents: 13066
diff changeset
   466
 apply(assumption)
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   467
apply clarify
12516
d09d0f160888 exceptions
kleing
parents: 11549
diff changeset
   468
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
11229
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   469
 apply simp
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   470
apply (blast intro!: le_listD less_lengthI)
f417841385b7 Got rid of is_dfa
nipkow
parents: 11184
diff changeset
   471
done
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   472
14191
2014eac694d2 Mod due to new thm in Map.
nipkow
parents: 13601
diff changeset
   473
end