src/HOL/UNITY/SubstAx.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 14150 9a23e4eb5eb3
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
     1.5  
     1.6  
     1.7 -(*Resembles the previous definition of LeadsTo*)
     1.8 +text{*Resembles the previous definition of LeadsTo*}
     1.9  lemma LeadsTo_eq_leadsTo: 
    1.10       "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
    1.11  apply (unfold LeadsTo_def)
    1.12 @@ -76,7 +76,7 @@
    1.13  lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
    1.14  by (simp add: LeadsTo_def)
    1.15  
    1.16 -(*Useful with cancellation, disjunction*)
    1.17 +text{*Useful with cancellation, disjunction*}
    1.18  lemma LeadsTo_Un_duplicate:
    1.19       "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
    1.20  by (simp add: Un_ac)
    1.21 @@ -91,14 +91,14 @@
    1.22  apply (blast intro: LeadsTo_Union)
    1.23  done
    1.24  
    1.25 -(*Binary union introduction rule*)
    1.26 +text{*Binary union introduction rule*}
    1.27  lemma LeadsTo_Un:
    1.28       "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
    1.29  apply (subst Un_eq_Union)
    1.30  apply (blast intro: LeadsTo_Union)
    1.31  done
    1.32  
    1.33 -(*Lets us look at the starting state*)
    1.34 +text{*Lets us look at the starting state*}
    1.35  lemma single_LeadsTo_I:
    1.36       "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
    1.37  by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
    1.38 @@ -182,8 +182,8 @@
    1.39  apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
    1.40  done
    1.41  
    1.42 -(*Set difference: maybe combine with leadsTo_weaken_L??
    1.43 -  This is the most useful form of the "disjunction" rule*)
    1.44 +text{*Set difference: maybe combine with leadsTo_weaken_L??
    1.45 +  This is the most useful form of the "disjunction" rule*}
    1.46  lemma LeadsTo_Diff:
    1.47       "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
    1.48        ==> F \<in> A LeadsTo C"
    1.49 @@ -198,18 +198,18 @@
    1.50  done
    1.51  
    1.52  
    1.53 -(*Version with no index set*)
    1.54 +text{*Version with no index set*}
    1.55  lemma LeadsTo_UN_UN_noindex: 
    1.56       "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
    1.57  by (blast intro: LeadsTo_UN_UN)
    1.58  
    1.59 -(*Version with no index set*)
    1.60 +text{*Version with no index set*}
    1.61  lemma all_LeadsTo_UN_UN:
    1.62       "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
    1.63        ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
    1.64  by (blast intro: LeadsTo_UN_UN)
    1.65  
    1.66 -(*Binary union version*)
    1.67 +text{*Binary union version*}
    1.68  lemma LeadsTo_Un_Un:
    1.69       "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
    1.70              ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
    1.71 @@ -247,18 +247,18 @@
    1.72  done
    1.73  
    1.74  
    1.75 -(** The impossibility law **)
    1.76 +text{*The impossibility law*}
    1.77  
    1.78 -(*The set "A" may be non-empty, but it contains no reachable states*)
    1.79 -lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
    1.80 +text{*The set "A" may be non-empty, but it contains no reachable states*}
    1.81 +lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
    1.82  apply (simp add: LeadsTo_def Always_eq_includes_reachable)
    1.83  apply (drule leadsTo_empty, auto)
    1.84  done
    1.85  
    1.86  
    1.87 -(** PSP: Progress-Safety-Progress **)
    1.88 +subsection{*PSP: Progress-Safety-Progress*}
    1.89  
    1.90 -(*Special case of PSP: Misra's "stable conjunction"*)
    1.91 +text{*Special case of PSP: Misra's "stable conjunction"*}
    1.92  lemma PSP_Stable:
    1.93       "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
    1.94        ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
    1.95 @@ -336,7 +336,7 @@
    1.96        ==> F \<in> A LeadsTo B"
    1.97  by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
    1.98  
    1.99 -(*Integer version.  Could generalize from 0 to any lower bound*)
   1.100 +text{*Integer version.  Could generalize from 0 to any lower bound*}
   1.101  lemma integ_0_le_induct:
   1.102       "[| F \<in> Always {s. (0::int) \<le> f s};   
   1.103           !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo