src/HOL/SPARK/SPARK_Setup.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 69605 a96320074298
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/SPARK/SPARK_Setup.thy
     2     Author:     Stefan Berghofer
     3     Copyright:  secunet Security Networks AG
     4 
     5 Setup for SPARK/Ada verification environment.
     6 *)
     7 
     8 theory SPARK_Setup
     9 imports "HOL-Word.Word" "HOL-Word.Bit_Comparison"
    10 keywords
    11   "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
    12   "spark_open" :: thy_load ("siv", "fdl", "rls") and
    13   "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
    14   "spark_vc" :: thy_goal and
    15   "spark_status" :: diag
    16 begin
    17 
    18 ML_file "Tools/fdl_lexer.ML"
    19 ML_file "Tools/fdl_parser.ML"
    20 
    21 text \<open>
    22 SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
    23 \<close>
    24 
    25 definition sdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
    26   "a sdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
    27 
    28 lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
    29   by (simp add: sdiv_def sgn_if)
    30 
    31 lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
    32   by (simp add: sdiv_def sgn_if)
    33 
    34 text \<open>
    35 Correspondence between HOL's and SPARK's version of div
    36 \<close>
    37 
    38 lemma sdiv_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = a div b"
    39   by (simp add: sdiv_def sgn_if)
    40 
    41 lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
    42   by (simp add: sdiv_def sgn_if)
    43 
    44 lemma sdiv_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = - (- a div b)"
    45   by (simp add: sdiv_def sgn_if)
    46 
    47 lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
    48   by (simp add: sdiv_def sgn_if)
    49 
    50 
    51 text \<open>
    52 Updating a function at a set of points. Useful for building arrays.
    53 \<close>
    54 
    55 definition fun_upds :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" where
    56   "fun_upds f xs y z = (if z \<in> xs then y else f z)"
    57 
    58 syntax
    59   "_updsbind" :: "['a, 'a] => updbind"             ("(2_ [:=]/ _)")
    60 
    61 translations
    62   "f(xs[:=]y)" == "CONST fun_upds f xs y"
    63 
    64 lemma fun_upds_in [simp]: "z \<in> xs \<Longrightarrow> (f(xs [:=] y)) z = y"
    65   by (simp add: fun_upds_def)
    66 
    67 lemma fun_upds_notin [simp]: "z \<notin> xs \<Longrightarrow> (f(xs [:=] y)) z = f z"
    68   by (simp add: fun_upds_def)
    69 
    70 lemma upds_singleton [simp]: "f({x} [:=] y) = f(x := y)"
    71   by (simp add: fun_eq_iff)
    72 
    73 
    74 text \<open>Enumeration types\<close>
    75 
    76 class spark_enum = ord + finite +
    77   fixes pos :: "'a \<Rightarrow> int"
    78   assumes range_pos: "range pos = {0..<int (card (UNIV::'a set))}"
    79   and less_pos: "(x < y) = (pos x < pos y)"
    80   and less_eq_pos: "(x \<le> y) = (pos x \<le> pos y)"
    81 begin
    82 
    83 definition "val = inv pos"
    84 
    85 definition "succ x = val (pos x + 1)"
    86 
    87 definition "pred x = val (pos x - 1)"
    88 
    89 lemma inj_pos: "inj pos"
    90   using finite_UNIV
    91   by (rule eq_card_imp_inj_on) (simp add: range_pos)
    92 
    93 lemma val_pos: "val (pos x) = x"
    94   unfolding val_def using inj_pos
    95   by (rule inv_f_f)
    96 
    97 lemma pos_val: "z \<in> range pos \<Longrightarrow> pos (val z) = z"
    98   unfolding val_def
    99   by (rule f_inv_into_f)
   100 
   101 subclass linorder
   102 proof
   103   fix x::'a and y show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
   104     by (simp add: less_pos less_eq_pos less_le_not_le)
   105 next
   106   fix x::'a show "x \<le> x" by (simp add: less_eq_pos)
   107 next
   108   fix x::'a and y z assume "x \<le> y" and "y \<le> z"
   109   then show "x \<le> z" by (simp add: less_eq_pos)
   110 next
   111   fix x::'a and y assume "x \<le> y" and "y \<le> x"
   112   with inj_pos show "x = y"
   113     by (auto dest: injD simp add: less_eq_pos)
   114 next
   115   fix x::'a and y show "x \<le> y \<or> y \<le> x"
   116     by (simp add: less_eq_pos linear)
   117 qed
   118 
   119 definition "first_el = val 0"
   120 
   121 definition "last_el = val (int (card (UNIV::'a set)) - 1)"
   122 
   123 lemma first_el_smallest: "first_el \<le> x"
   124 proof -
   125   have "pos x \<in> range pos" by (rule rangeI)
   126   then have "pos (val 0) \<le> pos x"
   127     by (simp add: range_pos pos_val)
   128   then show ?thesis by (simp add: first_el_def less_eq_pos)
   129 qed
   130 
   131 lemma last_el_greatest: "x \<le> last_el"
   132 proof -
   133   have "pos x \<in> range pos" by (rule rangeI)
   134   then have "pos x \<le> pos (val (int (card (UNIV::'a set)) - 1))"
   135     by (simp add: range_pos pos_val)
   136   then show ?thesis by (simp add: last_el_def less_eq_pos)
   137 qed
   138 
   139 lemma pos_succ:
   140   assumes "x \<noteq> last_el"
   141   shows "pos (succ x) = pos x + 1"
   142 proof -
   143   have "x \<le> last_el" by (rule last_el_greatest)
   144   with assms have "x < last_el" by simp
   145   then have "pos x < pos last_el"
   146     by (simp add: less_pos)
   147   with rangeI [of pos x]
   148   have "pos x + 1 \<in> range pos"
   149     by (simp add: range_pos last_el_def pos_val)
   150   then show ?thesis
   151     by (simp add: succ_def pos_val)
   152 qed
   153 
   154 lemma pos_pred:
   155   assumes "x \<noteq> first_el"
   156   shows "pos (pred x) = pos x - 1"
   157 proof -
   158   have "first_el \<le> x" by (rule first_el_smallest)
   159   with assms have "first_el < x" by simp
   160   then have "pos first_el < pos x"
   161     by (simp add: less_pos)
   162   with rangeI [of pos x]
   163   have "pos x - 1 \<in> range pos"
   164     by (simp add: range_pos first_el_def pos_val)
   165   then show ?thesis
   166     by (simp add: pred_def pos_val)
   167 qed
   168 
   169 lemma succ_val: "x \<in> range pos \<Longrightarrow> succ (val x) = val (x + 1)"
   170   by (simp add: succ_def pos_val)
   171 
   172 lemma pred_val: "x \<in> range pos \<Longrightarrow> pred (val x) = val (x - 1)"
   173   by (simp add: pred_def pos_val)
   174 
   175 end
   176 
   177 lemma interval_expand:
   178   "x < y \<Longrightarrow> (z::int) \<in> {x..<y} = (z = x \<or> z \<in> {x+1..<y})"
   179   by auto
   180 
   181 
   182 text \<open>Load the package\<close>
   183 
   184 ML_file "Tools/spark_vcs.ML"
   185 ML_file "Tools/spark_commands.ML"
   186 
   187 end