src/HOL/IMP/Abs_Int1_parity.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61890 f6ded81f5690
child 64593 50c715579715
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@51359
     1
(* Author: Tobias Nipkow *)
nipkow@51359
     2
nipkow@47613
     3
theory Abs_Int1_parity
nipkow@47613
     4
imports Abs_Int1
nipkow@47613
     5
begin
nipkow@47613
     6
nipkow@47613
     7
subsection "Parity Analysis"
nipkow@47613
     8
blanchet@58310
     9
datatype parity = Even | Odd | Either
nipkow@47613
    10
nipkow@51359
    11
text{* Instantiation of class @{class order} with type @{typ parity}: *}
nipkow@47613
    12
nipkow@51359
    13
instantiation parity :: order
nipkow@47613
    14
begin
nipkow@47613
    15
nipkow@51359
    16
text{* First the definition of the interface function @{text"\<le>"}. Note that
nipkow@51359
    17
the header of the definition must refer to the ascii name @{const less_eq} of the
nipkow@51359
    18
constants as @{text less_eq_parity} and the definition is named @{text
nipkow@51359
    19
less_eq_parity_def}.  Inside the definition the symbolic names can be used. *}
nipkow@51359
    20
nipkow@51359
    21
definition less_eq_parity where
nipkow@51359
    22
"x \<le> y = (y = Either \<or> x=y)"
nipkow@47613
    23
nipkow@51359
    24
text{* We also need @{text"<"}, which is defined canonically: *}
nipkow@47613
    25
nipkow@51359
    26
definition less_parity where
nipkow@51359
    27
"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
nipkow@51359
    28
nipkow@51625
    29
text{*\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.)
nipkow@51359
    30
nipkow@51359
    31
Now the instance proof, i.e.\ the proof that the definition fulfills
nipkow@47613
    32
the axioms (assumptions) of the class. The initial proof-step generates the
nipkow@47613
    33
necessary proof obligations. *}
nipkow@47613
    34
nipkow@47613
    35
instance
nipkow@47613
    36
proof
nipkow@51359
    37
  fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
nipkow@51359
    38
next
nipkow@51359
    39
  fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
nipkow@51359
    40
    by(auto simp: less_eq_parity_def)
nipkow@47613
    41
next
nipkow@51359
    42
  fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
nipkow@51359
    43
    by(auto simp: less_eq_parity_def)
nipkow@51359
    44
next
nipkow@51359
    45
  fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
nipkow@47613
    46
qed
nipkow@47613
    47
nipkow@47613
    48
end
nipkow@47613
    49
nipkow@51826
    50
text{* Instantiation of class @{class semilattice_sup_top} with type @{typ parity}: *}
nipkow@47613
    51
nipkow@51826
    52
instantiation parity :: semilattice_sup_top
nipkow@47613
    53
begin
nipkow@47613
    54
nipkow@51389
    55
definition sup_parity where
nipkow@51624
    56
"x \<squnion> y = (if x = y then x else Either)"
nipkow@47613
    57
nipkow@51359
    58
definition top_parity where
nipkow@47613
    59
"\<top> = Either"
nipkow@47613
    60
nipkow@61179
    61
text{* Now the instance proof. This time we take a shortcut with the help of
nipkow@61179
    62
proof method @{text goal_cases}: it creates cases 1 ... n for the subgoals
nipkow@61179
    63
1 ... n; in case i, i is also the name of the assumptions of subgoal i and
nipkow@61179
    64
@{text "case?"} refers to the conclusion of subgoal i.
nipkow@61179
    65
The class axioms are presented in the same order as in the class definition. *}
nipkow@47613
    66
nipkow@47613
    67
instance
nipkow@61179
    68
proof (standard, goal_cases)
nipkow@61179
    69
  case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
nipkow@47613
    70
next
nipkow@61179
    71
  case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
nipkow@47613
    72
next
nipkow@61179
    73
  case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
nipkow@47613
    74
next
nipkow@61179
    75
  case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
nipkow@47613
    76
qed
nipkow@47613
    77
nipkow@47613
    78
end
nipkow@47613
    79
nipkow@47613
    80
nipkow@47613
    81
text{* Now we define the functions used for instantiating the abstract
nipkow@47613
    82
interpretation locales. Note that the Isabelle terminology is
nipkow@47613
    83
\emph{interpretation}, not \emph{instantiation} of locales, but we use
nipkow@47613
    84
instantiation to avoid confusion with abstract interpretation.  *}
nipkow@47613
    85
nipkow@47613
    86
fun \<gamma>_parity :: "parity \<Rightarrow> val set" where
nipkow@47613
    87
"\<gamma>_parity Even = {i. i mod 2 = 0}" |
nipkow@47613
    88
"\<gamma>_parity Odd  = {i. i mod 2 = 1}" |
nipkow@47613
    89
"\<gamma>_parity Either = UNIV"
nipkow@47613
    90
nipkow@47613
    91
fun num_parity :: "val \<Rightarrow> parity" where
nipkow@47613
    92
