src/HOL/UNITY/Extend.ML
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7878 43b03d412b82
     1.1 --- a/src/HOL/UNITY/Extend.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -70,12 +70,17 @@
     1.4  by (Blast_tac 1);
     1.5  qed "extend_set_mono";
     1.6  
     1.7 -Goalw [extend_set_def]
     1.8 -     "z : extend_set h A = (f z : A)";
     1.9 +Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
    1.10  by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
    1.11  qed "mem_extend_set_iff";
    1.12  AddIffs [mem_extend_set_iff]; 
    1.13  
    1.14 +Goalw [extend_set_def]
    1.15 +    "(extend_set h A <= extend_set h B) = (A <= B)";
    1.16 +by (Force_tac 1);
    1.17 +qed "extend_set_strict_mono";
    1.18 +AddIffs [extend_set_strict_mono];
    1.19 +
    1.20  Goal "{s. P (f s)} = extend_set h {s. P s}";
    1.21  by Auto_tac;
    1.22  qed "Collect_eq_extend_set";
    1.23 @@ -177,6 +182,12 @@
    1.24  qed "extend_act_inverse";
    1.25  Addsimps [extend_act_inverse];
    1.26  
    1.27 +(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
    1.28 +Goalw [extend_act_def, project_act_def]
    1.29 +     "act' <= extend_act h act ==> project_act C h act' <= act";
    1.30 +by (Force_tac 1);
    1.31 +qed "subset_extend_act_D";
    1.32 +
    1.33  Goal "inj (extend_act h)";
    1.34  by (rtac inj_on_inverseI 1);
    1.35  by (rtac extend_act_inverse 1);
    1.36 @@ -189,11 +200,12 @@
    1.37  qed "extend_act_Image";
    1.38  Addsimps [extend_act_Image];
    1.39  
    1.40 -Goalw [extend_set_def, extend_act_def]
    1.41 -    "(extend_set h A <= extend_set h B) = (A <= B)";
    1.42 -by (Force_tac 1);
    1.43 -qed "extend_set_strict_mono";
    1.44 -Addsimps [extend_set_strict_mono];
    1.45 +Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)";
    1.46 +by Auto_tac;
    1.47 +qed "extend_act_strict_mono";
    1.48 +
    1.49 +AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq];
    1.50 +(*The latter theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)
    1.51  
    1.52  Goalw [extend_set_def, extend_act_def]
    1.53      "Domain (extend_act h act) = extend_set h (Domain act)";
    1.54 @@ -226,6 +238,12 @@
    1.55  
    1.56  Addsimps [extend_act_Id, project_act_Id];
    1.57  
    1.58 +Goal "(extend_act h act = Id) = (act = Id)";
    1.59 +by Auto_tac;
    1.60 +by (rewtac extend_act_def);
    1.61 +by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
    1.62 +qed "extend_act_Id_iff";
    1.63 +
    1.64  Goal "Id : extend_act h `` Acts F";
    1.65  by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
    1.66  	      simpset() addsimps [image_iff]));
    1.67 @@ -326,26 +344,56 @@
    1.68  by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
    1.69  qed "extend_invariant";
    1.70  
    1.71 +(*Converse fails: A and B may differ in their extra variables*)
    1.72 +Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
    1.73 +by (auto_tac (claset(), 
    1.74 +	      simpset() addsimps [constrains_def, project_set_def]));
    1.75 +by (Force_tac 1);
    1.76 +qed "extend_constrains_project_set";
    1.77 +
    1.78  
    1.79  (*** Diff, needed for localTo ***)
    1.80  
    1.81  Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
    1.82  by (auto_tac (claset() addSIs [program_equalityI],
    1.83  	      simpset() addsimps [Diff_def,
    1.84 -				  inj_extend_act RS image_set_diff RS sym]));
    1.85 +				  inj_extend_act RS image_set_diff]));
    1.86  qed "Diff_extend_eq";
    1.87  
    1.88  Goal "(Diff (extend h G) (extend_act h `` acts) \
    1.89  \         : (extend_set h A) co (extend_set h B)) \
    1.90  \     = (Diff G acts : A co B)";
    1.91  by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
    1.92 -qed "Diff_extend_co";
    1.93 +qed "Diff_extend_constrains";
    1.94  
    1.95  Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
    1.96  \     = (Diff G acts : stable A)";
    1.97 -by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1);
    1.98 +by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
    1.99  qed "Diff_extend_stable";
   1.100  
   1.101 +Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
   1.102 +\     ==> Diff G acts : (project_set h A) co (project_set h B)";
   1.103 +by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
   1.104 +					   extend_constrains_project_set]) 1);
   1.105 +qed "Diff_extend_constrains_project_set";
   1.106 +
   1.107 +Goalw [localTo_def]
   1.108 +     "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
   1.109 +by (simp_tac (simpset() addsimps []) 1);
   1.110 +(*A trick to strip both quantifiers*)
   1.111 +by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
   1.112 +by (stac Collect_eq_extend_set 1);
   1.113 +by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
   1.114 +qed "extend_localTo_extend_eq";
   1.115 +
   1.116 +Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
   1.117 +by (simp_tac (simpset() addsimps [Disjoint_def,
   1.118 +				  inj_extend_act RS image_Int RS sym]) 1);
   1.119 +by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
   1.120 +by (blast_tac (claset() addEs [equalityE]) 1);
   1.121 +qed "Disjoint_extend_eq";
   1.122 +Addsimps [Disjoint_extend_eq];
   1.123 +
   1.124  (*** Weak safety primitives: Co, Stable ***)
   1.125  
   1.126  Goal "p : reachable (extend h F) ==> f p : reachable F";