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.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.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.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.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)"
```