"num_parity i = (if i mod 2 = 0 then Even else Odd)"
nipkow@47613
    93
nipkow@47613
    94
fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where
nipkow@47613
    95
"plus_parity Even Even = Even" |
nipkow@47613
    96
"plus_parity Odd  Odd  = Even" |
nipkow@47613
    97
"plus_parity Even Odd  = Odd" |
nipkow@47613
    98
"plus_parity Odd  Even = Odd" |
nipkow@47613
    99
"plus_parity Either y  = Either" |
nipkow@47613
   100
"plus_parity x Either  = Either"
nipkow@47613
   101
nipkow@47613
   102
text{* First we instantiate the abstract value interface and prove that the
nipkow@47613
   103
functions on type @{typ parity} have all the necessary properties: *}
nipkow@47613
   104
haftmann@61890
   105
global_interpretation Val_semilattice
nipkow@47613
   106
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
nipkow@61179
   107
proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
nipkow@61179
   108
  case 1 thus ?case by(auto simp: less_eq_parity_def)
nipkow@47613
   109
next
nipkow@61179
   110
  case 2 show ?case by(auto simp: top_parity_def)
nipkow@47613
   111
next
nipkow@61179
   112
  case 3 show ?case by auto
nipkow@61179
   113
next
nipkow@61179
   114
  case (4 _ a1 _ a2) thus ?case
nipkow@52525
   115
    by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
nipkow@47613
   116
qed
nipkow@47613
   117
nipkow@61179
   118
text{* In case 4 we needed to refer to particular variables.
nipkow@61179
   119
Writing (i x y z) fixes the names of the variables in case i to be x, y and z
nipkow@61179
   120
in the left-to-right order in which the variables occur in the subgoal.
nipkow@61179
   121
Underscores are anonymous placeholders for variable names we don't care to fix. *}
nipkow@61179
   122
nipkow@47613
   123
text{* Instantiating the abstract interpretation locale requires no more
nipkow@47613
   124
proofs (they happened in the instatiation above) but delivers the
nipkow@49344
   125
instantiated abstract interpreter which we call @{text AI_parity}: *}
nipkow@47613
   126
haftmann@61890
   127
global_interpretation Abs_Int
nipkow@47613
   128
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
haftmann@61671
   129
defines aval_parity = aval' and step_parity = step' and AI_parity = AI
nipkow@47613
   130
..
nipkow@47613
   131
nipkow@47613
   132
nipkow@47613
   133
subsubsection "Tests"
nipkow@47613
   134
nipkow@47613
   135
definition "test1_parity =
nipkow@52046
   136
  ''x'' ::= N 1;;
nipkow@47613
   137
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
haftmann@56927
   138
value "show_acom (the(AI_parity test1_parity))"
nipkow@47613
   139
nipkow@47613
   140
definition "test2_parity =
nipkow@52046
   141
  ''x'' ::= N 1;;
nipkow@47613
   142
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
nipkow@47613
   143
nipkow@51711
   144
definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
nipkow@47613
   145
nipkow@47613
   146
value "show_acom (steps test2_parity 0)"
nipkow@47613
   147
value "show_acom (steps test2_parity 1)"
nipkow@47613
   148
value "show_acom (steps test2_parity 2)"
nipkow@47613
   149
value "show_acom (steps test2_parity 3)"
nipkow@47613
   150
value "show_acom (steps test2_parity 4)"
nipkow@47613
   151
value "show_acom (steps test2_parity 5)"
nipkow@49188
   152
value "show_acom (steps test2_parity 6)"
nipkow@50995
   153
value "show_acom (the(AI_parity test2_parity))"
nipkow@47613
   154
nipkow@47613
   155
nipkow@47613
   156
subsubsection "Termination"
nipkow@47613
   157
haftmann@61890
   158
global_interpretation Abs_Int_mono
nipkow@47613
   159
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
nipkow@61179
   160
proof (standard, goal_cases)
nipkow@61179
   161
  case (1 _ a1 _ a2) thus ?case
nipkow@52525
   162
    by(induction a1 a2 rule: plus_parity.induct)
nipkow@52525
   163
      (auto simp add:less_eq_parity_def)
nipkow@47613
   164
qed
nipkow@47613
   165
nipkow@47613
   166
definition m_parity :: "parity \<Rightarrow> nat" where
nipkow@51389
   167
"m_parity x = (if x = Either then 0 else 1)"
nipkow@47613
   168
haftmann@61890
   169
global_interpretation Abs_Int_measure
nipkow@47613
   170
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
nipkow@49433
   171
and m = m_parity and h = "1"
nipkow@61179
   172
proof (standard, goal_cases)
nipkow@61179
   173
  case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
nipkow@47613
   174
next
nipkow@61179
   175
  case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
nipkow@47613
   176
qed
nipkow@47613
   177
nipkow@47613
   178
thm AI_Some_measure
nipkow@47613
   179
nipkow@47613
   180
end