src/HOL/UNITY/ELT.thy
changeset 13812 91713a1915ee
parent 13798 4c1a53627500
child 13819 78f5885b76a9
     1.1 --- a/src/HOL/UNITY/ELT.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/ELT.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -281,22 +281,11 @@
     1.4       "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]  
     1.5      ==> F : A leadsTo[CC] (B' Un A')"
     1.6  apply (rule leadsETo_cancel1)
     1.7 -prefer 2 apply assumption
     1.8 -apply (simp_all (no_asm_simp))
     1.9 + prefer 2 apply assumption
    1.10 +apply simp_all
    1.11  done
    1.12  
    1.13  
    1.14 -(** The impossibility law **)
    1.15 -
    1.16 -lemma leadsETo_empty_lemma: "F : A leadsTo[CC] B ==> B={} --> A={}"
    1.17 -apply (erule leadsETo_induct)
    1.18 -apply (simp_all (no_asm_simp))
    1.19 -apply (unfold ensures_def constrains_def transient_def, blast)
    1.20 -done
    1.21 -
    1.22 -lemma leadsETo_empty: "F : A leadsTo[CC] {} ==> A={}"
    1.23 -by (blast intro!: leadsETo_empty_lemma [THEN mp])
    1.24 -
    1.25  
    1.26  (** PSP: Progress-Safety-Progress **)
    1.27  
    1.28 @@ -367,23 +356,6 @@
    1.29  apply (blast intro: constrains_Int [THEN constrains_weaken])+
    1.30  done
    1.31  
    1.32 -(*useful??*)
    1.33 -lemma Join_leadsETo_stable_imp_leadsETo:
    1.34 -     "[| F Join G : (A leadsTo[CC] B);  ALL C:CC. G : stable C |]  
    1.35 -      ==> F: (A leadsTo[CC] B)"
    1.36 -apply (erule leadsETo_induct)
    1.37 -prefer 3 apply (blast intro: leadsETo_Union)
    1.38 -prefer 2 apply (blast intro: leadsETo_Trans)
    1.39 -apply (rule leadsETo_Basis)
    1.40 -apply (case_tac "A <= B")
    1.41 -apply (erule subset_imp_ensures)
    1.42 -apply (auto intro: constrains_weaken simp add: stable_def ensures_def Join_transient)
    1.43 -apply (erule_tac V = "?F : ?A co ?B" in thin_rl)+
    1.44 -apply (erule transientE)
    1.45 -apply (unfold constrains_def)
    1.46 -apply (blast dest!: bspec)
    1.47 -done
    1.48 -
    1.49  (**** Relationship with traditional "leadsTo", strong & weak ****)
    1.50  
    1.51  (** strong **)
    1.52 @@ -538,18 +510,6 @@
    1.53  done
    1.54  
    1.55  
    1.56 -
    1.57 -(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
    1.58 -lemma (in Extend) 
    1.59 -     "[| G : preserves (v o f);  project h C G : transient D;   
    1.60 -         D : givenBy v |] ==> D={}"
    1.61 -apply (rule stable_transient_empty)
    1.62 - prefer 2 apply assumption
    1.63 -(*If addIs then PROOF FAILED at depth 2*)
    1.64 -apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)
    1.65 -done
    1.66 -
    1.67 -
    1.68  (*This version's stronger in the "ensures" precondition
    1.69    BUT there's no ensures_weaken_L*)
    1.70  lemma (in Extend) Join_project_ensures_strong:
    1.71 @@ -563,20 +523,7 @@
    1.72  apply (auto simp add: Int_Diff)
    1.73  done
    1.74  
    1.75 -(*Generalizes preserves_project_transient_empty*)
    1.76 -lemma (in Extend) preserves_o_project_transient_empty:
    1.77 -     "[| G : preserves (v o f);   
    1.78 -         project h C G : transient (C' Int D);   
    1.79 -         project h C G : stable C';  D : givenBy v |]     
    1.80 -      ==> C' Int D = {}"
    1.81 -apply (rule stable_transient_empty)
    1.82 -prefer 2 apply assumption
    1.83 -(*Fragile proof.  Was just a single blast call.
    1.84 -  If just "intro" then PROOF FAILED at depth 3*)
    1.85 -apply (rule stable_Int) 
    1.86 - apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)+
    1.87 -done
    1.88 -
    1.89 +(*NOT WORKING.  MODIFY AS IN Project.thy
    1.90  lemma (in Extend) pld_lemma:
    1.91       "[| extend h F Join G : stable C;   
    1.92           F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
    1.93 @@ -596,7 +543,7 @@
    1.94   prefer 2
    1.95   apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
    1.96  apply (rule Join_project_ensures_strong)
    1.97 -apply (auto dest: preserves_o_project_transient_empty intro: project_stable_project_set simp add: Int_left_absorb)
    1.98 +apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
    1.99  apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
   1.100  done
   1.101  
   1.102 @@ -652,6 +599,7 @@
   1.103  apply (unfold extending_def)
   1.104  apply (blast intro: project_LeadsETo_D)
   1.105  done
   1.106 +*)
   1.107  
   1.108  
   1.109  (*** leadsETo in the precondition ***)