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