src/HOL/UNITY/Constrains.ML
changeset 6739 66e4118eead9
parent 6704 5febcf428342
child 6741 540fc00ec32b
equal deleted inserted replaced
6738:06189132c67b 6739:66e4118eead9
   294 qed "Always_weaken";
   294 qed "Always_weaken";
   295 
   295 
   296 
   296 
   297 (*** "Co" rules involving Always ***)
   297 (*** "Co" rules involving Always ***)
   298 
   298 
   299 Goal "[| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A'";
   299 Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')";
   300 by (asm_full_simp_tac
   300 by (asm_simp_tac
   301     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
   301     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
   302 			 Constrains_def, Int_assoc RS sym]) 1);
   302 			 Constrains_def, Int_assoc RS sym]) 1);
   303 qed "Always_ConstrainsI";
   303 qed "Always_Constrains_pre";
   304 
   304 
   305 (* [| F : Always INV; F : (INV Int A) Co A |]
   305 Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')";
   306    ==> F : Stable A *)
   306 by (asm_simp_tac
   307 bind_thm ("Always_StableI", Always_ConstrainsI RS StableI);
       
   308 
       
   309 Goal "[| F : Always INV;  F : A Co A' |]   \
       
   310 \     ==> F : A Co (INV Int A')";
       
   311 by (asm_full_simp_tac
       
   312     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
   307     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
   313 			 Constrains_eq_constrains, Int_assoc RS sym]) 1);
   308 			 Constrains_eq_constrains, Int_assoc RS sym]) 1);
   314 qed "Always_ConstrainsD";
   309 qed "Always_Constrains_post";
   315 
   310 
   316 bind_thm ("Always_StableD", StableD RSN (2,Always_ConstrainsD));
   311 (* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
       
   312 bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
       
   313 
       
   314 (* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
       
   315 bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
   317 
   316 
   318 
   317 
   319 
   318 
   320 (** Conjoining Always properties **)
   319 (** Conjoining Always properties **)
   321 
   320 
   350 	      REPEAT (FIRSTGOAL (etac disjE)),
   349 	      REPEAT (FIRSTGOAL (etac disjE)),
   351 	      ALLGOALS Clarify_tac,
   350 	      ALLGOALS Clarify_tac,
   352 	      ALLGOALS Asm_full_simp_tac]) i;
   351 	      ALLGOALS Asm_full_simp_tac]) i;
   353 
   352 
   354 
   353 
       
   354 leadsTo_wf_induct