Quelle SPARK_Setup.thy Sprache: Isabelle

(*  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 \<open>Tools/fdl_lexer.ML\<close>
ML_file \<open>Tools/fdl_parser.ML\<close>

text \<open>
SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
\<close>

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 \<open>
Correspondence between HOL's and SPARK's version of div
\<close>

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 \<open>
Updating a function at a set of points. Useful for building arrays.
\<close>

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"  (\<open>(\<open>indent=2 notation=\<open>infix update set\<close>\<close>_ [:=]/ _)\<close>)
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 \<open>Enumeration types\<close>

class spark_enum = ord + finite +
  fixes pos :: "'a \ int"
  assumes range_pos: "range pos = {0..
  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.. z \ {x+1..
  by auto

text \<open>Load the package\<close>

ML_file \<open>Tools/spark_vcs.ML\<close>
ML_file \<open>Tools/spark_commands.ML\<close>

end

quality98%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.