src/HOL/UNITY/Extend.thy
author nipkow
Fri, 27 Mar 2020 12:28:05 +0100
changeset 71593 71579bd59cd4
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Extend.thy
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     3
    Copyright   1998  University of Cambridge
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     4
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13790
diff changeset
     5
Extending of state setsExtending of state sets
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     6
  function f (forget)    maps the extended state to the original state
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     7
  function g (forgotten) maps the extended state to the "extending part"
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     8
*)
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
     9
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
    10
section\<open>Extending State Sets\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13790
diff changeset
    11
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13819
diff changeset
    12
theory Extend imports Guar begin
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    13
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    14
definition
8948
b797cfa3548d restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents: 8703
diff changeset
    15
  (*MOVE to Relation.thy?*)
b797cfa3548d restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents: 8703
diff changeset
    16
  Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
61943
7fba644ed827 discontinued ASCII replacement syntax <*>;
wenzelm
parents: 61941
diff changeset
    17
  where "Restrict A r = r \<inter> (A \<times> UNIV)"
8948
b797cfa3548d restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents: 8703
diff changeset
    18
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    19
definition
7482
7badd511844d working snapshot
paulson
parents: 7399
diff changeset
    20
  good_map :: "['a*'b => 'c] => bool"
61941
31f2105521ee discontinued ASCII replacement syntax <->;
wenzelm
parents: 61424
diff changeset
    21
  where "good_map h \<longleftrightarrow> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
7482
7badd511844d working snapshot
paulson
parents: 7399
diff changeset
    22
     (*Using the locale constant "f", this is  f (h (x,y))) = x*)
7badd511844d working snapshot
paulson
parents: 7399
diff changeset
    23
  
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    24
definition
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    25
  extend_set :: "['a*'b => 'c, 'a set] => 'c set"
61943
7fba644ed827 discontinued ASCII replacement syntax <*>;
wenzelm
parents: 61941
diff changeset
    26
  where "extend_set h A = h ` (A \<times> UNIV)"
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    27
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    28
definition
7342
532841541d73 project constants
paulson
parents: 6677
diff changeset
    29
  project_set :: "['a*'b => 'c, 'c set] => 'a set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    30
  where "project_set h C = {x. \<exists>y. h(x,y) \<in> C}"
7342
532841541d73 project constants
paulson
parents: 6677
diff changeset
    31
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    32
definition
7342
532841541d73 project constants
paulson
parents: 6677
diff changeset
    33
  extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    34
  where "extend_act h = (%act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))})"
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    35
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    36
definition
7878
43b03d412b82 working version with localTo[C] instead of localTo
paulson
parents: 7826
diff changeset
    37
  project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    38
  where "project_act h act = {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
7342
532841541d73 project constants
paulson
parents: 6677
diff changeset
    39
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    40
definition
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    41
  extend :: "['a*'b => 'c, 'a program] => 'c program"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    42
  where "extend h F = mk_program (extend_set h (Init F),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    43
                               extend_act h ` Acts F,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    44
                               project_act h -` AllowedActs F)"
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    45
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    46
definition
7878
43b03d412b82 working version with localTo[C] instead of localTo
paulson
parents: 7826
diff changeset
    47
  (*Argument C allows weak safety laws to be projected*)
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    48
  project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 33057
diff changeset
    49
  where "project h C F =
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 8948
diff changeset
    50
       mk_program (project_set h (Init F),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    51
                   project_act h ` Restrict C ` Acts F,
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    52
                   {act. Restrict (project_set h C) act \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
    53
                         project_act h ` Restrict C ` AllowedActs F})"
7342
532841541d73 project constants
paulson
parents: 6677
diff changeset
    54
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
    55
