# File Abstraction.ML

    (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
        ID:         $Id: Abstraction.ML,v 1.18 2005/09/02 15:23:59 wenzelm Exp $
        Author:     Olaf Müller
    *)

    section "cex_abs";

    (* ---------------------------------------------------------------- *)
    (*                             cex_abs                              *)
    (* ---------------------------------------------------------------- *)

    Goal "cex_abs f (s,UU) = (f s, UU)";
    by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    qed"cex_abs_UU";

    Goal "cex_abs f (s,nil) = (f s, nil)";
    by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    qed"cex_abs_nil";

    Goal "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))";
    by (simp_tac (simpset() addsimps [cex_abs_def]) 1);
    qed"cex_abs_cons";

    Addsimps [cex_abs_UU, cex_abs_nil, cex_abs_cons];

    section "lemmas";

    (* ---------------------------------------------------------------- *)
    (*                           Lemmas                                 *)
    (* ---------------------------------------------------------------- *)

    Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
    by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
         NOT_def,temp_sat_def,satisfies_def]) 1);
    by Auto_tac;
    qed"temp_weakening_def2";

    Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
    by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
         NOT_def]) 1);
    by Auto_tac;
    qed"state_weakening_def2";

    section "Abstraction Rules for Properties";

    (* ---------------------------------------------------------------- *)
    (*                Abstraction Rules for Properties                  *)
    (* ---------------------------------------------------------------- *)

    Goalw [cex_abs_def]
     "[| is_abstraction h C A |] ==>\
    \ !s. reachable C s & is_exec_frag C (s,xs) \
    \ --> is_exec_frag A (cex_abs h (s,xs))";

    by (Asm_full_simp_tac 1);
    by (pair_induct_tac "xs" [is_exec_frag_def] 1);
    (* main case *)
    by (safe_tac set_cs);
    by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
    by (forward_tac [reachable.reachable_n] 1);
    by (assume_tac 1);
    by (Asm_full_simp_tac 1);
    qed_spec_mp"exec_frag_abstraction";

    Goal "is_abstraction h C A ==> weakeningIOA A C h";
    by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
    by Auto_tac;
    by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    (* start state *)
    by (rtac conjI 1);
    by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
    (* is-execution-fragment *)
    by (etac exec_frag_abstraction 1);
    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
    qed"abs_is_weakening";

    Goal "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
    \         ==> validIOA C P";
    by (dtac abs_is_weakening 1);
    by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def,
        validIOA_def, temp_strengthening_def])1);
    by (safe_tac set_cs);
    by (pair_tac "ex" 1);
    qed"AbsRuleT1";

    (* FIX: Nach TLS.ML *)

    Goal "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))";
    by (simp_tac (simpset() addsimps [IMPLIES_def,temp_sat_def, satisfies_def])1);
    qed"IMPLIES_temp_sat";

    Goal "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))";
    by (simp_tac (simpset() addsimps [AND_def,temp_sat_def, satisfies_def])1);
    qed"AND_temp_sat";

    Goal "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))";
    by (simp_tac (simpset() addsimps [OR_def,temp_sat_def, satisfies_def])1);
    qed"OR_temp_sat";

    Goal "(ex |== .~ P) = (~ (ex |== P))";
    by (simp_tac (simpset() addsimps [NOT_def,temp_sat_def, satisfies_def])1);
    qed"NOT_temp_sat";

    Addsimps [IMPLIES_temp_sat,AND_temp_sat,OR_temp_sat,NOT_temp_sat];

    Goalw [is_live_abstraction_def]
       "[|is_live_abstraction h (C,L) (A,M); \
    \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
    \         ==> validLIOA (C,L) P";
    by Auto_tac;
    by (dtac abs_is_weakening 1);
    by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
        validLIOA_def, validIOA_def, temp_strengthening_def])1);
    by (safe_tac set_cs);
    by (pair_tac "ex" 1);
    qed"AbsRuleT2";

    Goalw [is_live_abstraction_def]
       "[|is_live_abstraction h (C,L) (A,M); \
    \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
    \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
    \         ==> validLIOA (C,L) P";
    by Auto_tac;
    by (dtac abs_is_weakening 1);
    by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
        validLIOA_def, validIOA_def, temp_strengthening_def])1);
    by (safe_tac set_cs);
    by (pair_tac "ex" 1);
    qed"AbsRuleTImprove";

    section "Correctness of safe abstraction";

    (* ---------------------------------------------------------------- *)
    (*              Correctness of safe abstraction                     *)
    (* ---------------------------------------------------------------- *)

    Goalw [is_abstraction_def,is_ref_map_def]
    "is_abstraction h C A ==> is_ref_map h C A";
    by (safe_tac set_cs);
    by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
    by (asm_full_simp_tac (simpset() addsimps [move_def])1);
    qed"abstraction_is_ref_map";

    Goal "[| inp(C)=inp(A); out(C)=out(A); \
    \                  is_abstraction h C A |] \
    \               ==> C =<| A";
    by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
    by (rtac trace_inclusion 1);
    by (simp_tac (simpset() addsimps [externals_def])1);
    by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
    by (etac abstraction_is_ref_map 1);
    qed"abs_safety";

    section "Correctness of life abstraction";

    (* ---------------------------------------------------------------- *)
    (*              Correctness of life abstraction                     *)
    (* ---------------------------------------------------------------- *)

    (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
       that is to special Map Lemma *)
    Goalw [cex_abs_def,mk_trace_def,filter_act_def]
      "ext C = ext A \
    \        ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))";
    by (Asm_full_simp_tac 1);
    by (pair_induct_tac "xs" [] 1);
    qed"traces_coincide_abs";

    (* Does not work with abstraction_is_ref_map as proof of abs_safety, because
       is_live_abstraction includes temp_strengthening which is necessarily based
       on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
       way for cex_abs *)
    Goal "[| inp(C)=inp(A); out(C)=out(A); \
    \                  is_live_abstraction h (C,M) (A,L) |] \
    \               ==> live_implements (C,M) (A,L)";

    by (asm_full_simp_tac (simpset() addsimps [is_live_abstraction_def, live_implements_def,
    livetraces_def,liveexecutions_def]) 1);
    by (safe_tac set_cs);
    by (res_inst_tac[("x","cex_abs h ex")] exI 1);
    by (safe_tac set_cs);
      (* Traces coincide *)
      by (pair_tac "ex" 1);
      by (rtac traces_coincide_abs 1);
      by (simp_tac (simpset() addsimps [externals_def])1);
      by (SELECT_GOAL (auto_tac (claset(),simpset()))1);

      (* cex_abs is execution *)
      by (pair_tac "ex" 1);
      by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
      (* start state *)
      by (rtac conjI 1);
      by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def,cex_abs_def]) 1);
      (* is-execution-fragment *)
      by (etac exec_frag_abstraction 1);
      by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);

     (* Liveness *)
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2]) 1);
     by (pair_tac "ex" 1);
    qed"abs_liveness";

    (* FIX: NAch Traces.ML bringen *)

    Goalw [ioa_implements_def]
    "[| A =<| B; B =<| C|] ==> A =<| C";
    by Auto_tac;
    qed"implements_trans";

    section "Abstraction Rules for Automata";

    (* ---------------------------------------------------------------- *)
    (*                Abstraction Rules for Automata                    *)
    (* ---------------------------------------------------------------- *)

    Goal "[| inp(C)=inp(A); out(C)=out(A); \
    \                  inp(Q)=inp(P); out(Q)=out(P); \
    \                  is_abstraction h1 C A; \
    \                  A =<| Q ; \
    \                  is_abstraction h2 Q P |] \
    \               ==> C =<| P";
    by (dtac abs_safety 1);
    by (REPEAT (atac 1));
    by (dtac abs_safety 1);
    by (REPEAT (atac 1));
    by (etac implements_trans 1);
    by (etac implements_trans 1);
    by (assume_tac 1);
    qed"AbsRuleA1";

    Goal "!!LC. [| inp(C)=inp(A); out(C)=out(A); \
    \                  inp(Q)=inp(P); out(Q)=out(P); \
    \                  is_live_abstraction h1 (C,LC) (A,LA); \
    \                  live_implements (A,LA) (Q,LQ) ; \
    \                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
    \               ==> live_implements (C,LC) (P,LP)";
    by (dtac abs_liveness 1);
    by (REPEAT (atac 1));
    by (dtac abs_liveness 1);
    by (REPEAT (atac 1));
    by (etac live_implements_trans 1);
    by (etac live_implements_trans 1);
    by (assume_tac 1);
    qed"AbsRuleA2";

    Delsimps [split_paired_All];

    section "Localizing Temporal Strengthenings and Weakenings";

    (* ---------------------------------------------------------------- *)
    (*                Localizing Temproal Strengthenings - 1               *)
    (* ---------------------------------------------------------------- *)

    Goalw [temp_strengthening_def]
    "[| temp_strengthening P1 Q1 h; \
    \         temp_strengthening P2 Q2 h |] \
    \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
    by Auto_tac;
    qed"strength_AND";

    Goalw [temp_strengthening_def]
    "[| temp_strengthening P1 Q1 h; \
    \         temp_strengthening P2 Q2 h |] \
    \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
    by Auto_tac;
    qed"strength_OR";

    Goalw [temp_strengthening_def]
    "[| temp_weakening P Q h |] \
    \      ==> temp_strengthening (.~ P) (.~ Q) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    by Auto_tac;
    qed"strength_NOT";

    Goalw [temp_strengthening_def]
    "[| temp_weakening P1 Q1 h; \
    \         temp_strengthening P2 Q2 h |] \
    \      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    qed"strength_IMPLIES";

    (* ---------------------------------------------------------------- *)
    (*                Localizing Temproal Weakenings - Part 1           *)
    (* ---------------------------------------------------------------- *)

    Goal
    "[| temp_weakening P1 Q1 h; \
    \         temp_weakening P2 Q2 h |] \
    \      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    qed"weak_AND";

    Goal
    "[| temp_weakening P1 Q1 h; \
    \         temp_weakening P2 Q2 h |] \
    \      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    qed"weak_OR";

    Goalw [temp_strengthening_def]
    "[| temp_strengthening P Q h |] \
    \      ==> temp_weakening (.~ P) (.~ Q) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    by Auto_tac;
    qed"weak_NOT";

    Goalw [temp_strengthening_def]
    "[| temp_strengthening P1 Q1 h; \
    \         temp_weakening P2 Q2 h |] \
    \      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
    qed"weak_IMPLIES";

    (* ---------------------------------------------------------------- *)
    (*             Localizing Temproal Strengthenings - 2               *)
    (* ---------------------------------------------------------------- *)

    (* ------------------ Box ----------------------------*)

    (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
    Goal "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))";
    by (Seq_case_simp_tac "x" 1);
    by Auto_tac;
    qed"UU_is_Conc";

    Goal
    "Finite s1 --> \
    \ (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))";
    by (rtac impI 1);
    by (Seq_Finite_induct_tac 1);
    by (Blast_tac 1);
    (* main case *)
    by (clarify_tac set_cs 1);
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    (* UU case *)
    by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
    (* nil case *)
    by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
    (* cons case *)
    by (pair_tac "aa" 1);
    by Auto_tac;
    qed_spec_mp"ex2seqConc";

    (* important property of ex2seq: can be shiftet, as defined "pointwise" *)

    Goalw [tsuffix_def,suffix_def]
    "tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
    by Auto_tac;
    by (dtac ex2seqConc 1);
    by Auto_tac;
    qed"ex2seq_tsuffix";

    (* FIX: NAch Sequence.ML bringen *)

    Goal "(Map f$s = nil) = (s=nil)";
    by (Seq_case_simp_tac "s" 1);
    qed"Mapnil";

    Goal "(Map f$s = UU) = (s=UU)";
    by (Seq_case_simp_tac "s" 1);
    qed"MapUU";

    (* important property of cex_absSeq: As it is a 1to1 correspondence,
      properties carry over *)

    Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
    "tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
    by Auto_tac;
    by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
    by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
    by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1);
    by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
    qed"cex_absSeq_tsuffix";

    Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def,
    satisfies_def,Box_def]
    "[| temp_strengthening P Q h |]\
    \      ==> temp_strengthening ([] P) ([] Q) h";
    by (clarify_tac set_cs 1);
    by (ftac ex2seq_tsuffix 1);
    by (clarify_tac set_cs 1);
    by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1);
    by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1);
    qed"strength_Box";

    (* ------------------ Init ----------------------------*)

    Goalw [temp_strengthening_def,state_strengthening_def,
    temp_sat_def,satisfies_def,Init_def,unlift_def]
    "[| state_strengthening P Q h |]\
    \      ==> temp_strengthening (Init P) (Init Q) h";
    by (safe_tac set_cs);
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    qed"strength_Init";

    (* ------------------ Next ----------------------------*)

    Goal
    "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)";
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    by (Seq_case_simp_tac "s" 1);
    by (pair_tac "a" 1);
    qed"TL_ex2seq_UU";

    Goal
    "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)";
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    by (Seq_case_simp_tac "s" 1);
    by (pair_tac "a" 1);
    qed"TL_ex2seq_nil";

    (* FIX: put to Sequence Lemmas *)
    Goal "Map f$(TL$s) = TL$(Map f$s)";
    by (Seq_induct_tac "s" [] 1);
    qed"MapTL";

    (* important property of cex_absSeq: As it is a 1to1 correspondence,
      properties carry over *)

    Goalw [cex_absSeq_def]
    "cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))";
    by (simp_tac (simpset() addsimps [MapTL]) 1);
    qed"cex_absSeq_TL";

    (* important property of ex2seq: can be shiftet, as defined "pointwise" *)

    Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')";
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    by Auto_tac;
    qed"TLex2seq";

    Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    by (Seq_case_simp_tac "s" 1);
    by (pair_tac "a" 1);
    qed"ex2seqnilTL";

    Goalw [temp_strengthening_def,state_strengthening_def,
    temp_sat_def, satisfies_def,Next_def]
    "[| temp_strengthening P Q h |]\
    \      ==> temp_strengthening (Next P) (Next Q) h";
    by (Asm_full_simp_tac 1);
    by (safe_tac set_cs);
    by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    (* cons case *)
    by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
            ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
    by (etac conjE 1);
    by (dtac TLex2seq 1);
    by (assume_tac 1);
    by Auto_tac;
    qed"strength_Next";

    (* ---------------------------------------------------------------- *)
    (*             Localizing Temporal Weakenings     - 2               *)
    (* ---------------------------------------------------------------- *)

    Goal
    "[| state_weakening P Q h |]\
    \      ==> temp_weakening (Init P) (Init Q) h";
    by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
          state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
    by (safe_tac set_cs);
    by (pair_tac "ex" 1);
    by (Seq_case_simp_tac "y" 1);
    by (pair_tac "a" 1);
    qed"weak_Init";

    (* ---------------------------------------------------------------- *)
    (*             Localizing Temproal Strengthenings - 3               *)
    (* ---------------------------------------------------------------- *)

    Goalw [Diamond_def]
    "[| temp_strengthening P Q h |]\
    \      ==> temp_strengthening (<> P) (<> Q) h";
    by (rtac strength_NOT 1);
    by (rtac weak_Box 1);
    by (etac weak_NOT 1);
    qed"strength_Diamond";

    Goalw [Leadsto_def]
    "[| temp_weakening P1 P2 h;\
    \         temp_strengthening Q1 Q2 h |]\
    \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
    by (rtac strength_Box 1);
    by (etac strength_IMPLIES 1);
    by (etac strength_Diamond 1);
    qed"strength_Leadsto";

    (* ---------------------------------------------------------------- *)
    (*             Localizing Temporal Weakenings - 3                   *)
    (* ---------------------------------------------------------------- *)

    Goalw [Diamond_def]
    "[| temp_weakening P Q h |]\
    \      ==> temp_weakening (<> P) (<> Q) h";
    by (rtac weak_NOT 1);
    by (rtac strength_Box 1);
    by (etac strength_NOT 1);
    qed"weak_Diamond";

    Goalw [Leadsto_def]
    "[| temp_strengthening P1 P2 h;\
    \         temp_weakening Q1 Q2 h |]\
    \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
    by (rtac weak_Box 1);
    by (etac weak_IMPLIES 1);
    by (etac weak_Diamond 1);
    qed"weak_Leadsto";

    Goalw [WF_def]
      " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \
    \   ==> temp_weakening (WF A acts) (WF C acts) h";
    by (rtac weak_IMPLIES 1);
    by (rtac strength_Diamond 1);
    by (rtac strength_Box 1);
    by (rtac strength_Init 1);
    by (rtac weak_Box 2);
    by (rtac weak_Diamond 2);
    by (rtac weak_Init 2);
    by (auto_tac (claset(),
                  simpset() addsimps [state_weakening_def,state_strengthening_def,
                                 xt2_def,plift_def,option_lift_def,NOT_def]));
    qed"weak_WF";

    Goalw [SF_def]
      " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \
    \   ==> temp_weakening (SF A acts) (SF C acts) h";
    by (rtac weak_IMPLIES 1);
    by (rtac strength_Box 1);
    by (rtac strength_Diamond 1);
    by (rtac strength_Init 1);
    by (rtac weak_Box 2);
    by (rtac weak_Diamond 2);
    by (rtac weak_Init 2);
    by (auto_tac (claset(),
                  simpset() addsimps [state_weakening_def,state_strengthening_def,
                                 xt2_def,plift_def,option_lift_def,NOT_def]));
    qed"weak_SF";

    val weak_strength_lemmas =
        [weak_OR,weak_AND,weak_NOT,weak_IMPLIES,weak_Box,weak_Next,weak_Init,
         weak_Diamond,weak_Leadsto,strength_OR,strength_AND,strength_NOT,
         strength_IMPLIES,strength_Box,strength_Next,strength_Init,
         strength_Diamond,strength_Leadsto,weak_WF,weak_SF];

    fun abstraction_tac i =
        SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas,
                               simpset() addsimps [state_strengthening_def,state_weakening_def])) i;