src/HOL/UNITY/Extend.thy
changeset 13798 4c1a53627500
parent 13790 8d7e9fce8c50
child 13805 3786b2fd6808
     1.1 --- a/src/HOL/UNITY/Extend.thy	Thu Jan 30 18:08:09 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Fri Jan 31 20:12:44 2003 +0100
     1.3 @@ -3,11 +3,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -Extending of state sets
     1.8 +Extending of state setsExtending of state sets
     1.9    function f (forget)    maps the extended state to the original state
    1.10    function g (forgotten) maps the extended state to the "extending part"
    1.11  *)
    1.12  
    1.13 +header{*Extending State Sets*}
    1.14 +
    1.15  theory Extend = Guar:
    1.16  
    1.17  constdefs
    1.18 @@ -60,7 +62,8 @@
    1.19  (** These we prove OUTSIDE the locale. **)
    1.20  
    1.21  
    1.22 -(*** Restrict [MOVE to Relation.thy?] ***)
    1.23 +subsection{*Restrict*}
    1.24 +(*MOVE to Relation.thy?*)
    1.25  
    1.26  lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)"
    1.27  by (unfold Restrict_def, blast)
    1.28 @@ -130,7 +133,7 @@
    1.29  done
    1.30  
    1.31  
    1.32 -(*** Trivial properties of f, g, h ***)
    1.33 +subsection{*Trivial properties of f, g, h*}
    1.34  
    1.35  lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" 
    1.36  by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
    1.37 @@ -163,7 +166,7 @@
    1.38  
    1.39  
    1.40  
    1.41 -(*** extend_set: basic properties ***)
    1.42 +subsection{*@{term extend_set}: basic properties*}
    1.43  
    1.44  lemma project_set_iff [iff]:
    1.45       "(x : project_set h C) = (EX y. h(x,y) : C)"
    1.46 @@ -210,7 +213,7 @@
    1.47  apply (auto simp add: split_extended_all)
    1.48  done
    1.49  
    1.50 -(*** project_set: basic properties ***)
    1.51 +subsection{*@{term project_set}: basic properties*}
    1.52  
    1.53  (*project_set is simply image!*)
    1.54  lemma (in Extend) project_set_eq: "project_set h C = f ` C"
    1.55 @@ -221,7 +224,7 @@
    1.56  by (auto simp add: split_extended_all)
    1.57  
    1.58  
    1.59 -(*** More laws ***)
    1.60 +subsection{*More laws*}
    1.61  
    1.62  (*Because A and B could differ on the "other" part of the state, 
    1.63     cannot generalize to 
    1.64 @@ -265,7 +268,7 @@
    1.65  by (unfold extend_set_def, auto)
    1.66  
    1.67  
    1.68 -(*** extend_act ***)
    1.69 +subsection{*@{term extend_act}*}
    1.70  
    1.71  (*Can't strengthen it to
    1.72    ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
    1.73 @@ -335,9 +338,9 @@
    1.74  
    1.75  
    1.76  
    1.77 -(**** extend ****)
    1.78 +subsection{*extend ****)
    1.79  
    1.80 -(*** Basic properties ***)
    1.81 +(*** Basic properties*}
    1.82  
    1.83  lemma Init_extend [simp]:
    1.84       "Init (extend h F) = extend_set h (Init F)"
    1.85 @@ -451,7 +454,7 @@
    1.86  by (simp add: component_eq_subset, blast)
    1.87  
    1.88  
    1.89 -(*** Safety: co, stable ***)
    1.90 +subsection{*Safety: co, stable*}
    1.91  
    1.92  lemma (in Extend) extend_constrains:
    1.93       "(extend h F : (extend_set h A) co (extend_set h B)) =  
    1.94 @@ -477,7 +480,7 @@
    1.95  by (simp add: stable_def extend_constrains_project_set)
    1.96  
    1.97  
    1.98 -(*** Weak safety primitives: Co, Stable ***)
    1.99 +subsection{*Weak safety primitives: Co, Stable*}
   1.100  
   1.101  lemma (in Extend) reachable_extend_f:
   1.102       "p : reachable (extend h F) ==> f p : reachable F"
   1.103 @@ -570,7 +573,7 @@
   1.104  by (simp add: stable_def project_constrains_project_set)
   1.105  
   1.106  
   1.107 -(*** Progress: transient, ensures ***)
   1.108 +subsection{*Progress: transient, ensures*}
   1.109  
   1.110  lemma (in Extend) extend_transient:
   1.111       "(extend h F : transient (extend_set h A)) = (F : transient A)"
   1.112 @@ -591,7 +594,7 @@
   1.113  apply (simp add: leadsTo_UN extend_set_Union)
   1.114  done
   1.115  
   1.116 -(*** Proving the converse takes some doing! ***)
   1.117 +subsection{*Proving the converse takes some doing!*}
   1.118  
   1.119  lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
   1.120  by (simp (no_asm) add: slice_def)
   1.121 @@ -631,7 +634,7 @@
   1.122  apply (blast intro: leadsTo_UN)
   1.123  done
   1.124  
   1.125 -lemma (in Extend) extend_leadsTo_slice [rule_format (no_asm)]:
   1.126 +lemma (in Extend) extend_leadsTo_slice [rule_format]:
   1.127       "extend h F : AU leadsTo BU  
   1.128        ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"
   1.129  apply (erule leadsTo_induct)
   1.130 @@ -656,7 +659,7 @@
   1.131                extend_set_Int_distrib [symmetric])
   1.132  
   1.133  
   1.134 -(*** preserves ***)
   1.135 +subsection{*preserves*}
   1.136  
   1.137  lemma (in Extend) project_preserves_I:
   1.138       "G : preserves (v o f) ==> project h C G : preserves v"
   1.139 @@ -677,7 +680,7 @@
   1.140                     constrains_def g_def)
   1.141  
   1.142  
   1.143 -(*** Guarantees ***)
   1.144 +subsection{*Guarantees*}
   1.145  
   1.146  lemma (in Extend) project_extend_Join:
   1.147       "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"