Theory Abs_Int1_parity

(* Author: Tobias Nipkow *)

theory Abs_Int1_parity
imports Abs_Int1
begin

subsection "Parity Analysis"

datatype parity = Even | Odd | Either

text‹Instantiation of class @{class preord} with type @{typ parity}:›

instantiation parity :: preord
begin

text‹First the definition of the interface function ‹⊑›. Note that
the header of the definition must refer to the ascii name @{const le} of the
constants as ‹le_parity› and the definition is named ‹le_parity_def›.  Inside the definition the symbolic names can be used.›

definition le_parity where
"x ⊑ y = (y = Either ∨ x=y)"

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

instance
proof
  fix x::parity show "x ⊑ x" by(auto simp: le_parity_def)
next
  fix x y z :: parity assume "x ⊑ y" "y ⊑ z" thus "x ⊑ z"
    by(auto simp: le_parity_def)
qed

end

text‹Instantiation of class @{class SL_top} with type @{typ parity}:›

instantiation parity :: SL_top
begin


definition join_parity where
"x ⊔ y = (if x ⊑ y then y else if y ⊑ x then x else Either)"

definition Top_parity where
"⊤ = Either"

text‹Now the instance proof. This time we take a lazy shortcut: we do not
write out the proof obligations but use the ‹goali› primitive to refer
to the assumptions of subgoal i and ‹case?› to refer to the
conclusion of subgoal i. The class axioms are presented in the same order as
in the class definition.›

instance
proof (standard, goal_cases)
  case 1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
next
  case 2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
next
  case 3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
next
  case 4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
qed

end


text‹Now we define the functions used for instantiating the abstract
interpretation locales. Note that the Isabelle terminology is
\emph{interpretation}, not \emph{instantiation} of locales, but we use
instantiation 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
functions on type @{typ parity} have all the necessary properties:›

interpretation Val_abs
where γ = γ_parity and num' = num_parity and plus' = plus_parity
proof (standard, goal_cases) txt‹of the locale axioms›
  fix a b :: parity
  assume "a ⊑ b" thus "γ_parity a ⊆ γ_parity b"
    by(auto simp: le_parity_def)
next txt‹The rest in the lazy, implicit way›
  case 2 show ?case by(auto simp: Top_parity_def)
next
  case 3 show ?case by auto
next
  case (4 _ a1 _ a2) thus ?case
  proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust])
  qed (auto, presburger)
qed

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

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_opt (AI_parity test1_parity)"

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

value "show_acom ((step_parity ⊤ ^^1) (anno None test2_parity))"
value "show_acom ((step_parity ⊤ ^^2) (anno None test2_parity))"
value "show_acom ((step_parity ⊤ ^^3) (anno None test2_parity))"
value "show_acom ((step_parity ⊤ ^^4) (anno None test2_parity))"
value "show_acom ((step_parity ⊤ ^^5) (anno None test2_parity))"
value "show_acom_opt (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 b1 b2) thus ?case
  proof(cases a1 a2 b1 b2
   rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
  qed (auto simp add:le_parity_def)
qed


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

lemma measure_parity:
  "(strict{(x::parity,y). x ⊑ y})^-1 ⊆ measure m_parity"
by(auto simp add: m_parity_def le_parity_def)

lemma measure_parity_eq:
  "∀x y::parity. x ⊑ y ∧ y ⊑ x ⟶ m_parity x = m_parity y"
by(auto simp add: m_parity_def le_parity_def)

lemma AI_parity_Some: "∃c'. AI_parity c = Some c'"
by(rule AI_Some_measure[OF measure_parity measure_parity_eq])

end