src/HOL/IMP/Abs_Int2.thy
author nipkow
Wed, 01 May 2013 03:56:57 +0200
changeset 51848 ed847ce0b70c
parent 51834 8deb369ee70b
child 51849 19ee0cebe76d
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     2
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     3
theory Abs_Int2
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     4
imports Abs_Int1
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     5
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     6
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
     7
instantiation prod :: (order,order) order
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     8
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     9
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    10
definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    11
definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    12
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    13
instance
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    14
proof
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    15
  case goal1 show ?case by(rule less_prod_def)
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    16
next
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    17
  case goal2 show ?case by(simp add: less_eq_prod_def)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    18
next
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    19
  case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    20
next
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    21
  case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    22
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    23
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    24
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    25
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    26
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    27
subsection "Backward Analysis of Expressions"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    28
51826
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    29
subclass (in bounded_lattice) semilattice_sup_top ..
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    30
51826
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    31
locale Val_abs1_gamma = Gamma where \<gamma> = \<gamma>
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    32
  for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
    33
assumes inter_gamma_subset_gamma_inf:
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    34
  "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
49396
73fb17ed2e08 converted wt into a set, tuned names
nipkow
parents: 49344
diff changeset
    35
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    36
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    37
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
    38
lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
    39
by (metis IntI inter_gamma_subset_gamma_inf set_mp)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    40
51848
nipkow
parents: 51834
diff changeset
    41
lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
    42
by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
51389
8a9f0503b1c0 factored out Step
nipkow
parents: 51359
diff changeset
    43
  (metis inf_le1 inf_le2 le_inf_iff mono_gamma)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    44
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    45
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    46
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    47
51826
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    48
locale Val_abs1 = Val_abs1_gamma where \<gamma> = \<gamma>
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
    49
   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    50
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    51
and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    52
and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    53
assumes test_num': "test_num' n a = (n : \<gamma> a)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    54
and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    55
  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    56
and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    57
  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    58
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    59
51826
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    60
locale Abs_Int1 = Val_abs1 where \<gamma> = \<gamma>
054a40461449 canonical names of classes
nipkow
parents: 51785
diff changeset
    61
  for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    62
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    63
51389
8a9f0503b1c0 factored out Step
nipkow
parents: 51359
diff changeset
    64
lemma in_gamma_sup_UpI:
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
    65
  "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
    66
by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    67
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    68
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    69
"aval'' e None = \<bottom>" |
51834
nipkow
parents: 51826
diff changeset
    70
"aval'' e (Some S) = aval' e S"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    71
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
    72
lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
    73
