Quelle  Abs_Int1_parity.thy

(* Author: Tobias Nipkow *)

subsection "Parity Analysis"

theory Abs_Int1_parity
imports Abs_Int1
begin

datatype parity = Even | Odd | Either

text‹Instantiation of class 🍋‹order› with type 🍋‹parity›:›

instantiation parity :: order
begin

text‹First the definition of the interface function ‹≤›. Note that
  header of the definition must refer to the ascii name const‹less_eq› of the
  as ‹less_eq_parity› and the definition is named ‹less_eq_parity_def›. Inside the definition the symbolic names can be used.›

definition less_eq_parity where
"x ≤ y = (y = Either ∨ x=y)"

text‹We also need ‹<\<close>, which is defined canonically:›

  less_parity where
 x < y = (x ≤ y ∧ ¬ y ≤ (x::parity))"

 ‹\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.)

  the instance proof, i.e.\ the proof that the definition fulfills
  axioms (assumptions) of the class. The initial proof-step generates the
  proof obligations.›

 
 
 fix x::parity show "x ≤ x" by(auto simp: less_eq_parity_def)
 
 fix x y z :: parity assume "x ≤ y" "y ≤ z" thus "x ≤ z"
 by(auto simp: less_eq_parity_def)
 
 fix x y :: parity assume "x ≤ y" "y ≤ x" thus "x = y"
 by(auto simp: less_eq_parity_def)
 
 fix x y :: parity show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" by(rule less_parity_def)
 

 

 ‹Instantiation of class 🍋‹semilattice_sup_top› with type 🍋‹parity›:›

  parity :: semilattice_sup_top
 

  sup_parity where
 x ⊔ y = (if x = y then x else Either)"

  top_parity where
 ⊤ = Either"

 ‹Now the instance proof. This time we take a shortcut with the help of
  method ‹goal_cases›: it creates cases 1 ... n for the subgoals
  ... n; in case i, i is also the name of the assumptions of subgoal i and
 ‹case?› refers to the conclusion of subgoal i.
  class axioms are presented in the same order as in the class definition.›

 
  (standard, goal_cases)
  case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
  case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
  case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
  case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
qed

end


text‹Now we define the functions used for instantiating the abstract
  locales. Note that the Isabelle terminology is
 emph{interpretation}, not \emph{instantiation} of locales, but we use
  to avoid confusion with abstract interpretation.›

fun γ_parity :: "parity ==> val set" where
"γ_parity Even = {i. i mod 2 = 0}" |
"γ_parity Odd = {i. i mod 2 = 1}" |
"γ_parity Either = UNIV"

fun num_parity :: "val ==> parity" where
"num_parity i = (if i mod 2 = 0 then Even else Odd)"

fun plus_parity :: "parity ==> parity ==> parity" where
"plus_parity Even Even = Even" |
"plus_parity Odd Odd = Even" |
"plus_parity Even Odd = Odd" |
"plus_parity Odd Even = Odd" |
"plus_parity Either y = Either" |
"plus_parity x Either = Either"

text‹First we instantiate the abstract value interface and prove that the
  on type 🍋‹parity› have all the necessary properties:›

global_interpretation Val_semilattice
where γ = γ_parity and num' = num_parity and plus' = plus_parity
proof (standard, goal_cases) txt‹subgoals are the locale axioms›
  case 1 thus ?case by(auto simp: less_eq_parity_def)
next
  case 2 show ?case by(auto simp: top_parity_def)
next
  case 3 show ?case by auto
next
  case (4 _ a1 _ a2) thus ?case
    by (induction a1 a2 rule: plus_parity.induct)
      (auto simp add: mod_add_eq [symmetric])
qed

text‹In case 4 we needed to refer to particular variables.
  (i x y z) fixes the names of the variables in case i to be x, y and z
  the left-to-right order in which the variables occur in the subgoal.
  are anonymous placeholders for variable names we don't care to fix.›

text‹Instantiating the abstract interpretation locale requires no more
  (they happened in the instatiation above) but delivers the
  abstract interpreter which we call ‹AI_parity›:›

global_interpretation Abs_Int
where γ = γ_parity and num' = num_parity and plus' = plus_parity
defines aval_parity = aval' and step_parity = step' and AI_parity = AI
..


subsubsection "Tests"

definition "test1_parity =
  ''x'' ::= N 1;;
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
value "show_acom (the(AI_parity test1_parity))"

definition "test2_parity =
  ''x'' ::= N 1;;
  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"

definition "steps c i = ((step_parity ⊤) ^^ i) (bot c)"

value "show_acom (steps test2_parity 0)"
value "show_acom (steps test2_parity 1)"
value "show_acom (steps test2_parity 2)"
value "show_acom (steps test2_parity 3)"
value "show_acom (steps test2_parity 4)"
value "show_acom (steps test2_parity 5)"
value "show_acom (steps test2_parity 6)"
value "show_acom (the(AI_parity test2_parity))"


subsubsection "Termination"

global_interpretation Abs_Int_mono
where γ = γ_parity and num' = num_parity and plus' = plus_parity
proof (standard, goal_cases)
  case (1 _ a1 _ a2) thus ?case
    by(induction a1 a2 rule: plus_parity.induct)
      (auto simp add:less_eq_parity_def)
qed

definition m_parity :: "parity ==> nat" where
"m_parity x = (if x = Either then 0 else 1)"

global_interpretation Abs_Int_measure
where γ = γ_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
proof (standard, goal_cases)
  case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
next
  case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
qed

thm AI_Some_measure

end