src/HOL/IMP/Abs_Int0_parity.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:
46345
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     1
theory Abs_Int0_parity
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     2
imports Abs_Int0
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     3
begin
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     4
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     5
subsection "Parity Analysis"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     6
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     7
datatype parity = Even | Odd | Either
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     8
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
     9
text{* Instantiation of class @{class preord} with type @{typ parity}: *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    10
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    11
instantiation parity :: preord
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    12
begin
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    13
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    14
text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    15
the header of the definition must refer to the ascii name @{const le} of the
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    16
constants as @{text le_parity} and the definition is named @{text
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    17
le_parity_def}.  Inside the definition the symbolic names can be used. *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    18
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    19
definition le_parity where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    20
"x \<sqsubseteq> y = (y = Either \<or> x=y)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    21
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    22
text{* Now the instance proof, i.e.\ the proof that the definition fulfills
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    23
the axioms (assumptions) of the class. The initial proof-step generates the
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    24
necessary proof obligations. *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    25
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    26
instance
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    27
proof
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    28
  fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    29
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    30
  fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    31
    by(auto simp: le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    32
qed
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    33
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    34
end
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    35
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    36
text{* Instantiation of class @{class SL_top} with type @{typ parity}: *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    37
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    38
instantiation parity :: SL_top
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    39
begin
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    40
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    41
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    42
definition join_parity where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    43
"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    44
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    45
definition Top_parity where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    46
"\<top> = Either"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    47
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    48
text{* Now the instance proof. This time we take a lazy shortcut: we do not
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    49
write out the proof obligations but use the @{text goali} primitive to refer
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    50
to the assumptions of subgoal i and @{text "case?"} to refer to the
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    51
conclusion of subgoal i. The class axioms are presented in the same order as
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    52
in the class definition. *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    53
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    54
instance
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    55
proof
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    56
  case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    57
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    58
  case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    59
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    60
  case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    61
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    62
  case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    63
qed
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    64
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    65
end
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    66
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    67
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    68
text{* Now we define the functions used for instantiating the abstract
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    69
interpretation locales. Note that the Isabelle terminology is
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    70
\emph{interpretation}, not \emph{instantiation} of locales, but we use
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    71
instantiation to avoid confusion with abstract interpretation.  *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    72
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    73
fun \<gamma>_parity :: "parity \<Rightarrow> val set" where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    74
"\<gamma>_parity Even = {i. i mod 2 = 0}" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    75
"\<gamma>_parity Odd  = {i. i mod 2 = 1}" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    76
"\<gamma>_parity Either = UNIV"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    77
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    78
fun num_parity :: "val \<Rightarrow> parity" where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    79
"num_parity i = (if i mod 2 = 0 then Even else Odd)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    80
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    81
fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    82
"plus_parity Even Even = Even" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    83
"plus_parity Odd  Odd  = Even" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    84
"plus_parity Even Odd  = Odd" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    85
"plus_parity Odd  Even = Odd" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    86
"plus_parity Either y  = Either" |
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    87
"plus_parity x Either  = Either"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    88
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    89
text{* First we instantiate the abstract value interface and prove that the
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    90
functions on type @{typ parity} have all the necessary properties: *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    91
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    92
interpretation Val_abs
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    93
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    94
proof txt{* of the locale axioms *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    95
  fix a b :: parity
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    96
  assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    97
    by(auto simp: le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    98
next txt{* The rest in the lazy, implicit way *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
    99
  case goal2 show ?case by(auto simp: Top_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   100
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   101
  case goal3 show ?case by auto
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   102
next
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   103
  txt{* Warning: this subproof refers to the names @{text a1} and @{text a2}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   104
  from the statement of the axiom. *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   105
  case goal4 thus ?case
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   106
  proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust])
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   107
  qed (auto simp add:mod_add_eq)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   108
qed
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   109
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   110
text{* Instantiating the abstract interpretation locale requires no more
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   111
proofs (they happened in the instatiation above) but delivers the
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   112
instantiated abstract interpreter which we call AI: *}
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   113
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   114
interpretation Abs_Int
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   115
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
46346
10c18630612a removed duplicate definitions that made locale inconsistent
nipkow
parents: 46345
diff changeset
   116
defines aval_parity is aval' and step_parity is step' and AI_parity is AI
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   117
..
46345
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   118
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   119
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   120
subsubsection "Tests"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   121
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   122
definition "test1_parity =
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   123
  ''x'' ::= N 1;
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   124
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   125
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   126
value "show_acom_opt (AI_parity test1_parity)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   127
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   128
definition "test2_parity =
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   129
  ''x'' ::= N 1;
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   130
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   131
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   132
value "show_acom ((step_parity \<top> ^^1) (anno None test2_parity))"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   133
value "show_acom ((step_parity \<top> ^^2) (anno None test2_parity))"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   134
value "show_acom ((step_parity \<top> ^^3) (anno None test2_parity))"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   135
value "show_acom ((step_parity \<top> ^^4) (anno None test2_parity))"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   136
value "show_acom ((step_parity \<top> ^^5) (anno None test2_parity))"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   137
value "show_acom_opt (AI_parity test2_parity)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   138
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   139
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   140
subsubsection "Termination"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   141
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   142
interpretation Abs_Int_mono
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   143
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   144
proof
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   145
  case goal1 thus ?case
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   146
  proof(cases a1 a2 b1 b2
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   147
   rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   148
  qed (auto simp add:le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   149
qed
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   150
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   151
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   152
definition m_parity :: "parity \<Rightarrow> nat" where
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   153
"m_parity x = (if x=Either then 0 else 1)"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   154
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   155
lemma measure_parity:
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   156
  "(strict{(x::parity,y). x \<sqsubseteq> y})^-1 \<subseteq> measure m_parity"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   157
by(auto simp add: m_parity_def le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   158
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   159
lemma measure_parity_eq:
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   160
  "\<forall>x y::parity. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_parity x = m_parity y"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   161
by(auto simp add: m_parity_def le_parity_def)
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   162
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   163
lemma AI_parity_Some: "\<exists>c'. AI_parity c = Some c'"
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   164
by(rule AI_Some_measure[OF measure_parity measure_parity_eq])
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   165
202f8b8086a3 added parity analysis
nipkow
parents:
diff changeset
   166
end