src/HOL/UNITY/Constrains.ML
changeset 7541 1a7a38d8f5bd
parent 7403 c318acb88251
child 7689 affe0c2fdfbf
equal deleted inserted replaced
7540:8af61a565a4a 7541:1a7a38d8f5bd
   317 
   317 
   318 
   318 
   319 
   319 
   320 (** Conjoining Always properties **)
   320 (** Conjoining Always properties **)
   321 
   321 
       
   322 Goal "Always (A Int B) = Always A Int Always B";
       
   323 by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
       
   324 qed "Always_Int_distrib";
       
   325 
       
   326 Goal "Always (INTER I A) = (INT i:I. Always (A i))";
       
   327 by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
       
   328 qed "Always_INT_distrib";
       
   329 
   322 Goal "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)";
   330 Goal "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)";
   323 by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
   331 by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
   324 qed "Always_Int";
   332 qed "Always_Int_I";
   325 
   333 
   326 (*Delete the nearest invariance assumption (which will be the second one
   334 (*Delete the nearest invariance assumption (which will be the second one
   327   used by Always_Int) *)
   335   used by Always_Int_I) *)
   328 val Always_thin =
   336 val Always_thin =
   329     read_instantiate_sg (sign_of thy)
   337     read_instantiate_sg (sign_of thy)
   330                 [("V", "?F : Always ?A")] thin_rl;
   338                 [("V", "?F : Always ?A")] thin_rl;
   331 
   339 
   332 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   340 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   333 val Always_Int_tac = dtac Always_Int THEN' assume_tac THEN' etac Always_thin;
   341 val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
   334 
   342 
   335 (*Combines a list of invariance THEOREMS into one.*)
   343 (*Combines a list of invariance THEOREMS into one.*)
   336 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int);
   344 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
   337 
   345 
   338 
   346 
   339 (*To allow expansion of the program's definition when appropriate*)
   347 (*To allow expansion of the program's definition when appropriate*)
   340 val program_defs_ref = ref ([] : thm list);
   348 val program_defs_ref = ref ([] : thm list);
   341 
   349