(* Title: HOL/Hoare/Hoare.ML
ID: $Id$
Author: Norbert Galm & Tobias Nipkow
Copyright 1995 TUM
The verification condition generation tactics.
*)
open Hoare;
(*** Hoare rules ***)
val SkipRule = prove_goalw thy [SpecDef,SkipDef]
"(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
(fn prems => [fast_tac (HOL_cs addIs prems) 1]);
val AssignRule = prove_goalw thy [SpecDef,AssignDef]
"(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
(fn prems => [fast_tac (HOL_cs addIs prems) 1]);
val SeqRule = prove_goalw thy [SpecDef,SeqDef]
"[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
(fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
val IfRule = prove_goalw thy [SpecDef,CondDef]
"[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
\ Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
\ ==> Spec p (Cond b c c') r"
(fn [prem1,prem2,prem3] =>
[REPEAT (rtac allI 1),
REPEAT (rtac impI 1),
dresolve_tac [prem1] 1,
cut_facts_tac [prem2,prem3] 1,
fast_tac (HOL_cs addIs [prem1]) 1]);
val strenthen_pre = prove_goalw thy [SpecDef]
"[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
(fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
fast_tac (HOL_cs addIs [prem1]) 1]);
val [iter_0,iter_Suc] = nat_recs IterDef;
val lemma = prove_goalw thy [SpecDef,WhileDef]
"[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
\ ==> Spec inv (While b inv c) q"
(fn [prem1,prem2] =>
[REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
simp_tac (!simpset addsimps [iter_0]) 1,
fast_tac (HOL_cs addIs [prem2]) 1,
simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
val WhileRule = lemma RSN (2,strenthen_pre);
(*** meta_spec used in StateElimTac ***)
val meta_spec = prove_goal HOL.thy
"(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))"
(fn prems => [resolve_tac prems 1]);
(**************************************************************************************************)
(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***)
(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)" ***)
(**************************************************************************************************)
(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
mit Namen von in nach um *)
fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
then Abs (nach,t,rename_abs (von,nach,trm))
else Abs (s,t,rename_abs (von,nach,trm))
| rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
| rename_abs (_,_,trm) =trm;
(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen
mit Namen von in nach um. Vorgehen:
- Term t zu thoerem bestimmen
- Term t' zu t durch Umbenennen der Namen generieren
- Certified Term ct' zu t' erstellen
- Thoerem ct'==ct' anlegen
- Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct'
abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *)
fun ren_abs_thm (von,nach,theorem) =
equal_elim
(
reflexive (
cterm_of
(#sign (rep_thm theorem))
(rename_abs (von,nach,#prop (rep_thm theorem)))
)
)
theorem;
(**************************************************************************************************)
(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***)
(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***)
(*** - Instanziieren von freien Variablen im Theorem ***)
(*** - Composing des Subgoals mit dem Theorem ***)
(**************************************************************************************************)
(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
- insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
fun comp_inst_ren_tac rens insts theorem i =
let
fun compose_inst_ren_tac [] insts theorem i =
compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
| compose_inst_ren_tac ((von,nach)::rl) insts theorem i =
compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
in
compose_inst_ren_tac rens insts theorem i
end;
(**************************************************************************************************)
(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***)
(*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***)
(**************************************************************************************************)
(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a")
wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
fun pvars_of_term (name,trm) =
let
fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
then if trm mem vl
then vl
else trm::vl
else add_vars (name,trm,vl)
| add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl)
| add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl))
| add_vars (_,_,vl) =vl
in
add_vars (name,trm,[])
end;
(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
- v::vl:(term) list Liste der zu eliminierenden Programmvariablen
- meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird
z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
- namexAll:string Name von ^ (hier "x")
- varx:term Term zu ^ (hier Var(("x",0),...))
- varP:term Term zu ^ (hier Var(("P",0),...))
- type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
Vorgehen:
- eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
- Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
- Instanziierungen in meta_spec:
varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
- zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
- substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
trm1 = "s(Suc(0)) = xs ==> xs = 1"
- abstrahiere ueber xs:
trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
- abstrahiere ueber restliche Vorkommen von s:
trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
- instanziiere varP mit trm3
*)
fun VarsElimTac ([],_,_,_,_,_) i =all_tac
| VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i =
STATE (
fn state =>
comp_inst_ren_tac
[(namexAll,pvar2pvarID v)]
[(
cterm_of (#sign (rep_thm state)) varx,
cterm_of (#sign (rep_thm state)) (
Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
)
),(
cterm_of (#sign (rep_thm state)) varP,
cterm_of (#sign (rep_thm state)) (
let
val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
val (sname,trm0) = variant_abs ("s",dummyT,trm);
val xsname = variant_name ("xs",trm0);
val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
in
Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
end
)
)]
meta_spec i
)
THEN
(VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
zur Erinnerung:
- das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
- meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
*)
fun StateElimTac i =
STATE (
fn state =>
let
val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
(_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
in
VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
end
);
(*** tactics for verification condition generation ***)
(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall
von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann
generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen
Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
and HoareRuleTac i pre_cond =
STATE(fn state =>
((WlpTac i) THEN (HoareRuleTac i pre_cond))
ORELSE
(FIRST[rtac SkipRule i,
rtac AssignRule i,
EVERY[rtac IfRule i,
HoareRuleTac (i+2) false,
HoareRuleTac (i+1) false],
EVERY[rtac WhileRule i,
Asm_full_simp_tac (i+2),
HoareRuleTac (i+1) true]]
THEN
(if pre_cond then (Asm_full_simp_tac i) else (atac i))
)
);
val HoareTac1 =
EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
val hoare_tac = SELECT_GOAL (HoareTac1);