src/HOL/SPARK/SPARK_Setup.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,212 @@
+(*  Title:      HOL/SPARK/SPARK_Setup.thy
+    Author:     Stefan Berghofer
+    Copyright:  secunet Security Networks AG
+
+Setup for SPARK/Ada verification environment.
+*)
+
+theory SPARK_Setup
+imports Word
+uses
+  "Tools/fdl_lexer.ML"
+  "Tools/fdl_parser.ML"
+  ("Tools/spark_vcs.ML")
+  ("Tools/spark_commands.ML")
+begin
+
+text {*
+SPARK versions of div and mod, see section 4.4.1.1 of SPARK Proof Manual
+*}
+
+definition sdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
+  "a sdiv b =
+     (if 0 \<le> a then
+        if 0 \<le> b then a div b
+        else - (a div - b)
+      else
+        if 0 \<le> b then - (- a div b)
+        else - a div - b)"
+
+definition smod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "smod" 70) where
+  "a smod b = a - ((a sdiv b) * b)"
+
+lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
+  by (simp add: sdiv_def)
+
+lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
+  by (simp add: sdiv_def)
+
+lemma smod_minus_dividend: "- a smod b = - (a smod b)"
+  by (simp add: smod_def sdiv_minus_dividend)
+
+lemma smod_minus_divisor: "a smod - b = a smod b"
+  by (simp add: smod_def sdiv_minus_divisor)
+
+text {*
+Correspondence between HOL's and SPARK's versions of div and mod
+*}
+
+lemma sdiv_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = a div b"
+  by (simp add: sdiv_def)
+
+lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
+  by (simp add: sdiv_def)
+
+lemma sdiv_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = - (- a div b)"
+  by (simp add: sdiv_def)
+
+lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
+  by (simp add: sdiv_def)
+
+lemma smod_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = a mod b"
+  by (simp add: smod_def sdiv_pos_pos zmod_zdiv_equality')
+
+lemma smod_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a smod b = a mod - b"
+  by (simp add: smod_def sdiv_pos_neg zmod_zdiv_equality')
+
+lemma smod_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = - (- a mod b)"
+  by (simp add: smod_def sdiv_neg_pos zmod_zdiv_equality')
+
+lemma smod_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a smod b = - (- a mod - b)"
+  by (simp add: smod_def sdiv_neg_neg zmod_zdiv_equality')
+
+
+text {*
+Updating a function at a set of points. Useful for building arrays.
+*}
+
+definition fun_upds :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" where
+  "fun_upds f xs y z = (if z \<in> 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 \<in> xs \<Longrightarrow> (f(xs [:=] y)) z = y"
+  by (simp add: fun_upds_def)
+
+lemma fun_upds_notin [simp]: "z \<notin> xs \<Longrightarrow> (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 enum = ord + finite +
+  fixes pos :: "'a \<Rightarrow> 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 \<le> y) = (pos x \<le> 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 \<in> range pos \<Longrightarrow> 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 \<le> y \<and> \<not> y \<le> x)"
+    by (simp add: less_pos less_eq_pos less_le_not_le)
+next
+  fix x::'a show "x \<le> x" by (simp add: less_eq_pos)
+next
+  fix x::'a and y z assume "x \<le> y" and "y \<le> z"
+  then show "x \<le> z" by (simp add: less_eq_pos)
+next
+  fix x::'a and y assume "x \<le> y" and "y \<le> x"
+  with inj_pos show "x = y"
+    by (auto dest: injD simp add: less_eq_pos)
+next
+  fix x::'a and y show "x \<le> y \<or> y \<le> 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 \<le> x"
+proof -
+  have "pos x \<in> range pos" by (rule rangeI)
+  then have "pos (val 0) \<le> 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 \<le> last_el"
+proof -
+  have "pos x \<in> range pos" by (rule rangeI)
+  then have "pos x \<le> 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 \<noteq> last_el"
+  shows "pos (succ x) = pos x + 1"
+proof -
+  have "x \<le> 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 \<in> 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 \<noteq> first_el"
+  shows "pos (pred x) = pos x - 1"
+proof -
+  have "first_el \<le> 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 \<in> 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 \<in> range pos \<Longrightarrow> succ (val x) = val (x + 1)"
+  by (simp add: succ_def pos_val)
+
+lemma pred_val: "x \<in> range pos \<Longrightarrow> pred (val x) = val (x - 1)"
+  by (simp add: pred_def pos_val)
+
+end
+
+lemma interval_expand:
+  "x < y \<Longrightarrow> (z::int) \<in> {x..<y} = (z = x \<or> z \<in> {x+1..<y})"
+  by auto
+
+
+text {* Load the package *}
+
+use "Tools/spark_vcs.ML"
+use "Tools/spark_commands.ML"
+
+setup SPARK_Commands.setup
+
+end