src/HOL/IMP/Abs_Int0_const.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46355 42a01315d998
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_Int0_const
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45200
diff changeset
     4
imports Abs_Int0 Abs_Int_Tests
45111
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 "Constant Propagation"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     8
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
     9
datatype const = Const val | Any
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    10
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    11
fun \<gamma>_const where
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    12
"\<gamma>_const (Const n) = {n}" |
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    13
"\<gamma>_const (Any) = UNIV"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    14
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    15
fun plus_const where
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    16
"plus_const (Const m) (Const n) = Const(m+n)" |
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    17
"plus_const _ _ = Any"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    18
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    19
lemma plus_const_cases: "plus_const a1 a2 =
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    20
  (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    21
by(auto split: prod.split const.split)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    22
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    23
instantiation const :: SL_top
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    24
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    25
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    26
fun le_const where
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    27
"_ \<sqsubseteq> Any = True" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    28
"Const n \<sqsubseteq> Const m = (n=m)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    29
"Any \<sqsubseteq> Const _ = False"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    30
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    31
fun join_const where
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    32
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    33
"_ \<squnion> _ = Any"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    34
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    35
definition "\<top> = Any"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    36
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    37
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    39
  case goal1 thus ?case by (cases x) simp_all
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    41
  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    42
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    43
  case goal3 thus ?case by(cases x, cases y, simp_all)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    44
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    45
  case goal4 thus ?case by(cases y, cases x, simp_all)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    47
  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    48
next
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    49
  case goal6 thus ?case by(simp add: Top_const_def)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    52
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    53
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    54
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
    55
interpretation Val_abs
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    56
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    57
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    59
    by(cases a, cases b, simp, simp, cases b, simp, simp)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    60
next
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    61
  case goal2 show ?case by(simp add: Top_const_def)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    62
next
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45111
diff changeset
    63
  case goal3 show ?case by simp
45111
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
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    66
    by(auto simp: plus_const_cases split: const.split)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    67
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    68
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
    69
interpretation Abs_Int
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
    70
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
46346
10c18630612a removed duplicate definitions that made locale inconsistent
nipkow
parents: 46334
diff changeset
    71
defines AI_const is AI and step_const is step' and aval'_const is aval'
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46353
diff changeset
    72
..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    73
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    74
46353
nipkow
parents: 46346
diff changeset
    75
subsubsection "Tests"
nipkow
parents: 46346
diff changeset
    76
nipkow
parents: 46346
diff changeset
    77
value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
nipkow
parents: 46346
diff changeset
    78
value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
nipkow
parents: 46346
diff changeset
    79
value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
nipkow
parents: 46346
diff changeset
    80
value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
nipkow
parents: 46346
diff changeset
    81
value "show_acom_opt (AI_const test1_const)"
nipkow
parents: 46346
diff changeset
    82
nipkow
parents: 46346
diff changeset
    83
value "show_acom_opt (AI_const test2_const)"
nipkow
parents: 46346
diff changeset
    84
value "show_acom_opt (AI_const test3_const)"
nipkow
parents: 46346
diff changeset
    85
nipkow
parents: 46346
diff changeset
    86
value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
nipkow
parents: 46346
diff changeset
    87
value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
nipkow
parents: 46346
diff changeset
    88
value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
nipkow
parents: 46346
diff changeset
    89
value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
nipkow
parents: 46346
diff changeset
    90
value "show_acom_opt (AI_const test4_const)"
nipkow
parents: 46346
diff changeset
    91
nipkow
parents: 46346
diff changeset
    92
value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    93
value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    94
value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    95
value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    96
value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    97
value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
nipkow
parents: 46346
diff changeset
    98
value "show_acom_opt (AI_const test5_const)"
nipkow
parents: 46346
diff changeset
    99
nipkow
parents: 46346
diff changeset
   100
value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   101
value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   102
value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   103
value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   104
value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   105
value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   106
value "show_acom (((step_const \<top>)^^6) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   107
value "show_acom (((step_const \<top>)^^7) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   108
value "show_acom (((step_const \<top>)^^8) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   109
value "show_acom (((step_const \<top>)^^9) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   110
value "show_acom (((step_const \<top>)^^10) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   111
value "show_acom (((step_const \<top>)^^11) (\<bottom>\<^sub>c test6_const))"
nipkow
parents: 46346
diff changeset
   112
value "show_acom_opt (AI_const test6_const)"
nipkow
parents: 46346
diff changeset
   113
nipkow
parents: 46346
diff changeset
   114
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45200
diff changeset
   115
text{* Monotonicity: *}
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   116
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   117
interpretation Abs_Int_mono
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   118
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45200
diff changeset
   119
proof
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45200
diff changeset
   120
  case goal1 thus ?case
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   121
    by(auto simp: plus_const_cases split: const.split)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45200
diff changeset
   122
qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   123
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   124
text{* Termination: *}
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   125
46334
nipkow
parents: 46158
diff changeset
   126
definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
nipkow
parents: 46158
diff changeset
   127
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   128
lemma measure_const:
46334
nipkow
parents: 46158
diff changeset
   129
  "(strict{(x::const,y). x \<sqsubseteq> y})^-1 \<subseteq> measure m_const"
nipkow
parents: 46158
diff changeset
   130
by(auto simp: m_const_def split: const.splits)
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   131
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   132
lemma measure_const_eq:
46334
nipkow
parents: 46158
diff changeset
   133
  "\<forall> x y::const. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_const x = m_const y"
nipkow
parents: 46158
diff changeset
   134
by(auto simp: m_const_def split: const.splits)
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   135
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   136
lemma "EX c'. AI_const c = Some c'"
46334
nipkow
parents: 46158
diff changeset
   137
by(rule AI_Some_measure[OF measure_const measure_const_eq])
46158
8b5f1f91ef38 Added termination to IMP Abs_Int
nipkow
parents: 46063
diff changeset
   138
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   139
end