src/HOL/IMP/Collecting.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46334 3858dc8eabd8
child 47818 151d137f1095
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:
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     1
theory Collecting
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     2
imports Complete_Lattice_ix ACom
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     3
begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     4
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     5
subsection "Collecting Semantics of Commands"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     6
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     7
subsubsection "Annotated commands as a complete lattice"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     8
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     9
(* Orderings could also be lifted generically (thus subsuming the
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    10
instantiation for preord and order), but then less_eq_acom would need to
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    11
become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    12
need to unfold this defn first. *)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    13
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    14
instantiation acom :: (order) order
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    15
begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    16
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    17
fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
45885
nipkow
parents: 45655
diff changeset
    18
"(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
nipkow
parents: 45655
diff changeset
    19
"(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
nipkow
parents: 45655
diff changeset
    20
"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
nipkow
parents: 45655
diff changeset
    21
"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
nipkow
parents: 45655
diff changeset
    22
  (b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
nipkow
parents: 45655
diff changeset
    23
"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
nipkow
parents: 45655
diff changeset
    24
  (b=b' \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    25
"less_eq_acom _ _ = False"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    26
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    27
lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    28
by (cases c) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    29
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    30
lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    31
by (cases c) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    32
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    33
lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    34
by (cases c) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    35
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    36
lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    37
  (\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    38
by (cases c) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    39
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    40
lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    41
  (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    42
by (cases w) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    43
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    44
definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    45
"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    46
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    47
instance
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    48
proof
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    49
  case goal1 show ?case by(simp add: less_acom_def)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    50
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    51
  case goal2 thus ?case by (induct x) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    52
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    53
  case goal3 thus ?case
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    54
  apply(induct x y arbitrary: z rule: less_eq_acom.induct)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    55
  apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    56
  done
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    57
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    58
  case goal4 thus ?case
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    59
  apply(induct x y rule: less_eq_acom.induct)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    60
  apply (auto intro: le_antisym)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    61
  done
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    62
qed
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    63
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    64
end
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    65
45919
nipkow
parents: 45903
diff changeset
    66
fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
nipkow
parents: 45903
diff changeset
    67
"sub\<^isub>1(c1;c2) = c1" |
nipkow
parents: 45903
diff changeset
    68
"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
nipkow
parents: 45903
diff changeset
    69
"sub\<^isub>1({I} WHILE b DO c {P}) = c"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    70
45919
nipkow
parents: 45903
diff changeset
    71
fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
nipkow
parents: 45903
diff changeset
    72
"sub\<^isub>2(c1;c2) = c2" |
nipkow
parents: 45903
diff changeset
    73
"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    74
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    75
fun invar :: "'a acom \<Rightarrow> 'a" where
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    76
"invar({I} WHILE b DO c {P}) = I"
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    77
46116
b903d272c37d generalised type
nipkow
parents: 46070
diff changeset
    78
fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    79
where
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    80
"lift F com.SKIP M = (SKIP {F (post ` M)})" |
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    81
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    82
"lift F (c1;c2) M =
45919
nipkow
parents: 45903
diff changeset
    83
  lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    84
"lift F (IF b THEN c1 ELSE c2) M =
45919
nipkow
parents: 45903
diff changeset
    85
  IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    86
  {F (post ` M)}" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    87
"lift F (WHILE b DO c) M =
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    88
 {F (invar ` M)}
45919
nipkow
parents: 45903
diff changeset
    89
 WHILE b DO lift F c (sub\<^isub>1 ` M)
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    90
 {F (post ` M)}"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    91
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    92
interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    93
proof
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    94
  case goal1
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    95
  have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    96
  proof(induction a arbitrary: A)
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    97
    case Semi from Semi.prems show ?case by(force intro!: Semi.IH)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    98
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
    99
    case If from If.prems show ?case by(force intro!: If.IH)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   100
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   101
    case While from While.prems show ?case by(force intro!: While.IH)
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   102
  qed force+
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   103
  with goal1 show ?case by auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   104
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   105
  case goal2
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   106
  thus ?case
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   107
  proof(induction b arbitrary: i A)
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   108
    case SKIP thus ?case by (force simp:SKIP_le)
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   109
  next
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   110
    case Assign thus ?case by (force simp:Assign_le)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   111
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   112
    case Semi from Semi.prems show ?case
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   113
      by (force intro!: Semi.IH simp:Semi_le)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   114
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   115
    case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   116
  next
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   117
    case While from While.prems show ?case
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   118
      by(fastforce simp: While_le intro: While.IH)
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   119
  qed
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   120
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   121
  case goal3
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   122
  have "strip(lift Inter i A) = i"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   123
  proof(induction i arbitrary: A)
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   124
    case Semi from Semi.prems show ?case
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   125
      by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   126
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   127
    case If from If.prems show ?case
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   128
      by (fastforce intro!: If.IH simp: strip_eq_If)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   129
  next
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   130
    case While from While.prems show ?case
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   131
      by(fastforce intro: While.IH simp: strip_eq_While)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   132
  qed auto
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   133
  thus ?case by auto
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   134
qed
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   135
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   136
lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   137
by(induction c d rule: less_eq_acom.induct) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   138
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   139
subsubsection "Collecting semantics"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   140
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   141
fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   142
"step S (SKIP {P}) = (SKIP {S})" |
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   143
"step S (x ::= e {P}) =
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   144
  (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   145
"step S (c1; c2) = step S c1; step (post c1) c2" |
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   146
"step S (IF b THEN c1 ELSE c2 {P}) =
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   147
   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   148
   {post c1 \<union> post c2}" |
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   149
"step S ({Inv} WHILE b DO c {P}) =
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   150
  {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   151
46070
nipkow
parents: 46069
diff changeset
   152
definition CS :: "com \<Rightarrow> state set acom" where
nipkow
parents: 46069
diff changeset
   153
"CS c = lfp (step UNIV) c"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   154
46334
nipkow
parents: 46116
diff changeset
   155
lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
nipkow
parents: 46116
diff changeset
   156
proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   157
  case 2 thus ?case by fastforce
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   158
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   159
  case 3 thus ?case by(simp add: le_post)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   160
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   161
  case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   162
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   163
  case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   164
qed auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   165
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   166
lemma mono_step: "mono (step S)"
46334
nipkow
parents: 46116
diff changeset
   167
by(blast intro: monoI mono2_step)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   168
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   169
lemma strip_step: "strip(step S c) = strip c"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   170
by (induction c arbitrary: S) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   171
46066
e81411bfa7ef tuned argument order
nipkow
parents: 45919
diff changeset
   172
lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   173
apply(rule lfp_unfold[OF _  mono_step])
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   174
apply(simp add: strip_step)
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   175
done
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   176
46070
nipkow
parents: 46069
diff changeset
   177
lemma CS_unfold: "CS c = step UNIV (CS c)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   178
by (metis CS_def lfp_cs_unfold)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   179
46070
nipkow
parents: 46069
diff changeset
   180
lemma strip_CS[simp]: "strip(CS c) = c"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45885
diff changeset
   181
by(simp add: CS_def index_lfp[simplified])
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   182
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   183
end