Working version after a FAILED attempt to base Follows upon LeadsETo
authorpaulson
Wed Dec 22 17:18:03 1999 +0100 (1999-12-22)
changeset 807436a6c38e0eca
parent 8073 6c99b44b333e
child 8075 93b62f856af7
Working version after a FAILED attempt to base Follows upon LeadsETo
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
     1.1 --- a/src/HOL/UNITY/Follows.ML	Wed Dec 22 17:16:53 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Wed Dec 22 17:18:03 1999 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4  by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
     1.5  qed "mono_LeadsTo_o";
     1.6  
     1.7 +(*NOT PROVABLE USING leadsETo because givenBy f <= givenBy (h o f) fails*)
     1.8  Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
     1.9  by (Clarify_tac 1);
    1.10  by (asm_full_simp_tac
    1.11 @@ -30,17 +31,34 @@
    1.12  			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
    1.13  qed "mono_Follows_o";
    1.14  
    1.15 +(*NOT PROVABLE USING leadsETo since it needs the previous thm*)
    1.16  Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
    1.17  by (dtac mono_Follows_o 1);
    1.18  by (force_tac (claset(), simpset() addsimps [o_def]) 1);
    1.19  qed "mono_Follows_apply";
    1.20  
    1.21 +(*NOT PROVABLE USING leadsETo since givenBy g doesn't imply givenBy f*)
    1.22  Goalw [Follows_def]
    1.23       "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
    1.24  by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.25  by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
    1.26  qed "Follows_trans";
    1.27  
    1.28 +(*
    1.29 +try:
    1.30 +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.31 +auto();
    1.32 +by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1);
    1.33 +br LeadsETo_Trans 1;
    1.34 +by (Blast_tac 2);
    1.35 +bd spec 1;
    1.36 +be LeadsETo_weaken 1;
    1.37 +auto();
    1.38 +by (thin_tac "All ?P" 1);
    1.39 +by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    1.40 +by Safe_tac;
    1.41 +**)
    1.42 +
    1.43  
    1.44  (** Destructiom rules **)
    1.45  
    1.46 @@ -92,14 +110,11 @@
    1.47  by (Blast_tac 1);
    1.48  qed "Always_Un";
    1.49  
    1.50 -
    1.51 -
    1.52  Goalw [Increasing_def]
    1.53       "F : Increasing f ==> F : Stable {s. x <= f s}";
    1.54  by (Blast_tac 1);
    1.55  qed "IncreasingD";
    1.56  
    1.57 -
    1.58  (*Lemma to re-use the argument that one variable increases (progress)
    1.59    while the other variable doesn't decrease (safety)*)
    1.60  Goal "[| F : Increasing f; F : Increasing g; \
     2.1 --- a/src/HOL/UNITY/Follows.thy	Wed Dec 22 17:16:53 1999 +0100
     2.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Dec 22 17:18:03 1999 +0100
     2.3 @@ -4,9 +4,12 @@
     2.4      Copyright   1998  University of Cambridge
     2.5  
     2.6  The Follows relation of Charpentier and Sivilotte
     2.7 +
     2.8 +The safety conditions ensures that "givenBy f" is implementable in the
     2.9 +  progress part: g cannot do anything silly.
    2.10  *)
    2.11  
    2.12 -Follows = Union +
    2.13 +Follows = ELT +
    2.14  
    2.15  constdefs
    2.16