(* 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" ("(2_ [:=]/ _)")
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
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
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.
|
