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