src/HOL/IMP/Abs_Int2.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46430 ead59736792b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     2
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     3
theory Abs_Int2
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     4
imports Abs_Int1_ivl
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     5
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     6
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     7
subsection "Widening and Narrowing"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     8
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     9
class WN = SL_top +
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    10
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    11
assumes widen1: "x \<sqsubseteq> x \<nabla> y"
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    12
assumes widen2: "y \<sqsubseteq> x \<nabla> y"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    13
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    14
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    15
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    16
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    17
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    18
subsubsection "Intervals"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    19
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    20
instantiation ivl :: WN
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    21
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    22
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    23
definition "widen_ivl ivl1 ivl2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    24
  ((*if is_empty ivl1 then ivl2 else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    25
   if is_empty ivl2 then ivl1 else*)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    26
     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    27
       I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    28
         (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    29
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    30
definition "narrow_ivl ivl1 ivl2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    31
  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    32
     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    33
       I (if l1 = None then l2 else l1)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    34
         (if h1 = None then h2 else h1))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    35
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    36
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    37
proof qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
  (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    39
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    41
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    42
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    43
subsubsection "Abstract State"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    44
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    45
instantiation st :: (WN)WN
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    47
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    48
definition "widen_st F1 F2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    49
  FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
definition "narrow_st F1 F2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    52
  FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    53
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    54
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    55
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    56
  case goal1 thus ?case
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    57
    by(simp add: widen_st_def le_st_def lookup_def widen1)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    59
  case goal2 thus ?case
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    60
    by(simp add: widen_st_def le_st_def lookup_def widen2)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    61
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    62
  case goal3 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    63
    by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    64
next
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    65
  case goal4 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    66
    by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    67
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    68
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    69
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    70
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    71
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    72
subsubsection "Option"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
    73
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    74
instantiation option :: (WN)WN
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    75
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    76
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    77
fun widen_option where
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    78
"None \<nabla> x = x" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    79
"x \<nabla> None = x" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    80
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    81
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    82
fun narrow_option where
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    83
"None \<triangle> x = None" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    84
"x \<triangle> None = None" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    85
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    86
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    87
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    88
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    89
  case goal1 show ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    90
    by(induct x y rule: widen_option.induct) (simp_all add: widen1)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    91
next
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    92
  case goal2 show ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    93
    by(induct x y rule: widen_option.induct) (simp_all add: widen2)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    94
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    95
  case goal3 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    96
    by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    97
next
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    98
  case goal4 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
    99
    by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   100
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   101
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   102
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   103
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   104
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   105
subsubsection "Annotated commands"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   106
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   107
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   108
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   109
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   110
"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   111
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   112
  (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   113
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   114
  ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   115
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   116
abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   117
where "widen_acom == map2_acom (op \<nabla>)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   118
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   119
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   120
where "narrow_acom == map2_acom (op \<triangle>)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   121
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   122
lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'"
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   123
by(induct c c' rule: le_acom.induct)(simp_all add: widen1)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   124
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   125
lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'"
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   126
by(induct c c' rule: le_acom.induct)(simp_all add: widen2)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   127
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   128
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   129
by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   130
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   131
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   132
by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   133
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   134
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   135
subsubsection "Post-fixed point computation"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   136
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   137
definition iter_widen :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> ('a::WN)acom option"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   138
where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla>\<^sub>c f c)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   139
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   140
definition iter_narrow :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a::WN acom option"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   141
where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) (\<lambda>c. c \<triangle>\<^sub>c f c)"
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   142
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   143
definition pfp_wn ::
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   144
  "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   145
where "pfp_wn f c = (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   146
                     | Some c' \<Rightarrow> iter_narrow f c')"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   147
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   148
lemma strip_map2_acom:
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   149
 "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   150
by(induct f c1 c2 rule: map2_acom.induct) simp_all
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   151
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   152
lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   153
by(auto simp add: iter_widen_def dest: while_option_stop)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   154
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   155
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   156
assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   157
shows "strip c' = strip c"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   158
using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)]
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   159
by (metis assms(1))
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   160
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   161
lemma strip_iter_widen: fixes f :: "'a::WN acom \<Rightarrow> 'a acom"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   162
assumes "\<forall>c. strip (f c) = strip c" and "iter_widen f c = Some c'"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   163
shows "strip c' = strip c"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   164
proof-
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   165
  have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   166
  from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   167
qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   168
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   169
lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   170
and "iter_narrow f c0 = Some c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   171
shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c")
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   172
proof-
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   173
  { fix c assume "?P c"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   174
    note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   175
    let ?c' = "c \<triangle>\<^sub>c f c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   176
    have "?P ?c'"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   177
    proof
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   178
      have "f ?c' \<sqsubseteq> f c"  by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   179
      also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1_acom[OF 1])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   180
      finally show "f ?c' \<sqsubseteq> ?c'" .
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   181
      have "?c' \<sqsubseteq> c" by (rule narrow2_acom[OF 1])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   182
      also have "c \<sqsubseteq> c0" by(rule 2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   183
      finally show "?c' \<sqsubseteq> c0" .
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   184
    qed
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   185
  }
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   186
  with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]]
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   187
    assms(2) le_refl
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   188
  show ?thesis by blast
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   189
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   190
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   191
lemma pfp_wn_pfp:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   192
  "\<lbrakk> mono f;  pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   193
