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