locale Extend =
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    56
  fixes f     :: "'c => 'a"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    57
    and g     :: "'c => 'b"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    58
    and h     :: "'a*'b => 'c"    (*isomorphism between 'a * 'b and 'c *)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    59
    and slice :: "['c set, 'b] => 'a set"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    60
  assumes
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    61
    good_h:  "good_map h"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    62
  defines f_def: "f z == fst (inv h z)"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    63
      and g_def: "g z == snd (inv h z)"
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    64
      and slice_def: "slice Z y == {x. h(x,y) \<in> Z}"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    65
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    66
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    67
(** These we prove OUTSIDE the locale. **)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    68
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    69
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
    70
subsection\<open>Restrict\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13790
diff changeset
    71
(*MOVE to Relation.thy?*)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    72
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    73
lemma Restrict_iff [iff]: "((x,y) \<in> Restrict A r) = ((x,y) \<in> r & x \<in> A)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    74
by (unfold Restrict_def, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    75
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    76
lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    77
apply (rule ext)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    78
apply (auto simp add: Restrict_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    79
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    80
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    81
lemma Restrict_empty [simp]: "Restrict {} r = {}"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    82
by (auto simp add: Restrict_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    83
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    84
lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    85
by (unfold Restrict_def, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    86
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    87
lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    88
by (unfold Restrict_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    89
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    90
lemma Restrict_subset: "Restrict A r \<subseteq> r"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    91
by (unfold Restrict_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    92
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    93
lemma Restrict_eq_mono: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    94
     "[| A \<subseteq> B;  Restrict B r = Restrict B s |]  
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    95
      ==> Restrict A r = Restrict A s"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    96
by (unfold Restrict_def, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    97
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
    98
lemma Restrict_imageI: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    99
     "[| s \<in> RR;  Restrict A r = Restrict A s |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   100
      ==> Restrict A r \<in> Restrict A ` RR"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   101
by (unfold Restrict_def image_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   102
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   103
lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   104
by blast
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   105
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   106
lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   107
by blast
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   108
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   109
(*Possibly easier than reasoning about "inv h"*)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   110
lemma good_mapI: 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   111
     assumes surj_h: "surj h"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   112
         and prem:   "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   113
     shows "good_map h"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   114
apply (simp add: good_map_def) 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   115
apply (safe intro!: surj_h)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   116
apply (rule prem)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   117
apply (subst surjective_pairing [symmetric])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   118
apply (subst surj_h [THEN surj_f_inv_f])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   119
apply (rule refl)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   120
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   121
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   122
lemma good_map_is_surj: "good_map h ==> surj h"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   123
by (unfold good_map_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   124
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   125
(*A convenient way of finding a closed form for inv h*)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   126
lemma fst_inv_equalityI: 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   127
     assumes surj_h: "surj h"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 16417
diff changeset
   128
         and prem:   "!! x y. g (h(x,y)) = x"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   129
     shows "fst (inv h z) = g z"
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 58889
diff changeset
   130
by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   131
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   132
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   133
subsection\<open>Trivial properties of f, g, h\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   134
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   135
context Extend
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   136
begin
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   137
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   138
lemma f_h_eq [simp]: "f(h(x,y)) = x" 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   139
by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   140
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   141
lemma h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   142
apply (drule_tac f = f in arg_cong)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   143
apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   144
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   145
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   146
lemma h_f_g_equiv: "h(f z, g z) == z"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   147
by (simp add: f_def g_def 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   148
            good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   149
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   150
lemma h_f_g_eq: "h(f z, g z) = z"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   151
by (simp add: h_f_g_equiv)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   152
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   153
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   154
lemma split_extended_all:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   155
     "(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   156
proof 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   157
   assume allP: "\<And>z. PROP P z"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   158
   fix u y
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   159
   show "PROP P (h (u, y))" by (rule allP)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   160
 next
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   161
   assume allPh: "\<And>u y. PROP P (h(u,y))"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   162
   fix z
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   163
   have Phfgz: "PROP P (h (f z, g z))" by (rule allPh)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   164
   show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   165
qed 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   166
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   167
end
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   168
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   169
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
   170
subsection\<open>\<^term>\<open>extend_set\<close>: basic properties\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   171
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   172
lemma project_set_iff [iff]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   173
     "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   174
by (simp add: project_set_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   175
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   176
lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   177
by (unfold extend_set_def, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   178
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   179
context Extend
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   180
begin
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   181
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   182
lemma mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   183
apply (unfold extend_set_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   184
apply (force intro: h_f_g_eq [symmetric])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   185
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   186
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   187
lemma extend_set_strict_mono [iff]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   188
     "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   189
by (unfold extend_set_def, force)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   190
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   191
lemma (in -) extend_set_empty [simp]: "extend_set h {} = {}"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   192
by (unfold extend_set_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   193
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   194
lemma extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   195
by auto
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   196
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   197
lemma extend_set_sing: "extend_set h {x} = {s. f s = x}"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   198
by auto
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   199
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   200
lemma extend_set_inverse [simp]: "project_set h (extend_set h C) = C"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   201
by (unfold extend_set_def, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   202
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   203
lemma extend_set_project_set: "C \<subseteq> extend_set h (project_set h C)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   204
apply (unfold extend_set_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   205
apply (auto simp add: split_extended_all, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   206
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   207
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   208
lemma inj_extend_set: "inj (extend_set h)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   209
apply (rule inj_on_inverseI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   210
apply (rule extend_set_inverse)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   211
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   212
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   213
lemma extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   214
apply (unfold extend_set_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   215
apply (auto simp add: split_extended_all)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   216
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   217
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
   218
subsection\<open>\<^term>\<open>project_set\<close>: basic properties\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   219
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   220
(*project_set is simply image!*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   221
lemma project_set_eq: "project_set h C = f ` C"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   222
by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   223
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   224
(*Converse appears to fail*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   225
lemma project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   226
by (auto simp add: split_extended_all)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   227
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   228
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   229
subsection\<open>More laws\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   230
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   231
(*Because A and B could differ on the "other" part of the state, 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   232
   cannot generalize to 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   233
      project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   234
*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   235
lemma project_set_extend_set_Int: "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   236
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   237
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   238
(*Unused, but interesting?*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   239
lemma project_set_extend_set_Un: "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   240
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   241
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   242
lemma (in -) project_set_Int_subset:
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   243
    "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   244
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   245
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   246
lemma extend_set_Un_distrib: "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   247
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   248
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   249
lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   250
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   251
69313
b021008c5397 removed legacy input syntax
haftmann
parents: 67613
diff changeset
   252
lemma extend_set_INT_distrib: "extend_set h (\<Inter>(B ` A)) = (\<Inter>x \<in> A. extend_set h (B x))"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   253
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   254
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   255
lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   256
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   257
61952
546958347e05 prefer symbols for "Union", "Inter";
wenzelm
parents: 61943
diff changeset
   258
lemma extend_set_Union: "extend_set h (\<Union>A) = (\<Union>X \<in> A. extend_set h X)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   259
  by blast
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   260
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   261
lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   262
  by (auto simp: extend_set_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   263
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   264
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69313
diff changeset
   265
subsection\<open>\<^term>\<open>extend_act\<close>\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   266
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   267
(*Can't strengthen it to
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   268
  ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   269
  because h doesn't have to be injective in the 2nd argument*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   270
lemma mem_extend_act_iff [iff]: "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   271
  by (auto simp: extend_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   272
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   273
(*Converse fails: (z,z') would include actions that changed the g-part*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   274
lemma extend_act_D: "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   275
  by (auto simp: extend_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   276
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   277
lemma extend_act_inverse [simp]: "project_act h (extend_act h act) = act"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   278
  unfolding extend_act_def project_act_def by blast
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   279
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   280
lemma project_act_extend_act_restrict [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   281
     "project_act h (Restrict C (extend_act h act)) =  
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   282
      Restrict (project_set h C) act"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   283
  unfolding extend_act_def project_act_def by blast
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   284
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   285
lemma subset_extend_act_D: "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   286
  unfolding extend_act_def project_act_def by force
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   287
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   288
lemma inj_extend_act: "inj (extend_act h)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   289
apply (rule inj_on_inverseI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   290
apply (rule extend_act_inverse)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   291
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   292
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   293
lemma extend_act_Image [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   294
     "extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   295
  unfolding extend_set_def extend_act_def by force
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   296
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   297
lemma extend_act_strict_mono [iff]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   298
     "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   299
  by (auto simp: extend_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   300
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   301
lemma [iff]: "(extend_act h act = extend_act h act') = (act = act')"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   302
  by (rule inj_extend_act [THEN inj_eq])
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   303
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   304
lemma (in -) Domain_extend_act:
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   305
    "Domain (extend_act h act) = extend_set h (Domain act)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   306
  unfolding extend_set_def extend_act_def by force
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   307
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   308
lemma extend_act_Id [simp]: "extend_act h Id = Id"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   309
  unfolding extend_act_def by (force intro: h_f_g_eq [symmetric])
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   310
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   311
lemma project_act_I:  "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   312
  unfolding project_act_def by (force simp add: split_extended_all)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   313
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   314
lemma project_act_Id [simp]: "project_act h Id = Id"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   315
  unfolding project_act_def by force
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   316
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   317
lemma Domain_project_act: "Domain (project_act h act) = project_set h (Domain act)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   318
  unfolding project_act_def by (force simp add: split_extended_all)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   319
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   320
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   321
subsection\<open>extend\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   322
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   323
text\<open>Basic properties\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   324
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   325
lemma (in -) Init_extend [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   326
     "Init (extend h F) = extend_set h (Init F)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   327
  by (auto simp: extend_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   328
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   329
lemma (in -) Init_project [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   330
     "Init (project h C F) = project_set h (Init F)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   331
  by (auto simp: project_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   332
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   333
lemma Acts_extend [simp]: "Acts (extend h F) = (extend_act h ` Acts F)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   334
  by (simp add: extend_def insert_Id_image_Acts)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   335
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   336
lemma AllowedActs_extend [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   337
     "AllowedActs (extend h F) = project_act h -` AllowedActs F"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   338
  by (simp add: extend_def insert_absorb)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   339
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   340
lemma (in -) Acts_project [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   341
     "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   342
  by (auto simp add: project_def image_iff)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   343
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   344
lemma AllowedActs_project [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   345
     "AllowedActs(project h C F) =  
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   346
        {act. Restrict (project_set h C) act  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   347
               \<in> project_act h ` Restrict C ` AllowedActs F}"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   348
apply (simp (no_asm) add: project_def image_iff)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   349
apply (subst insert_absorb)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   350
apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   351
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   352
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   353
lemma Allowed_extend: "Allowed (extend h F) = project h UNIV -` Allowed F"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   354
  by (auto simp add: Allowed_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   355
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   356
lemma extend_SKIP [simp]: "extend h SKIP = SKIP"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   357
apply (unfold SKIP_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   358
apply (rule program_equalityI, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   359
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   360
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   361
lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   362
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   363
61952
546958347e05 prefer symbols for "Union", "Inter";
wenzelm
parents: 61943
diff changeset
   364
lemma (in -) project_set_Union: "project_set h (\<Union>A) = (\<Union>X \<in> A. project_set h X)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   365
  by blast
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   366
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
   367
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   368
(*Converse FAILS: the extended state contributing to project_set h C
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   369
  may not coincide with the one contributing to project_act h act*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   370
lemma (in -) project_act_Restrict_subset:
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   371
     "project_act h (Restrict C act) \<subseteq> Restrict (project_set h C) (project_act h act)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   372
  by (auto simp add: project_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   373
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   374
lemma project_act_Restrict_Id_eq: "project_act h (Restrict C Id) = Restrict (project_set h C) Id"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   375
  by (auto simp add: project_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   376
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   377
lemma project_extend_eq:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   378
     "project h C (extend h F) =  
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   379
      mk_program (Init F, Restrict (project_set h C) ` Acts F,  
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   380
                  {act. Restrict (project_set h C) act 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   381
                          \<in> project_act h ` Restrict C ` 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   382
                                     (project_act h -` AllowedActs F)})"
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   383
apply (rule program_equalityI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   384
  apply simp
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   385
 apply (simp add: image_image)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   386
apply (simp add: project_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   387
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   388
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   389
lemma extend_inverse [simp]:
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   390
     "project h UNIV (extend h F) = F"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   391
apply (simp (no_asm_simp) add: project_extend_eq
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   392
          subset_UNIV [THEN subset_trans, THEN Restrict_triv])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   393
apply (rule program_equalityI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   394
apply (simp_all (no_asm))
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   395
apply (subst insert_absorb)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   396
apply (simp (no_asm) add: bexI [of _ Id])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   397
apply auto
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   398
apply (simp add: image_def)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   399
using project_act_Id apply blast
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   400
apply (simp add: image_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   401
apply (rename_tac "act")
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   402
apply (rule_tac x = "extend_act h act" in exI)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   403
apply simp
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   404
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   405
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   406
lemma inj_extend: "inj (extend h)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   407
apply (rule inj_on_inverseI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   408
apply (rule extend_inverse)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   409
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   410
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   411
lemma extend_Join [simp]: "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   412
apply (rule program_equalityI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   413
apply (simp (no_asm) add: extend_set_Int_distrib)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   414
apply (simp add: image_Un, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   415
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   416
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   417
lemma extend_JN [simp]: "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   418
apply (rule program_equalityI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   419
  apply (simp (no_asm) add: extend_set_INT_distrib)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   420
 apply (simp add: image_UN, auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   421
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   422
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   423
(** These monotonicity results look natural but are UNUSED **)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   424
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   425
lemma extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   426
  by (force simp add: component_eq_subset)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   427
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   428
lemma project_mono: "F \<le> G ==> project h C F \<le> project h C G"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   429
  by (simp add: component_eq_subset, blast)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   430
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   431
lemma all_total_extend: "all_total F ==> all_total (extend h F)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   432
  by (simp add: all_total_def Domain_extend_act)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   433
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   434
subsection\<open>Safety: co, stable\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   435
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   436
lemma extend_constrains:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   437
     "(extend h F \<in> (extend_set h A) co (extend_set h B)) =  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   438
      (F \<in> A co B)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   439
  by (simp add: constrains_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   440
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   441
lemma extend_stable:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   442
     "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   443
  by (simp add: stable_def extend_constrains)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   444
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   445
lemma extend_invariant:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   446
     "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   447
  by (simp add: invariant_def extend_stable)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   448
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   449
(*Projects the state predicates in the property satisfied by  extend h F.
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   450
  Converse fails: A and B may differ in their extra variables*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   451
lemma extend_constrains_project_set:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   452
     "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   453
  by (auto simp add: constrains_def, force)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   454
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   455
lemma extend_stable_project_set:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   456
     "extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   457
  by (simp add: stable_def extend_constrains_project_set)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   458
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   459
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   460
subsection\<open>Weak safety primitives: Co, Stable\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   461
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   462
lemma reachable_extend_f: "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   463
  by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   464
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   465
lemma h_reachable_extend: "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   466
  by (force dest!: reachable_extend_f)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   467
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   468
lemma reachable_extend_eq: "reachable (extend h F) = extend_set h (reachable F)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   469
apply (unfold extend_set_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   470
apply (rule equalityI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   471
apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   472
apply (erule reachable.induct)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   473
apply (force intro: reachable.intros)+
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   474
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   475
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   476
lemma extend_Constrains:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   477
     "(extend h F \<in> (extend_set h A) Co (extend_set h B)) =   
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   478
      (F \<in> A Co B)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   479
  by (simp add: Constrains_def reachable_extend_eq extend_constrains 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   480
              extend_set_Int_distrib [symmetric])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   481
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   482
lemma extend_Stable: "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   483
  by (simp add: Stable_def extend_Constrains)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   484
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   485
lemma extend_Always: "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   486
  by (simp add: Always_def extend_Stable)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   487
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   488
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   489
(** Safety and "project" **)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   490
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   491
(** projection: monotonicity for safety **)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   492
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   493
lemma (in -) project_act_mono:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   494
     "D \<subseteq> C ==>  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   495
      project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   496
  by (auto simp add: project_act_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   497
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   498
lemma project_constrains_mono:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   499
     "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   500
apply (auto simp add: constrains_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   501
apply (drule project_act_mono, blast)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   502
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   503
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   504
lemma project_stable_mono:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   505
     "[| D \<subseteq> C;  project h C F \<in> stable A |] ==> project h D F \<in> stable A"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   506
  by (simp add: stable_def project_constrains_mono)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   507
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   508
(*Key lemma used in several proofs about project and co*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   509
lemma project_constrains: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   510
     "(project h C F \<in> A co B)  =   
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   511
      (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   512
apply (unfold constrains_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   513
apply (auto intro!: project_act_I simp add: ball_Un)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   514
apply (force intro!: project_act_I dest!: subsetD)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   515
(*the <== direction*)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   516
apply (unfold project_act_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   517
apply (force dest!: subsetD)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   518
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   519
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   520
lemma project_stable: "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   521
  by (simp add: stable_def project_constrains)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   522
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   523
lemma project_stable_I: "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   524
apply (drule project_stable [THEN iffD2])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   525
apply (blast intro: project_stable_mono)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   526
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   527
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   528
lemma Int_extend_set_lemma:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   529
     "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   530
  by (auto simp add: split_extended_all)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   531
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   532
(*Strange (look at occurrences of C) but used in leadsETo proofs*)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   533
lemma project_constrains_project_set:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   534
     "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   535
  by (simp add: constrains_def project_def project_act_def, blast)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   536
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   537
lemma project_stable_project_set:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   538
     "G \<in> stable C ==> project h C G \<in> stable (project_set h C)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   539
  by (simp add: stable_def project_constrains_project_set)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   540
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   541
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   542
subsection\<open>Progress: transient, ensures\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   543
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   544
lemma extend_transient:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   545
     "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   546
  by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   547
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   548
lemma extend_ensures:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   549
     "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   550
      (F \<in> A ensures B)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   551
  by (simp add: ensures_def extend_constrains extend_transient 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   552
        extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   553
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   554
lemma leadsTo_imp_extend_leadsTo:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   555
     "F \<in> A leadsTo B  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   556
      ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   557
apply (erule leadsTo_induct)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   558
  apply (simp add: leadsTo_Basis extend_ensures)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   559
 apply (blast intro: leadsTo_Trans)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   560
apply (simp add: leadsTo_UN extend_set_Union)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   561
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   562
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   563
subsection\<open>Proving the converse takes some doing!\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   564
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   565
lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   566
  by (simp add: slice_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   567
61952
546958347e05 prefer symbols for "Union", "Inter";
wenzelm
parents: 61943
diff changeset
   568
lemma slice_Union: "slice (\<Union>S) y = (\<Union>x \<in> S. slice x y)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   569
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   570
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   571
lemma slice_extend_set: "slice (extend_set h A) y = A"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   572
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   573
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   574
lemma project_set_is_UN_slice: "project_set h A = (\<Union>y. slice A y)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   575
  by auto
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   576
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   577
lemma extend_transient_slice:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   578
     "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   579
  by (auto simp: transient_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   580
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   581
(*Converse?*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   582
lemma extend_constrains_slice:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   583
     "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   584
  by (auto simp add: constrains_def)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   585
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   586
lemma extend_ensures_slice:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   587
     "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   588
apply (auto simp add: ensures_def extend_constrains extend_transient)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   589
apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   590
apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   591
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   592
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   593
lemma leadsTo_slice_project_set:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   594
     "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   595
apply (simp add: project_set_is_UN_slice)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   596
apply (blast intro: leadsTo_UN)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   597
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   598
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   599
lemma extend_leadsTo_slice [rule_format]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   600
     "extend h F \<in> AU leadsTo BU  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   601
      ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   602
apply (erule leadsTo_induct)
46577
e5438c5797ae tuned proofs;
wenzelm
parents: 40702
diff changeset
   603
  apply (blast intro: extend_ensures_slice)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   604
 apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   605
apply (simp add: leadsTo_UN slice_Union)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   606
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   607
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   608
lemma extend_leadsTo:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   609
     "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   610
      (F \<in> A leadsTo B)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   611
apply safe
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   612
apply (erule_tac [2] leadsTo_imp_extend_leadsTo)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   613
apply (drule extend_leadsTo_slice)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   614
apply (simp add: slice_extend_set)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   615
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   616
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   617
lemma extend_LeadsTo:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   618
     "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =   
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   619
      (F \<in> A LeadsTo B)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   620
  by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   621
              extend_set_Int_distrib [symmetric])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   622
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   623
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   624
subsection\<open>preserves\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   625
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   626
lemma project_preserves_I:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   627
     "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   628
  by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   629
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   630
(*to preserve f is to preserve the whole original state*)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   631
lemma project_preserves_id_I:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   632
     "G \<in> preserves f ==> project h C G \<in> preserves id"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   633
  by (simp add: project_preserves_I)
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   634
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   635
lemma extend_preserves:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   636
     "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   637
  by (auto simp add: preserves_def extend_stable [symmetric] 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   638
                   extend_set_eq_Collect)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   639
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   640
lemma inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   641
  by (auto simp add: preserves_def extend_def extend_act_def stable_def 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   642
                   constrains_def g_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   643
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   644
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 62343
diff changeset
   645
subsection\<open>Guarantees\<close>
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   646
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   647
lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   648
  apply (rule program_equalityI)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   649
  apply (auto simp add: project_set_extend_set_Int image_iff)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   650
  apply (metis Un_iff extend_act_inverse image_iff)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   651
  apply (metis Un_iff extend_act_inverse image_iff)
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   652
  done
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61952
diff changeset
   653
  
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   654
lemma extend_Join_eq_extend_D:
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   655
     "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   656
apply (drule_tac f = "project h UNIV" in arg_cong)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   657
apply (simp add: project_extend_Join)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   658
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   659
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   660
(** Strong precondition and postcondition; only useful when
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   661
    the old and new state sets are in bijection **)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   662
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   663
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   664
lemma ok_extend_imp_ok_project: "extend h F ok G ==> F ok project h UNIV G"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   665
apply (auto simp add: ok_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   666
apply (drule subsetD)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   667
apply (auto intro!: rev_image_eqI)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   668
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   669
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   670
lemma ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   671
apply (simp add: ok_def, safe)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   672
apply force+
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   673
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   674
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   675
lemma OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   676
apply (unfold OK_def, safe)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   677
apply (drule_tac x = i in bspec)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   678
apply (drule_tac [2] x = j in bspec)
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   679
apply force+
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   680
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   681
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   682
lemma guarantees_imp_extend_guarantees:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   683
     "F \<in> X guarantees Y ==>  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   684
      extend h F \<in> (extend h ` X) guarantees (extend h ` Y)"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   685
apply (rule guaranteesI, clarify)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   686
apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   687
                   guaranteesD)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   688
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   689
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   690
lemma extend_guarantees_imp_guarantees:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   691
     "extend h F \<in> (extend h ` X) guarantees (extend h ` Y)  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   692
      ==> F \<in> X guarantees Y"
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   693
apply (auto simp add: guar_def)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   694
apply (drule_tac x = "extend h G" in spec)
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   695
apply (simp del: extend_Join 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   696
            add: extend_Join [symmetric] ok_extend_iff 
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   697
                 inj_extend [THEN inj_image_mem_iff])
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   698
done
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   699
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   700
lemma extend_guarantees_eq:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   701
     "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   702
      (F \<in> X guarantees Y)"
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   703
  by (blast intro: guarantees_imp_extend_guarantees 
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 10834
diff changeset
   704
                 extend_guarantees_imp_guarantees)
6297
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
   705
5b9fbdfe22b7 new theory of extending the state space
paulson
parents:
diff changeset
   706
end
46912
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   707
e0cd5c4df8e6 tuned context specifications and proofs;
wenzelm
parents: 46577
diff changeset
   708
end