unfolding pfp_wn_def
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   194
by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   195
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   196
lemma strip_pfp_wn:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   197
  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   198
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   199
by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   200
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   201
locale Abs_Int2 = Abs_Int1_mono
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   202
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   203
begin
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   204
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   205
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   206
"AI_wn = pfp_wn (step' \<top>)"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   207
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   208
lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   209
proof(simp add: CS_def AI_wn_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   210
  assume 1: "pfp_wn (step' \<top>) c = Some c'"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   211
  from pfp_wn_pfp[OF mono_step'2 1]
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   212
  have 2: "step' \<top> c' \<sqsubseteq> c'" .
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   213
  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1])
46066
e81411bfa7ef tuned argument order
nipkow
parents: 46063
diff changeset
   214
  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45655
diff changeset
   215
  proof(rule lfp_lowerbound[simplified,OF 3])
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   216
    show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
46068
b9d4ec0f79ac tuned proofs
nipkow
parents: 46066
diff changeset
   217
    proof(rule step_preserves_le[OF _ _])
46039
nipkow
parents: 45903
diff changeset
   218
      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
nipkow
parents: 45903
diff changeset
   219
      show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   220
    qed
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   221
  qed
46066
e81411bfa7ef tuned argument order
nipkow
parents: 46063
diff changeset
   222
  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
46039
nipkow
parents: 45903
diff changeset
   223
    by (blast intro: mono_gamma_c order_trans)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   224
qed
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   225
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   226
end
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   227
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   228
interpretation Abs_Int2
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   229
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46430
ead59736792b simplified code generation
nipkow
parents: 46387
diff changeset
   230
and test_num' = in_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   231
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   232
defines AI_ivl' is AI_wn
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46303
diff changeset
   233
..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   234
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   235
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   236
subsubsection "Tests"
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   237
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   238
definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
   239
definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   240
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   241
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
46303
nipkow
parents: 46251
diff changeset
   242
the loop took to execute. In contrast, @{const AI_ivl'} converges in a
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   243
constant number of steps: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   244
46303
nipkow
parents: 46251
diff changeset
   245
value "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
nipkow
parents: 46251
diff changeset
   246
value "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
nipkow
parents: 46251
diff changeset
   247
value "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
nipkow
parents: 46251
diff changeset
   248
value "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
nipkow
parents: 46251
diff changeset
   249
value "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
nipkow
parents: 46251
diff changeset
   250
value "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
nipkow
parents: 46251
diff changeset
   251
value "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
nipkow
parents: 46251
diff changeset
   252
value "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   253
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   254
text{* Now all the analyses terminate: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   255
46303
nipkow
parents: 46251
diff changeset
   256
value "show_acom_opt (AI_ivl' test4_ivl)"
nipkow
parents: 46251
diff changeset
   257
value "show_acom_opt (AI_ivl' test5_ivl)"
nipkow
parents: 46251
diff changeset
   258
value "show_acom_opt (AI_ivl' test6_ivl)"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   259
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   260
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   261
subsubsection "Termination: Intervals"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   262
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   263
definition m_ivl :: "ivl \<Rightarrow> nat" where
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   264
"m_ivl ivl = (case ivl of I l h \<Rightarrow>
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   265
     (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   266
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   267
lemma m_ivl_height: "m_ivl ivl \<le> 2"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   268
by(simp add: m_ivl_def split: ivl.split option.split)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   269
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   270
lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   271
by(auto simp: m_ivl_def le_option_def le_ivl_def
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   272
        split: ivl.split option.split if_splits)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   273
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   274
lemma m_ivl_widen:
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   275
  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   276
by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   277
        split: ivl.splits option.splits if_splits)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   278
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   279
lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   280
by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   281
        split: ivl.split option.split if_splits)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   282
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   283
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   284
definition n_ivl :: "ivl \<Rightarrow> nat" where
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   285
"n_ivl ivl = 2 - m_ivl ivl"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   286
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   287
lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   288
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   289
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   290
lemma n_ivl_narrow:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   291
  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   292
by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   293
        split: ivl.splits option.splits if_splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   294
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   295
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   296
subsubsection "Termination: Abstract State"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   297
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   298
definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   299
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   300
lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   301
shows "m_st m_ivl S \<le> 2 * card X"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   302
proof(auto simp: m_st_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   303
  have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _")
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   304
    by(rule setsum_mono)(simp add:m_ivl_height)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   305
  also have "\<dots> \<le> (\<Sum>x\<in>X. 2)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   306
    by(rule setsum_mono3[OF assms]) simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   307
  also have "\<dots> = 2 * card X" by(simp add: setsum_constant)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   308
  finally show "?L \<le> \<dots>" .
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   309
qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   310
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   311
lemma m_st_anti_mono:
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   312
  "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   313
proof(auto simp: m_st_def le_st_def lookup_def split: if_splits)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   314
  let ?X = "set(dom S1)" let ?Y = "set(dom S2)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   315
  let ?f = "fun S1" let ?g = "fun S2"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   316
  assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   317
  hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)" by(simp add: m_ivl_anti_mono)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   318
  have 0: "\<forall>x\<in>?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   319
  have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y-?X) \<union> (?Y\<inter>?X). m_ivl(?g y))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   320
    by (metis Un_Diff_Int)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   321
  also have "\<dots> = (\<Sum>y\<in>?Y-?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   322
    by(subst setsum_Un_disjoint) auto
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   323
  also have "(\<Sum>y\<in>?Y-?X. m_ivl(?g y)) = 0" using 0 by simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   324
  also have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" by simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   325
  also have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   326
    by(rule setsum_mono)(simp add: 1)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   327
  also have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   328
    by(simp add: setsum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2])
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   329
  finally show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   330
    by (metis add_less_cancel_left)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   331
qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   332
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   333
lemma m_st_widen:
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   334
assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   335
proof-
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   336
  { let ?X = "set(dom S1)" let ?Y = "set(dom S2)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   337
    let ?f = "fun S1" let ?g = "fun S2"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   338
    fix x assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   339
    have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R")
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   340
    proof cases
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   341
      assume "x : ?Y"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   342
      have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   343
      proof(rule setsum_strict_mono1, simp)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   344
        show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   345
          by (metis m_ivl_anti_mono widen1)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   346
      next
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   347
        show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   348
          using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x`
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   349
          by (metis IntI m_ivl_widen lookup_def)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   350
      qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   351
      also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1])
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   352
      finally show ?thesis .
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   353
    next
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   354
      assume "x ~: ?Y"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   355
      have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   356
      proof(rule setsum_mono, simp)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   357
        fix x assume "x:?X \<and> x:?Y" show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   358
          by (metis m_ivl_anti_mono widen1)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   359
      qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   360
      also have "\<dots> < m_ivl(?f x) + \<dots>"
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   361
        using m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`]
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   362
        by (metis Nat.le_refl add_strict_increasing gr0I not_less0)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   363
      also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   364
        using `x ~: ?Y` by simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   365
      also have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   366
        by(rule setsum_mono3)(insert `x:?X`, auto)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   367
      finally show ?thesis .
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   368
    qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   369
  } with assms show ?thesis
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   370
    by(auto simp: le_st_def widen_st_def m_st_def Int_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   371
qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   372
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   373
definition "n_st m X st = (\<Sum>x\<in>X. m(lookup st x))"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   374
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   375
lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   376
shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   377
proof-
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   378
  have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   379
    apply(rule setsum_mono) using assms
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   380
    by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   381
  thus ?thesis by(simp add: n_st_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   382
qed
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   383
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   384
lemma n_st_narrow:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   385
assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   386
and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   387
shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   388
proof-
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   389
  have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   390
    using assms(2-4)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   391
    by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   392
            split: if_splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   393
  have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   394
    using assms(2-5)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   395
    by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   396
            split: if_splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   397
  have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   398
    apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   399
  thus ?thesis by(simp add: n_st_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   400
qed
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   401
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   402
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   403
subsubsection "Termination: Option"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   404
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   405
definition "m_o m n opt = (case opt of None \<Rightarrow> n+1 | Some x \<Rightarrow> m x)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   406
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   407
lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow>
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   408
  m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   409
apply(induction S1 S2 rule: le_option.induct)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   410
apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   411
           split: option.splits)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   412
done
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   413
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   414
lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   415
  m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1"
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   416
by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   417
        split: option.split)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   418
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   419
definition "n_o n opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n x + 1)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   420
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   421
lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   422
  n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   423
apply(induction S1 S2 rule: le_option.induct)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   424
apply(auto simp: domo_def n_o_def n_st_mono
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   425
           split: option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   426
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   427
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   428
lemma n_o_narrow:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   429
  "\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   430
  \<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   431
apply(induction S1 S2 rule: narrow_option.induct)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   432
apply(auto simp: n_o_def domo_def n_st_narrow)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   433
done
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   434
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   435
lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   436
apply(induction S1 S2 rule: widen_option.induct)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   437
apply (auto simp: domo_def widen_st_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   438
done
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   439
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   440
lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   441
apply(induction S1 S2 rule: narrow_option.induct)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   442
apply (auto simp: domo_def narrow_st_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   443
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   444
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   445
subsubsection "Termination: Commands"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   446
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   447
lemma strip_widen_acom[simp]:
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   448
  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<nabla>\<^sub>c c') = strip c"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   449
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   450
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   451
lemma strip_narrow_acom[simp]:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   452
  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<triangle>\<^sub>c c') = strip c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   453
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   454
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   455
lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   456
  annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   457
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   458
  (simp_all add: size_annos_same2)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   459
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   460
lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   461
  annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   462
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   463
  (simp_all add: size_annos_same2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   464
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   465
lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   466
  c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X"
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   467
apply(auto simp add: Com_def)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   468
apply(rename_tac S S' x)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   469
apply(erule in_set_zipE)
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   470
apply(auto simp: domo_def split: option.splits)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   471
apply(case_tac S)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   472
apply(case_tac S')
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   473
apply simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   474
apply fastforce
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   475
apply(case_tac S')
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   476
apply fastforce
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   477
apply (fastforce simp: widen_st_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   478
done
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   479
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   480
lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   481
  c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   482
apply(auto simp add: Com_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   483
apply(rename_tac S S' x)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   484
apply(erule in_set_zipE)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   485
apply(auto simp: domo_def split: option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   486
apply(case_tac S)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   487
apply(case_tac S')
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   488
apply simp
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   489
apply fastforce
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   490
apply(case_tac S')
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   491
apply fastforce
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   492
apply (fastforce simp: narrow_st_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   493
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   494
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   495
definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   496
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   497
lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'\<Colon>ivl st option acom.
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   498
     strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse>
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   499
    \<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   500
apply(auto simp: m_c_def Let_def Com_def)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   501
apply(subgoal_tac "length(annos c') = length(annos c)")
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   502
prefer 2 apply (simp add: size_annos_same2)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   503
apply (auto)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   504
apply(rule setsum_strict_mono1)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   505
apply simp
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   506
apply (clarsimp)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   507
apply(erule m_o_anti_mono)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   508
apply(rule subset_trans[OF domo_widen_subset])
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   509
apply fastforce
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   510
apply(rule widen1)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   511
apply(auto simp: le_iff_le_annos listrel_iff_nth)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   512
apply(rule_tac x=n in bexI)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   513
prefer 2 apply simp
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   514
apply(erule m_o_widen)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   515
apply (simp)+
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   516
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   517
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   518
lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'.
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   519
  strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   520
  \<subseteq> measure(m_c(n_o (n_st n_ivl X)))"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   521
apply(auto simp: m_c_def Let_def Com_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   522
apply(subgoal_tac "length(annos c') = length(annos c)")
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   523
prefer 2 apply (simp add: size_annos_same2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   524
apply (auto)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   525
apply(rule setsum_strict_mono1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   526
apply simp
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   527
apply (clarsimp)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   528
apply(rule n_o_mono)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   529
using domo_narrow_subset apply fastforce
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   530
apply fastforce
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   531
apply(rule narrow2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   532
apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   533
apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   534
apply(rule_tac x=n in bexI)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   535
prefer 2 apply simp
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   536
apply(erule n_o_narrow)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   537
apply (simp)+
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   538
done
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   539
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   540
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   541
subsubsection "Termination: Post-Fixed Point Iterations"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   542
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   543
lemma iter_widen_termination:
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   544
fixes c0 :: "'a::WN acom"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   545
assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   546
assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   547
and "wf({(c::'a acom,c \<nabla>\<^sub>c c')|c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^-1)"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   548
and "P c0" and "c0 \<sqsubseteq> f c0" shows "EX c. iter_widen f c0 = Some c"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   549
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"])
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   550
  show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}"
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   551
    apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   552
next
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   553
  show "P c0" by(rule `P c0`)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   554
next
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   555
  fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   556
qed
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   557
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   558
lemma iter_narrow_termination:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   559
assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   560
and wf: "wf({(c, c \<triangle>\<^sub>c f c)|c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^-1)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   561
and "P c0" shows "EX c. iter_narrow f c0 = Some c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   562
proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   563
  show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   564
    apply(rule wf_subset[OF wf]) by(blast intro: P_f)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   565
next
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   566
  show "P c0" by(rule `P c0`)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   567
next
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   568
  fix c assume "P c" thus "P (c \<triangle>\<^sub>c f c)" by(simp add: P_f)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   569
qed
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   570
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   571
lemma iter_winden_step_ivl_termination:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   572
  "EX c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c"
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   573
apply(rule iter_widen_termination[where
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   574
  P = "%c. strip c = c0 \<and> c : Com(vars c0)"])
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   575
apply (simp_all add: step'_Com bot_acom)
46249
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   576
apply(rule wf_subset)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   577
apply(rule wf_measure)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   578
apply(rule subset_trans)
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   579
prefer 2
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   580
apply(rule measure_m_c[where X = "vars c0", OF finite_cvars])
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   581
apply blast
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   582
done
9f39ae84b593 Added termination proof for widening
nipkow
parents: 46153
diff changeset
   583
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   584
lemma iter_narrow_step_ivl_termination:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   585
  "c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow>
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   586
  EX c. iter_narrow (step_ivl \<top>) c0 = Some c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   587
apply(rule iter_narrow_termination[where
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   588
  P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   589
apply (simp_all add: step'_Com)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   590
apply(clarify)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   591
apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   592
apply assumption
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   593
apply(rule wf_subset)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   594
apply(rule wf_measure)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   595
apply(rule subset_trans)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   596
prefer 2
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   597
apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars])
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   598
apply auto
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   599
by (metis bot_least domo_Top order_refl step'_Com strip_step')
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   600
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   601
(* FIXME: simplify type system: Combine Com(X) and vars <= X?? *)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   602
lemma while_Com:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   603
fixes c :: "'a st option acom"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   604
assumes "while_option P f c = Some c'"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   605
and "!!c. strip(f c) = strip c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   606
and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   607
and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   608
using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   609
by(simp add: assms(2-))
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   610
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   611
lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   612
assumes "iter_widen f c = Some c'"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   613
and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   614
and "!!c. strip(f c) = strip c"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   615
and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   616
proof-
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   617
  have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   618
    by (metis (full_types) widen_acom_Com assms(2,3))
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   619
  from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   620
  show ?thesis using assms(3) by(simp)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   621
qed
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   622
46387
nipkow
parents: 46355
diff changeset
   623
nipkow
parents: 46355
diff changeset
   624
context Abs_Int2
nipkow
parents: 46355
diff changeset
   625
begin
nipkow
parents: 46355
diff changeset
   626
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   627
lemma iter_widen_step'_Com:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   628
  "iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   629
   \<Longrightarrow> c' : Com(X)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   630
apply(subgoal_tac "strip c'= strip c")
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   631
prefer 2 apply (metis strip_iter_widen strip_step')
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   632
apply(drule iter_widen_Com)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   633
prefer 3 apply assumption
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   634
prefer 3 apply assumption
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   635
apply (auto simp: step'_Com)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   636
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   637
46387
nipkow
parents: 46355
diff changeset
   638
end
nipkow
parents: 46355
diff changeset
   639
nipkow
parents: 46355
diff changeset
   640
theorem AI_ivl'_termination:
nipkow
parents: 46355
diff changeset
   641
  "EX c'. AI_ivl' c = Some c'"
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   642
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   643
apply(rule iter_narrow_step_ivl_termination)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   644
apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step')
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   645
apply(erule iter_widen_pfp)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   646
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   647
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   648
end
46251
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   649
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   650
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   651
(* interesting(?) relic
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   652
lemma widen_assoc:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   653
  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   654
apply(cases x)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   655
apply(cases y)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   656
apply(cases z)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   657
apply(rename_tac x1 x2 y1 y2 z1 z2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   658
apply(simp add: le_ivl_def)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   659
apply(case_tac x1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   660
apply(case_tac x2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   661
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   662
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   663
apply(case_tac x2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   664
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   665
apply(case_tac y1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   666
apply(case_tac y2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   667
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   668
apply(case_tac z1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   669
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   670
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   671
apply(case_tac y2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   672
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   673
apply(case_tac z1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   674
apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   675
apply(case_tac z2)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   676
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   677
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   678
done
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   679
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   680
lemma widen_step_trans:
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   681
  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x"
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   682
by (metis widen_assoc preord_class.le_trans widen1)
8fbcbcf4380e added termination of narrowing
nipkow
parents: 46249
diff changeset
   683
*)