Theory SPARK_Setup

(*  Title:      HOL/SPARK/SPARK_Setup.thy
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG

Setup for SPARK/Ada verification environment.
*)

theory SPARK_Setup
  imports "HOL-Library.Word"
  keywords "spark_open_vcg" :: thy_load (spark_vcg)
    and "spark_open" :: thy_load (spark_siv)
    and "spark_proof_functions" "spark_types" "spark_end" :: thy_decl
    and "spark_vc" :: thy_goal
    and "spark_status" :: diag
begin

ML_file ‹Tools/fdl_lexer.ML›
ML_file ‹Tools/fdl_parser.ML›

text ‹
SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
›

definition sdiv :: "int ⇒ int ⇒ int" (infixl ‹sdiv› 70) where
  "a sdiv b = sgn a * sgn b * (¦a¦ div ¦b¦)"

lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
  by (simp add: sdiv_def sgn_if)

lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
  by (simp add: sdiv_def sgn_if)

text ‹
Correspondence between HOL's and SPARK's version of div
›

lemma sdiv_pos_pos: "0 ≤ a ⟹ 0 ≤ b ⟹ a sdiv b = a div b"
  by (simp add: sdiv_def sgn_if)

lemma sdiv_pos_neg: "0 ≤ a ⟹ b < 0 ⟹ a sdiv b = - (a div - b)"
  by (simp add: sdiv_def sgn_if)

lemma sdiv_neg_pos: "a < 0 ⟹ 0 ≤ b ⟹ a sdiv b = - (- a div b)"
  by (simp add: sdiv_def sgn_if)

lemma sdiv_neg_neg: "a < 0 ⟹ b < 0 ⟹ a sdiv b = - a div - b"
  by (simp add: sdiv_def sgn_if)


text ‹
Updating a function at a set of points. Useful for building arrays.
›

definition fun_upds :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b ⇒ 'a ⇒ 'b" where
  "fun_upds f xs y z = (if z ∈ xs then y else f z)"

syntax
  "_updsbind" :: "['a, 'a] => updbind"  (‹(‹indent=2 notation=‹infix update set››_ [:=]/ _)›)
syntax_consts
  "_updsbind" == fun_upds
translations
  "f(xs[:=]y)" == "CONST fun_upds f xs y"

lemma fun_upds_in [simp]: "z ∈ xs ⟹ (f(xs [:=] y)) z = y"
  by (simp add: fun_upds_def)

lemma fun_upds_notin [simp]: "z ∉ xs ⟹ (f(xs [:=] y)) z = f z"
  by (simp add: fun_upds_def)

lemma upds_singleton [simp]: "f({x} [:=] y) = f(x := y)"
  by (simp add: fun_eq_iff)


text ‹Enumeration types›

class spark_enum = ord + finite +
  fixes pos :: "'a ⇒ int"
  assumes range_pos: "range pos = {0..<int (card (UNIV::'a set))}"
  and less_pos: "(x < y) = (pos x < pos y)"
  and less_eq_pos: "(x ≤ y) = (pos x ≤ pos y)"
begin

definition "val = inv pos"

definition "succ x = val (pos x + 1)"

definition "pred x = val (pos x - 1)"

lemma inj_pos: "inj pos"
  using finite_UNIV
  by (rule eq_card_imp_inj_on) (simp add: range_pos)

lemma val_pos: "val (pos x) = x"
  unfolding val_def using inj_pos
  by (rule inv_f_f)

lemma pos_val: "z ∈ range pos ⟹ pos (val z) = z"
  unfolding val_def
  by (rule f_inv_into_f)

subclass linorder
proof
  fix x::'a and y show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (simp add: less_pos less_eq_pos less_le_not_le)
next
  fix x::'a show "x ≤ x" by (simp add: less_eq_pos)
next
  fix x::'a and y z assume "x ≤ y" and "y ≤ z"
  then show "x ≤ z" by (simp add: less_eq_pos)
next
  fix x::'a and y assume "x ≤ y" and "y ≤ x"
  with inj_pos show "x = y"
    by (auto dest: injD simp add: less_eq_pos)
next
  fix x::'a and y show "x ≤ y ∨ y ≤ x"
    by (simp add: less_eq_pos linear)
qed

definition "first_el = val 0"

definition "last_el = val (int (card (UNIV::'a set)) - 1)"

lemma first_el_smallest: "first_el ≤ x"
proof -
  have "pos x ∈ range pos" by (rule rangeI)
  then have "pos (val 0) ≤ pos x"
    by (simp add: range_pos pos_val)
  then show ?thesis by (simp add: first_el_def less_eq_pos)
qed

lemma last_el_greatest: "x ≤ last_el"
proof -
  have "pos x ∈ range pos" by (rule rangeI)
  then have "pos x ≤ pos (val (int (card (UNIV::'a set)) - 1))"
    by (simp add: range_pos pos_val)
  then show ?thesis by (simp add: last_el_def less_eq_pos)
qed

lemma pos_succ:
  assumes "x ≠ last_el"
  shows "pos (succ x) = pos x + 1"
proof -
  have "x ≤ last_el" by (rule last_el_greatest)
  with assms have "x < last_el" by simp
  then have "pos x < pos last_el"
    by (simp add: less_pos)
  with rangeI [of pos x]
  have "pos x + 1 ∈ range pos"
    by (simp add: range_pos last_el_def pos_val)
  then show ?thesis
    by (simp add: succ_def pos_val)
qed

lemma pos_pred:
  assumes "x ≠ first_el"
  shows "pos (pred x) = pos x - 1"
proof -
  have "first_el ≤ x" by (rule first_el_smallest)
  with assms have "first_el < x" by simp
  then have "pos first_el < pos x"
    by (simp add: less_pos)
  with rangeI [of pos x]
  have "pos x - 1 ∈ range pos"
    by (simp add: range_pos first_el_def pos_val)
  then show ?thesis
    by (simp add: pred_def pos_val)
qed

lemma succ_val: "x ∈ range pos ⟹ succ (val x) = val (x + 1)"
  by (simp add: succ_def pos_val)

lemma pred_val: "x ∈ range pos ⟹ pred (val x) = val (x - 1)"
  by (simp add: pred_def pos_val)

end

lemma interval_expand:
  "x < y ⟹ (z::int) ∈ {x..<y} = (z = x ∨ z ∈ {x+1..<y})"
  by auto


text ‹Load the package›

ML_file ‹Tools/spark_vcs.ML›
ML_file ‹Tools/spark_commands.ML›

end