src/HOL/UNITY/Constrains.ML
changeset 7403 c318acb88251
parent 6741 540fc00ec32b
child 7541 1a7a38d8f5bd
     1.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Sep 01 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Wed Sep 01 11:16:02 1999 +0200
     1.3 @@ -43,7 +43,8 @@
     1.4  
     1.5  (*** Co ***)
     1.6  
     1.7 -overload_1st_set "Constrains.op Co";
     1.8 +(*Needed because its operands are sets*)
     1.9 +overload_1st_set "Constrains.Constrains";
    1.10  
    1.11  (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
    1.12  bind_thm ("constrains_reachable_Int",
    1.13 @@ -341,11 +342,18 @@
    1.14  (*proves "co" properties when the program is specified*)
    1.15  fun constrains_tac i = 
    1.16     SELECT_GOAL
    1.17 -      (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
    1.18 -	      REPEAT (resolve_tac [StableI, stableI,
    1.19 +      (EVERY [REPEAT (Always_Int_tac 1),
    1.20 +	      REPEAT (etac Always_ConstrainsI 1
    1.21 +		      ORELSE
    1.22 +		      resolve_tac [StableI, stableI,
    1.23  				   constrains_imp_Constrains] 1),
    1.24  	      rtac constrainsI 1,
    1.25 -	      Full_simp_tac 1,
    1.26 +	      full_simp_tac (simpset() addsimps !program_defs_ref) 1,
    1.27  	      REPEAT (FIRSTGOAL (etac disjE)),
    1.28  	      ALLGOALS Clarify_tac,
    1.29  	      ALLGOALS Asm_full_simp_tac]) i;
    1.30 +
    1.31 +
    1.32 +(*For proving invariants*)
    1.33 +fun always_tac i = 
    1.34 +    rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;