src/HOL/Hoare/Hoare_Logic_Abort.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44890 22f665a2e91c
child 48891 c0eafbd55de3
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
wenzelm@41959
     1
(*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
nipkow@13857
     2
    Author:     Leonor Prensa Nieto & Tobias Nipkow
nipkow@13857
     3
    Copyright   2003 TUM
nipkow@13857
     4
nipkow@13857
     5
Like Hoare.thy, but with an Abort statement for modelling run time errors.
nipkow@13857
     6
*)
nipkow@13857
     7
haftmann@35320
     8
theory Hoare_Logic_Abort
wenzelm@28457
     9
imports Main
wenzelm@42153
    10
uses ("hoare_syntax.ML") ("hoare_tac.ML")
wenzelm@24470
    11
begin
nipkow@13857
    12
wenzelm@42174
    13
type_synonym 'a bexp = "'a set"
wenzelm@42174
    14
type_synonym 'a assn = "'a set"
nipkow@13857
    15
nipkow@13857
    16
datatype
nipkow@13857
    17
 'a com = Basic "'a \<Rightarrow> 'a"
nipkow@13857
    18
   | Abort
nipkow@13857
    19
   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
nipkow@13857
    20
   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
nipkow@13857
    21
   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
wenzelm@35113
    22
wenzelm@35054
    23
abbreviation annskip ("SKIP") where "SKIP == Basic id"
nipkow@13857
    24
wenzelm@42174
    25
type_synonym 'a sem = "'a option => 'a option => bool"
nipkow@13857
    26
berghofe@36643
    27
inductive Sem :: "'a com \<Rightarrow> 'a sem"
berghofe@36643
    28
where
berghofe@36643
    29
  "Sem (Basic f) None None"
berghofe@36643
    30
| "Sem (Basic f) (Some s) (Some (f s))"
berghofe@36643
    31
| "Sem Abort s None"
berghofe@36643
    32
| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
berghofe@36643
    33
| "Sem (IF b THEN c1 ELSE c2 FI) None None"
berghofe@36643
    34
| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
berghofe@36643
    35
| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
berghofe@36643
    36
| "Sem (While b x c) None None"
berghofe@36643
    37
| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
berghofe@36643
    38
| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
berghofe@36643
    39
   Sem (While b x c) (Some s) s'"
nipkow@13857
    40
berghofe@36643
    41
inductive_cases [elim!]:
berghofe@36643
    42
  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
berghofe@36643
    43
  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
nipkow@13857
    44
haftmann@35416
    45
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
nipkow@13857
    46
  "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
nipkow@13857
    47
nipkow@13857
    48
wenzelm@35054
    49
syntax
wenzelm@42152
    50
  "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
wenzelm@35054
    51
wenzelm@35054
    52
syntax
haftmann@35320
    53
  "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
wenzelm@35054
    54
                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
wenzelm@35054
    55
syntax ("" output)
haftmann@35320
    56
  "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
wenzelm@35054
    57
                 ("{_} // _ // {_}" [0,55,0] 50)
wenzelm@42152
    58
wenzelm@42153
    59
use "hoare_syntax.ML"
wenzelm@42153
    60
parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
wenzelm@42153
    61
print_translation
wenzelm@42153
    62
  {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
nipkow@13857
    63
nipkow@13857
    64
nipkow@13857
    65
(*** The proof rules ***)
nipkow@13857
    66
nipkow@13857
    67
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
nipkow@13857
    68
by (auto simp:Valid_def)
nipkow@13857
    69
nipkow@13857
    70
lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
nipkow@13857
    71
by (auto simp:Valid_def)
nipkow@13857
    72
nipkow@13857
    73
lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
nipkow@13857
    74
by (auto simp:Valid_def)
nipkow@13857
    75
nipkow@13857
    76
lemma CondRule:
nipkow@13857
    77
 "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
nipkow@13857
    78
  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
nipkow@44890
    79
by (fastforce simp:Valid_def image_def)
nipkow@13857
    80
berghofe@36643
    81
lemma While_aux:
berghofe@36643
    82
  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
berghofe@36643
    83
  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
berghofe@36643
    84
    s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
berghofe@36643
    85
  using assms
berghofe@36643
    86
  by (induct "WHILE b INV {i} DO c OD" s s') auto
nipkow@13857
    87
nipkow@13857
    88
lemma WhileRule:
nipkow@13857
    89
 "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
nipkow@13857
    90
apply(simp add:Valid_def)
nipkow@13857
    91
apply(simp (no_asm) add:image_def)
nipkow@13857
    92
apply clarify
berghofe@36643
    93
apply(drule While_aux)
berghofe@36643
    94
  apply assumption
nipkow@13857
    95
 apply blast
nipkow@13857
    96
apply blast
nipkow@13857
    97
done
nipkow@13857
    98
nipkow@13857
    99
lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
nipkow@13857
   100
by(auto simp:Valid_def)
nipkow@13857
   101
wenzelm@24470
   102
wenzelm@24470
   103
subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *}
wenzelm@24470
   104
wenzelm@24470
   105
lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
wenzelm@24470
   106
  by blast
wenzelm@24470
   107
wenzelm@28457
   108
use "hoare_tac.ML"
nipkow@13857
   109
nipkow@13857
   110
method_setup vcg = {*
wenzelm@30549
   111
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
nipkow@13857
   112
  "verification condition generator"
nipkow@13857
   113
nipkow@13857
   114
method_setup vcg_simp = {*
wenzelm@30549
   115
  Scan.succeed (fn ctxt =>
wenzelm@32149
   116
    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
nipkow@13857
   117
  "verification condition generator plus simplification"
nipkow@13857
   118
nipkow@13875
   119
(* Special syntax for guarded statements and guarded array updates: *)
nipkow@13875
   120
nipkow@13875
   121
syntax
wenzelm@35352
   122
  "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
wenzelm@35352
   123
  "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
nipkow@13875
   124
translations
wenzelm@35101
   125
  "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
haftmann@34940
   126
  "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
nipkow@13875
   127
  (* reverse translation not possible because of duplicate "a" *)
nipkow@13875
   128
nipkow@13875
   129
text{* Note: there is no special syntax for guarded array access. Thus
nipkow@13875
   130
you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *}
nipkow@13875
   131
nipkow@13857
   132
end