src/HOL/Hoare/Hoare.ML

-(*  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.
 *)
 

 \     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,
+      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;
 
 val lemma = prove_goalw thy [SpecDef,WhileDef]
   "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \

 (**************************************************************************************************)
 
 (* 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) *)
-
-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;
+        - 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                                          ***)

 (**************************************************************************************************)
 
 (* - 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;
 
 
 (**************************************************************************************************)
 (*** 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;
+        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, ...)
+   - 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
+        );
 
 
 
 (*** tactics for verification condition generation ***)
 

    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))
+                ((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];
 
 val hoare_tac = SELECT_GOAL (HoareTac1);