by(cases S)(auto simp add: aval'_sound split: option.splits)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    74
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    75
subsubsection "Backward analysis"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    76
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    77
fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    78
"afilter (N n) a S = (if test_num' n a then S else None)" |
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    79
"afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    80
  let a' = fun S x \<sqinter> a in
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
    81
  if a' = \<bottom> then None else Some(update S x a'))" |
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    82
"afilter (Plus e1 e2) a S =
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    83
 (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
    84
  in afilter e1 a1 (afilter e2 a2 S))"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    85
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    86
text{* The test for @{const bot} in the @{const V}-case is important: @{const
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    87
bot} indicates that a variable has no possible values, i.e.\ that the current
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    88
program point is unreachable. But then the abstract state should collapse to
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    89
@{const None}. Put differently, we maintain the invariant that in an abstract
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    90
state of the form @{term"Some s"}, all variables are mapped to non-@{const
51389
8a9f0503b1c0 factored out Step
nipkow
parents: 51359
diff changeset
    91
bot} values. Otherwise the (pointwise) sup of two abstract states, one of
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    92
which contains @{const bot} values, may produce too large a result, thus
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    93
making the analysis less precise. *}
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    94
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    95
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    96
fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    97
"bfilter (Bc v) res S = (if v=res then S else None)" |
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    98
"bfilter (Not b) res S = bfilter b (\<not> res) S" |
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    99
"bfilter (And b1 b2) res S =
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   100
  (if res then bfilter b1 True (bfilter b2 True S)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   101
   else bfilter b1 False S \<squnion> bfilter b2 False S)" |
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   102
"bfilter (Less e1 e2) res S =
51037
0a6d84c41dbf tuned identifier
nipkow
parents: 51036
diff changeset
   103
  (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
0a6d84c41dbf tuned identifier
nipkow
parents: 51036
diff changeset
   104
   in afilter e1 a1 (afilter e2 a2 S))"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   105
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   106
lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   107
proof(induction e arbitrary: a S)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   108
  case N thus ?case by simp (metis test_num')
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   109
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   110
  case (V x)
49497
860b7c6bd913 tuned names
nipkow
parents: 49464
diff changeset
   111
  obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>s S'" using `s : \<gamma>\<^isub>o S`
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   112
    by(auto simp: in_gamma_option_iff)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   113
  moreover hence "s x : \<gamma> (fun S' x)"
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   114
    using V(1,2) by(simp add: \<gamma>_st_def)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   115
  moreover have "s x : \<gamma> a" using V by simp
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   116
  ultimately show ?case
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   117
    by(simp add: Let_def \<gamma>_st_def)
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   118
      (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   119
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   120
  case (Plus e1 e2) thus ?case
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   121
    using filter_plus'[OF _ aval''_sound aval''_sound]
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   122
    by (auto split: prod.split)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   123
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   124
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   125
lemma bfilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   126
proof(induction b arbitrary: S bv)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   127
  case Bc thus ?case by simp
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   128
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   129
  case (Not b) thus ?case by simp
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   130
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   131
  case (And b1 b2) thus ?case
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   132
    by simp (metis And(1) And(2) in_gamma_sup_UpI)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   133
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   134
  case (Less e1 e2) thus ?case
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   135
    by(auto split: prod.split)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   136
      (metis (lifting) afilter_sound aval''_sound filter_less')
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   137
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   138
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   139
definition "step' = Step
51389
8a9f0503b1c0 factored out Step
nipkow
parents: 51359
diff changeset
   140
  (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
8a9f0503b1c0 factored out Step
nipkow
parents: 51359
diff changeset
   141
  (\<lambda>b S. bfilter b True S)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   142
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   143
definition AI :: "com \<Rightarrow> 'av st option acom option" where
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   144
"AI c = pfp (step' \<top>) (bot c)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   145
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   146
lemma strip_step'[simp]: "strip(step' S c) = strip c"
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   147
by(simp add: step'_def)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   148
51785
9685a5b1f7ce more standard order of arguments
nipkow
parents: 51722
diff changeset
   149
lemma top_on_afilter: "\<lbrakk> top_on_opt S X;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt (afilter e a S) X"
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   150
by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   151
51785
9685a5b1f7ce more standard order of arguments
nipkow
parents: 51722
diff changeset
   152
lemma top_on_bfilter: "\<lbrakk>top_on_opt S X; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (bfilter b r S) X"
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   153
by(induction b arbitrary: r S) (auto simp: top_on_afilter top_on_sup split: prod.split)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   154
51785
9685a5b1f7ce more standard order of arguments
nipkow
parents: 51722
diff changeset
   155
lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (- vars C)"
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   156
unfolding step'_def
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   157
by(rule top_on_Step)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   158
  (auto simp add: top_on_top top_on_bfilter split: option.split)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   159
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   160
subsubsection "Soundness"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   161
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   162
lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   163
unfolding step_def step'_def
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   164
by(rule gamma_Step_subcomm)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   165
  (auto simp: intro!: aval'_sound bfilter_sound in_gamma_update split: option.splits)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   166
50986
c54ea7f5418f simplified proofs
nipkow
parents: 49497
diff changeset
   167
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   168
proof(simp add: CS_def AI_def)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   169
  assume 1: "pfp (step' \<top>) (bot c) = Some C"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   170
  have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   171
  have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
50986
c54ea7f5418f simplified proofs
nipkow
parents: 49497
diff changeset
   172
  proof(rule order_trans)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   173
    show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   174
    show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   175
  qed
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   176
  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   177
  have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   178
    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
50986
c54ea7f5418f simplified proofs
nipkow
parents: 49497
diff changeset
   179
  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   180
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   181
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   182
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   183
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   184
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   185
subsubsection "Monotonicity"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   186
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   187
locale Abs_Int1_mono = Abs_Int1 +
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
   188
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
   189
and mono_filter_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
   190
  filter_plus' r a1 a2 \<le> filter_plus' r' b1 b2"
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
   191
and mono_filter_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51037
diff changeset
   192
  filter_less' bv a1 a2 \<le> filter_less' bv b1 b2"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   193
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   194
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   195
lemma mono_aval':
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   196
  "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   197
by(induction e) (auto simp: mono_plus' mono_fun)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   198
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   199
lemma mono_aval'':
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   200
  "S1 \<le> S2 \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   201
apply(cases S1)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   202
 apply simp
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   203
apply(cases S2)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   204
 apply simp
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   205
by (simp add: mono_aval')
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   206
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   207
lemma mono_afilter: "r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   208
apply(induction e arbitrary: r1 r2 S1 S2)
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   209
   apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   210
   apply (metis mono_gamma subsetD)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   211
  apply (metis le_bot inf_mono le_st_iff)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   212
 apply (metis inf_mono mono_update le_st_iff)
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   213
apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   214
done
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   215
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   216
lemma mono_bfilter: "S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   217
apply(induction b arbitrary: bv S1 S2)
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   218
   apply(simp)
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   219
  apply(simp)
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   220
 apply simp
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   221
 apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   222
apply (simp split: prod.splits)
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   223
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   224
done
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   225
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   226
theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
51390
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   227
unfolding step'_def
1dff81cf425b more factorisation of Step & Co
nipkow
parents: 51389
diff changeset
   228
by(rule mono2_Step) (auto simp: mono_aval' mono_bfilter split: option.split)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   229
51711
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   230
lemma mono_step'_top: "C1 \<le> C2 \<Longrightarrow> step' \<top> C1 \<le> step' \<top> C2"
df3426139651 complete revision: finally got rid of annoying L-predicate
nipkow
parents: 51390
diff changeset
   231
by (metis mono_step' order_refl)
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   232
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   233
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   234
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   235
end