src/HOL/UNITY/UNITY_tactics.ML
changeset 42767 e6d920bea7a6
parent 37936 1e4c5015a72e
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:17:32 2011 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:18:06 2011 +0200
     1.3 @@ -13,7 +13,11 @@
     1.4  
     1.5  (*Proves "co" properties when the program is specified.  Any use of invariants
     1.6    (from weak constrains) must have been done already.*)
     1.7 -fun constrains_tac(cs,ss) i =
     1.8 +fun constrains_tac ctxt i =
     1.9 +  let
    1.10 +    val cs = claset_of ctxt;
    1.11 +    val ss = simpset_of ctxt;
    1.12 +  in
    1.13     SELECT_GOAL
    1.14        (EVERY [REPEAT (Always_Int_tac 1),
    1.15                (*reduce the fancy safety properties to "constrains"*)
    1.16 @@ -28,10 +32,15 @@
    1.17                full_simp_tac ss 1,
    1.18                REPEAT (FIRSTGOAL (etac disjE)),
    1.19                ALLGOALS (clarify_tac cs),
    1.20 -              ALLGOALS (asm_full_simp_tac ss)]) i;
    1.21 +              ALLGOALS (asm_full_simp_tac ss)]) i
    1.22 +  end;
    1.23  
    1.24  (*proves "ensures/leadsTo" properties when the program is specified*)
    1.25 -fun ensures_tac(cs,ss) sact =
    1.26 +fun ensures_tac ctxt sact =
    1.27 +  let
    1.28 +    val cs = claset_of ctxt;
    1.29 +    val ss = simpset_of ctxt;
    1.30 +  in
    1.31      SELECT_GOAL
    1.32        (EVERY [REPEAT (Always_Int_tac 1),
    1.33                etac @{thm Always_LeadsTo_Basis} 1
    1.34 @@ -46,9 +55,10 @@
    1.35                  [(("act", 0), sact)] @{thm transientI} 2,
    1.36                   (*simplify the command's domain*)
    1.37                simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    1.38 -              constrains_tac (cs,ss) 1,
    1.39 +              constrains_tac ctxt 1,
    1.40                ALLGOALS (clarify_tac cs),
    1.41 -              ALLGOALS (asm_lr_simp_tac ss)]);
    1.42 +              ALLGOALS (asm_lr_simp_tac ss)])
    1.43 +  end;
    1.44  
    1.45  
    1.46  (*Composition equivalences, from Lift_prog*)