src/HOL/Hoare/Hoare.ML
author berghofe
Tue, 25 Jun 1996 13:11:29 +0200
changeset 1824 44254696843a
parent 1558 9c6ebfab4e05
child 1875 54c0462f8fb2
permissions -rw-r--r--
Changed argument order of nat_rec.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     1
(*  Title:      HOL/Hoare/Hoare.ML
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     3
    Author:     Norbert Galm & Tobias Nipkow
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
The verification condition generation tactics.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
open Hoare;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
(*** Hoare rules ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    12
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    13
val SkipRule = prove_goalw thy [Spec_def,Skip_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    14
  "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    15
  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    16
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    17
val AssignRule = prove_goalw thy [Spec_def,Assign_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
  "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    21
val SeqRule = prove_goalw thy [Spec_def,Seq_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    22
  "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    23
  (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    25
val IfRule = prove_goalw thy [Spec_def,Cond_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
  "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
\     Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    28
\  ==> Spec p (Cond b c c') r"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
  (fn [prem1,prem2,prem3] =>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    30
     [REPEAT (rtac allI 1),
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    31
      REPEAT (rtac impI 1),
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    32
      dtac prem1 1,
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    33
      cut_facts_tac [prem2,prem3] 1,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    34
      fast_tac (HOL_cs addIs [prem1]) 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    35
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    36
val strenthen_pre = prove_goalw thy [Spec_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    37
  "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    38
  (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    39
                       fast_tac (HOL_cs addIs [prem1]) 1]);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    40
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    41
val [iter_0,iter_Suc] = nat_recs Iter_def;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    42
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    43
val lemma = prove_goalw thy [Spec_def,While_def]
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    44
  "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    45
\  ==> Spec inv (While b inv c) q"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    46
  (fn [prem1,prem2] =>
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    47
     [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    48
      etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    49
      res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    50
      simp_tac (!simpset addsimps [iter_0]) 1,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    51
      fast_tac (HOL_cs addIs [prem2]) 1,
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1465
diff changeset
    52
      simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    53
      cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    54
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    55
val WhileRule = lemma RSN (2,strenthen_pre);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    56
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    57
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    58
(*** meta_spec used in StateElimTac ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    59
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    60
val meta_spec = prove_goal HOL.thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    61
  "(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    62
  (fn prems => [resolve_tac prems 1]);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    63
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    64
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    65
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    66
(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    67
(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)"        ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    68
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    69
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    70
(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    71
   mit Namen von in nach um *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    72
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    73
fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    74
                                                then Abs (nach,t,rename_abs (von,nach,trm))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    75
                                                else Abs (s,t,rename_abs (von,nach,trm))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    76
  | rename_abs (von,nach,trm1 $ trm2)   =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    77
  | rename_abs (_,_,trm)                =trm;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    78
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    79
(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    80
   mit Namen von in nach um. Vorgehen:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    81
        - Term t zu thoerem bestimmen
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    82
        - Term t' zu t durch Umbenennen der Namen generieren
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    83
        - Certified Term ct' zu t' erstellen
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    84
        - Thoerem ct'==ct' anlegen
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    85
        - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct'
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    86
          abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    87
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    88
fun ren_abs_thm (von,nach,theorem)      =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    89
        equal_elim
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    90
                (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    91
                        reflexive (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    92
                                cterm_of
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    93
                                        (#sign (rep_thm theorem))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    94
                                        (rename_abs (von,nach,#prop (rep_thm theorem)))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    95
                        )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    96
                )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
    97
                theorem;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    98
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    99
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   100
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   101
(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch                         ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   102
(***  - Umbenennen von Lambda-Abstraktionen im Theorem                                          ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   103
(***  - Instanziieren von freien Variablen im Theorem                                           ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   104
(***  - Composing des Subgoals mit dem Theorem                                                  ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   105
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   106
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   107
(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   108
   - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   109
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   110
fun comp_inst_ren_tac rens insts theorem i      =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   111
        let
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   112
                fun compose_inst_ren_tac [] insts theorem i                     =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   113
                        compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   114
                  | compose_inst_ren_tac ((von,nach)::rl) insts theorem i       =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   115
                        compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   116
        in
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   117
                compose_inst_ren_tac rens insts theorem i
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   118
        end;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   119
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   120
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   121
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   122
(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen                               ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   123
(***    Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1"               ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   124
(**************************************************************************************************)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   125
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   126
(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   127
   aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   128
        Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a")
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   129
              wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   130
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   131
fun pvars_of_term (name,trm)    =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   132
        let
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   133
                fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   134
                                                                then if trm mem vl
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   135
                                                                        then vl
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   136
                                                                        else trm::vl
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   137
                                                                else add_vars (name,trm,vl)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   138
                  | add_vars (name,Abs (s,t,trm),vl)    =add_vars (name,trm,vl)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   139
                  | add_vars (name,trm1 $ trm2,vl)      =add_vars (name,trm2,add_vars (name,trm1,vl))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   140
                  | add_vars (_,_,vl)                   =vl
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   141
        in
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   142
                add_vars (name,trm,[])
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   143
        end;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   144
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   145
(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   146
   - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   147
   - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   148
                        z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   149
   - namexAll:string    Name von    ^                                  (hier "x")
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   150
   - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   151
   - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   152
   - type_pvar:typ      Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   153
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   154
   Vorgehen:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   155
        - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   156
        - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   157
          z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   158
                meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   159
        - Instanziierungen in meta_spec:
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   160
                varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   161
                varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   162
                 -      zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   163
                        trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   164
                 -      substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   165
                        trm1 = "s(Suc(0)) = xs ==> xs = 1"
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   166
                 -      abstrahiere ueber xs:
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   167
                        trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   168
                 -      abstrahiere ueber restliche Vorkommen von s:
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   169
                        trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   170
                 -      instanziiere varP mit trm3
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   171
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   172
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   173
fun VarsElimTac ([],_,_,_,_,_) i                                        =all_tac
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   174
  | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i        =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   175
        STATE (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   176
                fn state =>
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   177
                comp_inst_ren_tac
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   178
                        [(namexAll,pvar2pvarID v)]
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   179
                        [(
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   180
                                cterm_of (#sign (rep_thm state)) varx,
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   181
                                cterm_of (#sign (rep_thm state)) (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   182
                                        Abs  ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   183
                                )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   184
                        ),(
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   185
                                cterm_of (#sign (rep_thm state)) varP,
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   186
                                cterm_of (#sign (rep_thm state)) (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   187
                                        let
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   188
                                                val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   189
                                                val (sname,trm0) = variant_abs ("s",dummyT,trm);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   190
                                                val xsname = variant_name ("xs",trm0);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   191
                                                val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   192
                                                val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   193
                                        in
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   194
                                                Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   195
                                        end
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   196
                                )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   197
                        )]
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   198
                        meta_spec i
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   199
        )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   200
        THEN
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   201
        (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   202
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   203
(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   204
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   205
   zur Erinnerung:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   206
    -   das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   207
        d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   208
    -   meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   209
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   210
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   211
fun StateElimTac i      =
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   212
        STATE (
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   213
                fn state =>
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   214
                let
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   215
                        val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   216
                        val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   217
                                (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   218
                in
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   219
                        VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   220
                end
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   221
        );
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   222
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   223
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   224
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   225
(*** tactics for verification condition generation ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   226
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   227
(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   228
   von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   229
   generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   230
   Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   231
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   232
fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   233
and HoareRuleTac i pre_cond =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   234
      STATE(fn state =>
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   235
                ((WlpTac i) THEN (HoareRuleTac i pre_cond))
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   236
                ORELSE
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   237
                (FIRST[rtac SkipRule i,
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   238
                       rtac AssignRule i,
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   239
                       EVERY[rtac IfRule i,
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   240
                             HoareRuleTac (i+2) false,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   241
                             HoareRuleTac (i+1) false],
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   242
                       EVERY[rtac WhileRule i,
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   243
                             Asm_full_simp_tac (i+2),
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   244
                             HoareRuleTac (i+1) true]]
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   245
                 THEN
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   246
                 (if pre_cond then (Asm_full_simp_tac i) else (atac i))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   247
                )
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
   248
        );
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   249
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   250
val HoareTac1 =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   251
  EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   252
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   253
val hoare_tac = SELECT_GOAL (HoareTac1);
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   254