new thms for invariant
authorpaulson
Wed Nov 25 15:53:31 1998 +0100 (1998-11-25)
changeset 597044ff61e1fe82
parent 5969 e4fe567d10e5
child 5971 c5a7a7685826
new thms for invariant
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Union.ML	Wed Nov 25 15:53:04 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Union.ML	Wed Nov 25 15:53:31 1998 +0100
     1.3 @@ -89,12 +89,36 @@
     1.4  Addsimps [Join_absorb];
     1.5  
     1.6  
     1.7 +Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)";
     1.8 +by (auto_tac (claset() addSIs [program_equalityI],
     1.9 +	      simpset() addsimps [Acts_JN, Acts_Join]));
    1.10 +qed "JN_Join_miniscope";
    1.11 +
    1.12 +Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)";
    1.13 +by (auto_tac (claset() addSIs [program_equalityI],
    1.14 +	      simpset() addsimps [Acts_JN, Acts_Join]));
    1.15 +qed "JN_absorb";
    1.16 +
    1.17 +Goal "(JN i: I Un J. A i) = ((JN i: I. A i) Join (JN i:J. A i))";
    1.18 +by (auto_tac (claset() addSIs [program_equalityI],
    1.19 +	      simpset() addsimps [Acts_JN, Acts_Join]));
    1.20 +qed "JN_Join";
    1.21 +
    1.22 +Goal "i: I ==> (JN i:I. c) = c";
    1.23 +by (auto_tac (claset() addSIs [program_equalityI],
    1.24 +	      simpset() addsimps [Acts_JN]));
    1.25 +qed "JN_constant";
    1.26 +
    1.27 +Goal "(JN i:I. A i Join B i) = (JN i:I. A i)  Join  (JN i:I. B i)";
    1.28 +by (auto_tac (claset() addSIs [program_equalityI],
    1.29 +	      simpset() addsimps [Acts_JN, Acts_Join]));
    1.30 +qed "JN_Join_distrib";
    1.31  
    1.32  
    1.33  (*** Safety: constrains, stable, FP ***)
    1.34  
    1.35  Goalw [constrains_def, JOIN_def]
    1.36 -    "I ~= {} ==> \
    1.37 +    "i : I ==> \
    1.38  \    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
    1.39  by (Simp_tac 1);
    1.40  by (Blast_tac 1);
    1.41 @@ -130,24 +154,36 @@
    1.42  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    1.43  qed "constrains_Join_weaken";
    1.44  
    1.45 -Goal "I ~= {} ==> \
    1.46 +Goal "i : I ==> \
    1.47  \     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
    1.48  by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
    1.49  qed "stable_JN";
    1.50  
    1.51 +Goal "[| ALL i:I. F i : invariant A;  i : I |]  \
    1.52 +\      ==> (JN i:I. F i) : invariant A";
    1.53 +by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_JN]) 1);
    1.54 +by (Blast_tac 1);
    1.55 +bind_thm ("invariant_JN_I", ballI RS result());
    1.56 +
    1.57  Goal "F Join G : stable A = \
    1.58  \     (F : stable A & G : stable A)";
    1.59  by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
    1.60  qed "stable_Join";
    1.61  
    1.62 -Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
    1.63 +Goal "[| F : invariant A; G : invariant A |]  \
    1.64 +\     ==> F Join G : invariant A";
    1.65 +by (full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
    1.66 +by (Blast_tac 1);
    1.67 +qed "invariant_JoinI";
    1.68 +
    1.69 +Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
    1.70  by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
    1.71  qed "FP_JN";
    1.72  
    1.73  
    1.74  (*** Progress: transient, ensures ***)
    1.75  
    1.76 -Goal "I ~= {} ==> \
    1.77 +Goal "i : I ==> \
    1.78  \   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
    1.79  by (auto_tac (claset(),
    1.80  	      simpset() addsimps [transient_def, JOIN_def]));
    1.81 @@ -160,7 +196,7 @@
    1.82  				  Join_def]));
    1.83  qed "transient_Join";
    1.84  
    1.85 -Goal "I ~= {} ==> \
    1.86 +Goal "i : I ==> \
    1.87  \     (JN i:I. F i) : ensures A B = \
    1.88  \     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
    1.89  \      (EX i:I. F i : ensures A B))";