UNITY fully working at last...
authorpaulson
Wed Mar 03 10:50:42 1999 +0100 (1999-03-03)
changeset 62991a88db6e7c7e
parent 6298 a336f80158c8
child 6300 3815b5b095cb
UNITY fully working at last...
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Comp.ML	Wed Mar 03 10:36:24 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Wed Mar 03 10:50:42 1999 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4  qed "guaranteesI";
     1.5  
     1.6  Goalw [guarantees_def, component_def]
     1.7 -     "[| F : X guarantees Y;  F Join G : X;  compatible{F,G} |] \
     1.8 +     "[| F : X guarantees Y;  F Join G : X |] \
     1.9  \     ==> F Join G : Y";
    1.10  by (Blast_tac 1);
    1.11  qed "guaranteesD";
     2.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Mar 03 10:36:24 1999 +0100
     2.2 +++ b/src/HOL/UNITY/PPROD.ML	Wed Mar 03 10:50:42 1999 +0100
     2.3 @@ -21,7 +21,13 @@
     2.4  qed "lift_act_Id";
     2.5  Addsimps [lift_act_Id];
     2.6  
     2.7 -Goalw [lift_prog_def] "Init (lift_prog i F) = {f. f i : Init F}";
     2.8 +(*NEEDED????????????????????????????????????????????????????????????????*)
     2.9 +Goal "Id : lift_act i `` Acts F";
    2.10 +by (auto_tac (claset() addSIs [lift_act_Id RS sym], 
    2.11 +	      simpset() addsimps [image_iff]));
    2.12 +qed "Id_mem_lift_act";
    2.13 +
    2.14 +Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    2.15  by Auto_tac;
    2.16  qed "Init_lift_prog";
    2.17  Addsimps [Init_lift_prog];
    2.18 @@ -41,25 +47,20 @@
    2.19  qed "lift_act_eq";
    2.20  AddIffs [lift_act_eq];
    2.21  
    2.22 -Goal "i: I ==> Acts (PPROD I F) = (UN i:I. lift_act i `` Acts (F i))";
    2.23 +Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
    2.24  by (auto_tac (claset(),
    2.25  	      simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN]));
    2.26  qed "Acts_PPROD";
    2.27  
    2.28 -Goal "PPROD {} F = SKIP UNIV";
    2.29 -by (simp_tac (simpset() addsimps [PPROD_def]) 1);
    2.30 -qed "Acts_PPROD";
    2.31 -
    2.32 -Goal "i : I ==> (PPI i: I. SKIP A) = SKIP (INT i:I. lift_set i A)";
    2.33 -by (auto_tac (claset() addSIs [program_equalityI],
    2.34 -	      simpset() addsimps [eqStates_def, Acts_lift_prog, 
    2.35 -				  SKIP_def, Acts_PPROD]));
    2.36 -qed "PPROD_SKIP";
    2.37 -
    2.38  Goal "PPROD {} F = SKIP";
    2.39  by (simp_tac (simpset() addsimps [PPROD_def]) 1);
    2.40  qed "PPROD_empty";
    2.41  
    2.42 +Goal "(PPI i: I. SKIP) = SKIP";
    2.43 +by (auto_tac (claset() addSIs [program_equalityI],
    2.44 +	      simpset() addsimps [Acts_lift_prog, SKIP_def, Acts_PPROD]));
    2.45 +qed "PPROD_SKIP";
    2.46 +
    2.47  Addsimps [PPROD_SKIP, PPROD_empty];
    2.48  
    2.49  Goalw [PPROD_def]
    2.50 @@ -132,18 +133,21 @@
    2.51  
    2.52  (** invariant **)
    2.53  
    2.54 +(*????????????????*)
    2.55  Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)";
    2.56  by (auto_tac (claset(),
    2.57  	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
    2.58  qed "invariant_imp_lift_prog_invariant";
    2.59  
    2.60 +(*????????????????*)
    2.61  Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A";
    2.62  by (auto_tac (claset(),
    2.63  	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
    2.64  qed "lift_prog_invariant_imp_invariant";
    2.65  
    2.66  (*NOT clear that the previous lemmas help in proving this one.*)
    2.67 -Goal "[| F i : invariant A;  i : I |] ==> PPROD I F : invariant (lift_set i A)";
    2.68 +Goal "[| F i : invariant A;  i : I |] \
    2.69 +\     ==> PPROD I F : invariant (lift_set i A)";
    2.70  by (auto_tac (claset(),
    2.71  	      simpset() addsimps [invariant_def, PPROD_stable]));
    2.72  qed "invariant_imp_PPROD_invariant";
    2.73 @@ -248,10 +252,10 @@
    2.74  by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
    2.75  qed "Constrains_imp_PPROD_Constrains";
    2.76  
    2.77 -Goal "[| ALL i:I. f0 i : R i;  i: I |] \
    2.78 -\     ==> Applyall {f. (ALL i:I. f i : R i) & f i : A} i = R i Int A";
    2.79 -by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI],
    2.80 -	       simpset() addsimps [Applyall_def]) 1);
    2.81 +Goal "[| ALL i:I. f0 i : R i;   i: I |] \
    2.82 +\     ==> Applyall ({f. (ALL i:I. f i : R i)} Int lift_set i A) i = R i Int A";
    2.83 +by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
    2.84 +	       simpset() addsimps [Applyall_def, lift_set_def]) 1);
    2.85  qed "Applyall_Int_depend";
    2.86  
    2.87  (*Again, we need the f0 premise because otherwise Constrains holds trivially
    2.88 @@ -265,8 +269,7 @@
    2.89  by (dtac PPROD_constrains_projection 1);
    2.90  by (assume_tac 1);
    2.91  by (asm_full_simp_tac
    2.92 -    (simpset() addsimps [Applyall_Int_depend, Collect_conj_eq RS sym,
    2.93 -			 reachable_PPROD_eq]) 1);
    2.94 +    (simpset() addsimps [Applyall_Int_depend, reachable_PPROD_eq]) 1);
    2.95  qed "PPROD_Constrains_imp_Constrains";
    2.96  
    2.97  
    2.98 @@ -286,7 +289,8 @@
    2.99  
   2.100  (** PFUN (no dependence on i) doesn't require the f0 premise **)
   2.101  
   2.102 -Goal "i: I ==> Applyall {f. (ALL i:I. f i : R) & f i : A} i = R Int A";
   2.103 +Goal "i: I \
   2.104 +\     ==> Applyall ({f. (ALL i:I. f i : R)} Int lift_set i A) i = R Int A";
   2.105  by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1);
   2.106  qed "Applyall_Int";
   2.107  
     3.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:36:24 1999 +0100
     3.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:50:42 1999 +0100
     3.3 @@ -28,10 +28,8 @@
     3.4  time_use_thy "Lift";
     3.5  time_use_thy "Comp";
     3.6  time_use_thy "Client";
     3.7 -(**
     3.8  time_use_thy "Extend";
     3.9  time_use_thy "PPROD";
    3.10 -**)
    3.11  
    3.12  add_path "../Auth";	(*to find Public.thy*)
    3.13  use_thy"NSP_Bad";
     4.1 --- a/src/HOL/UNITY/Union.ML	Wed Mar 03 10:36:24 1999 +0100
     4.2 +++ b/src/HOL/UNITY/Union.ML	Wed Mar 03 10:50:42 1999 +0100
     4.3 @@ -167,12 +167,6 @@
     4.4  by (Blast_tac 1);
     4.5  qed "constrains_imp_JN_constrains";
     4.6  
     4.7 -Goal "[| i : I;  compatible (F``I) |] \
     4.8 -\     ==> (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
     4.9 -by (asm_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
    4.10 -by (Blast_tac 1);
    4.11 -qed "constrains_JN";
    4.12 -
    4.13      (**FAILS, I think; see 5.4.1, Substitution Axiom.
    4.14         The problem is to relate reachable (F Join G) with 
    4.15         reachable F and reachable G