new thm extend_JN; renamed extend_leadsto
authorpaulson
Mon May 17 10:38:47 1999 +0200 (1999-05-17)
changeset 66479ec7b9723f43
parent 6646 3ea726909fff
child 6648 d70810da5565
new thm extend_JN; renamed extend_leadsto
src/HOL/UNITY/Extend.ML
     1.1 --- a/src/HOL/UNITY/Extend.ML	Mon May 17 10:38:08 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.ML	Mon May 17 10:38:47 1999 +0200
     1.3 @@ -64,6 +64,11 @@
     1.4  qed "extend_set_Int_distrib";
     1.5  
     1.6  Goalw [extend_set_def]
     1.7 +    "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))";
     1.8 +by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
     1.9 +qed "extend_set_INTER_distrib";
    1.10 +
    1.11 +Goalw [extend_set_def]
    1.12      "extend_set h (A - B) = extend_set h A - extend_set h B";
    1.13  by Auto_tac;
    1.14  qed "extend_set_Diff_distrib";
    1.15 @@ -171,6 +176,13 @@
    1.16  qed "extend_Join";
    1.17  Addsimps [extend_Join];
    1.18  
    1.19 +Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";
    1.20 +by (rtac program_equalityI 1);
    1.21 +by (simp_tac (simpset() addsimps [image_UNION, Acts_JN]) 2);
    1.22 +by (simp_tac (simpset() addsimps [extend_set_INTER_distrib]) 1);
    1.23 +qed "extend_JN";
    1.24 +Addsimps [extend_JN];
    1.25 +
    1.26  
    1.27  (*** Safety: co, stable ***)
    1.28  
    1.29 @@ -223,6 +235,10 @@
    1.30  by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1);
    1.31  qed "extend_Stable";
    1.32  
    1.33 +Goal "(extend h F : Always (extend_set h A)) = (F : Always A)";
    1.34 +by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1);
    1.35 +qed "extend_Always";
    1.36 +
    1.37  
    1.38  (*** Progress: transient, ensures ***)
    1.39  
    1.40 @@ -313,13 +329,13 @@
    1.41  by (etac leadsTo_imp_extend_leadsTo 2);
    1.42  by (dtac extend_leadsTo_slice 1);
    1.43  by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
    1.44 -qed "extend_leadsto_eq";
    1.45 +qed "extend_leadsto";
    1.46  
    1.47  Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =  \
    1.48  \     (F : A LeadsTo B)";
    1.49  by (simp_tac
    1.50      (simpset() addsimps [LeadsTo_def, reachable_extend_eq, 
    1.51 -			 extend_leadsto_eq, extend_set_Int_distrib RS sym]) 1);
    1.52 +			 extend_leadsto, extend_set_Int_distrib RS sym]) 1);
    1.53  qed "extend_LeadsTo";
    1.54  
    1.55