--- a/src/HOL/Hoare/Hoare.ML Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Hoare/Hoare.ML Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Hoare/Hoare.ML
+(* Title: HOL/Hoare/Hoare.ML
ID: $Id$
- Author: Norbert Galm & Tobias Nipkow
+ Author: Norbert Galm & Tobias Nipkow
Copyright 1995 TUM
The verification condition generation tactics.
@@ -29,14 +29,14 @@
(fn [prem1,prem2,prem3] =>
[REPEAT (rtac allI 1),
REPEAT (rtac impI 1),
- dresolve_tac [prem1] 1,
+ dtac 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]);
+ fast_tac (HOL_cs addIs [prem1]) 1]);
val [iter_0,iter_Suc] = nat_recs IterDef;
@@ -70,31 +70,31 @@
(* 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;
+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) *)
+ - 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;
+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;
(**************************************************************************************************)
@@ -107,15 +107,15 @@
(* - 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;
+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;
(**************************************************************************************************)
@@ -125,100 +125,100 @@
(* 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) *)
+ 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;
+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, ...)
+ - 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
+ - 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);
+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,_)
+ - 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
- );
+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
+ );
@@ -232,20 +232,20 @@
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))
+ ((WlpTac i) THEN (HoareRuleTac i pre_cond))
ORELSE
- (FIRST[rtac SkipRule i,
- rtac AssignRule i,
- EVERY[rtac IfRule i,
+ (FIRST[rtac SkipRule i,
+ rtac AssignRule i,
+ EVERY[rtac IfRule i,
HoareRuleTac (i+2) false,
HoareRuleTac (i+1) false],
- EVERY[rtac WhileRule i,
+ EVERY[rtac WhileRule i,
Asm_full_simp_tac (i+2),
HoareRuleTac (i+1) true]]
- THEN
+ THEN
(if pre_cond then (Asm_full_simp_tac i) else (atac i))
- )
- );
+ )
+ );
val HoareTac1 =
EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];