src/HOL/UNITY/Guar.thy
author nipkow
Fri, 27 Mar 2020 12:28:05 +0100
changeset 71593 71579bd59cd4
parent 69313 b021008c5397
child 80914 d97fdabd9e2b
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Guar.thy
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27682
diff changeset
     3
    Author:     Sidi Ehmety
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
     4
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
     5
From Chandy and Sanders, "Reasoning About Program Composition",
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
     6
Technical Report 2000-003, University of Florida, 2000.
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
     7
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27682
diff changeset
     8
Compatibility, weakest guarantees, etc.  and Weakest existential
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27682
diff changeset
     9
property, from Charpentier and Chandy "Theorems about Composition",
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    10
Fifth International Conference on Mathematics of Program, 2000.
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    11
*)
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    12
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
    13
section\<open>Guarantees Specifications\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13792
diff changeset
    14
27682
25aceefd4786 added class preorder
haftmann
parents: 16647
diff changeset
    15
theory Guar
25aceefd4786 added class preorder
haftmann
parents: 16647
diff changeset
    16
imports Comp
25aceefd4786 added class preorder
haftmann
parents: 16647
diff changeset
    17
begin
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    18
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 11190
diff changeset
    19
instance program :: (type) order
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 59807
diff changeset
    20
  by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    21
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
    22
text\<open>Existential and Universal properties.  I formalize the two-program
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
    23
      case, proving equivalence with Chandy and Sanders's n-ary definitions\<close>
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    24
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    25
definition ex_prop :: "'a program set => bool" where
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    26
   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    27
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    28
definition strict_ex_prop  :: "'a program set => bool" where
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    29
   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    30
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    31
definition uv_prop  :: "'a program set => bool" where
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    32
   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    33
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    34
definition strict_uv_prop  :: "'a program set => bool" where
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    35
   "strict_uv_prop X == 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    36
      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    37
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
    38
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
    39
text\<open>Guarantees properties\<close>
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
    40
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    41
definition guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) where
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    42
          (*higher than membership, lower than Co*)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    43
   "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    44
  
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    45
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    46
  (* Weakest guarantees *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    47
definition wg :: "['a program, 'a program set] => 'a program set" where
61952
546958347e05 prefer symbols for "Union", "Inter";
wenzelm
parents: 61169
diff changeset
    48
  "wg F Y == \<Union>({X. F \<in> X guarantees Y})"
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    49
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    50
   (* Weakest existential property stronger than X *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    51
definition wx :: "('a program) set => ('a program)set" where
61952
546958347e05 prefer symbols for "Union", "Inter";
wenzelm
parents: 61169
diff changeset
    52
   "wx X == \<Union>({Y. Y \<subseteq> X & ex_prop Y})"
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    53
  
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    54
  (*Ill-defined programs can arise through "Join"*)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    55
definition welldef :: "'a program set" where
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    56
  "welldef == {F. Init F \<noteq> {}}"
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    57
  
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    58
definition refines :: "['a program, 'a program, 'a program set] => bool"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    59
                        ("(3_ refines _ wrt _)" [10,10,10] 10) where
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    60
  "G refines F wrt X ==
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
    61
     \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
    62
         (G\<squnion>H \<in> welldef \<inter> X)"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    63
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    64
definition iso_refines :: "['a program, 'a program, 'a program set] => bool"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    65
                              ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where
11190
44e157622cb2 *** empty log message ***
ehmety
parents: 10064
diff changeset
    66
  "G iso_refines F wrt X ==
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    67
   F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
    68
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    69
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    70
lemma OK_insert_iff:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    71
     "(OK (insert i I) F) = 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    72
      (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    73
by (auto intro: ok_sym simp add: OK_iff_ok)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    74
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    75
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
    76
subsection\<open>Existential Properties\<close>
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
    77
45477
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    78
lemma ex1:
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    79
  assumes "ex_prop X" and "finite GG"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    80
  shows "GG \<inter> X \<noteq> {} \<Longrightarrow> OK GG (%G. G) \<Longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    81
  apply (atomize (full))
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    82
  using assms(2) apply induct
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    83
   using assms(1) apply (unfold ex_prop_def)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    84
   apply (auto simp add: OK_insert_iff Int_insert_left)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
    85
  done
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    86
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    87
lemma ex2: 
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    88
     "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} \<longrightarrow> OK GG (\<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X 
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    89
      \<Longrightarrow> ex_prop X"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    90
apply (unfold ex_prop_def, clarify)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    91
apply (drule_tac x = "{F,G}" in spec)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    92
apply (auto dest: ok_sym simp add: OK_iff_ok)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    93
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    94
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    95
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    96
(*Chandy & Sanders take this as a definition*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    97
lemma ex_prop_finite:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
    98
     "ex_prop X = 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    99
      (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   100
by (blast intro: ex1 ex2)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   101
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   102
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   103
(*Their "equivalent definition" given at the end of section 3*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   104
lemma ex_prop_equiv: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   105
     "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   106
apply auto
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   107
apply (unfold ex_prop_def component_of_def, safe, blast, blast) 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   108
apply (subst Join_commute) 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   109
apply (drule ok_sym, blast) 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   110
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   111
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   112
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   113
subsection\<open>Universal Properties\<close>
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   114
45477
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   115
lemma uv1:
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   116
  assumes "uv_prop X"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   117
    and "finite GG"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   118
    and "GG \<subseteq> X"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   119
    and "OK GG (%G. G)"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   120
  shows "(\<Squnion>G \<in> GG. G) \<in> X"
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   121
  using assms(2-)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   122
  apply induct
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   123
   using assms(1)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   124
   apply (unfold uv_prop_def)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   125
   apply (auto simp add: Int_insert_left OK_insert_iff)
11d9c2768729 tuned proofs;
wenzelm
parents: 44871
diff changeset
   126
  done
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   127
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   128
lemma uv2: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   129
     "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   130
      ==> uv_prop X"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   131
apply (unfold uv_prop_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   132
apply (rule conjI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   133
 apply (drule_tac x = "{}" in spec)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   134
 prefer 2
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   135
 apply clarify 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   136
 apply (drule_tac x = "{F,G}" in spec)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   137
apply (auto dest: ok_sym simp add: OK_iff_ok)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   138
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   139
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   140
(*Chandy & Sanders take this as a definition*)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   141
lemma uv_prop_finite:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   142
     "uv_prop X = 
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
   143
      (\<forall>GG. finite GG \<and> GG \<subseteq> X \<and> OK GG (\<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   144
by (blast intro: uv1 uv2)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   145
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   146
subsection\<open>Guarantees\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   147
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   148
lemma guaranteesI:
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   149
     "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   150
by (simp add: guar_def component_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   151
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   152
lemma guaranteesD: 
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   153
     "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   154
by (unfold guar_def component_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   155
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   156
(*This version of guaranteesD matches more easily in the conclusion
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   157
  The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   158
lemma component_guaranteesD: 
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   159
     "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |] ==> H \<in> Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   160
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   161
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   162
lemma guarantees_weaken: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   163
     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   164
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   165
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   166
lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   167
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   168
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   169
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   170
lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   171
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   172
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   173
(*Remark at end of section 4.1 *)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   174
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   175
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   176
apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   177
apply safe
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   178
 apply (drule_tac x = x in spec)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   179
 apply (drule_tac [2] x = x in spec)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   180
 apply (drule_tac [2] sym)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   181
apply (auto simp add: component_of_def)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   182
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   183
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   184
lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   185
by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   186
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   187
lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   188
apply (rule iffI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   189
apply (rule ex_prop_imp)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   190
apply (auto simp add: guarantees_imp) 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   191
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   192
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   193
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   194
subsection\<open>Distributive Laws.  Re-Orient to Perform Miniscoping\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   195
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   196
lemma guarantees_UN_left: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   197
     "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   198
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   199
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   200
lemma guarantees_Un_left: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   201
     "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   202
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   203
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   204
lemma guarantees_INT_right: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   205
     "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   206
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   207
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   208
lemma guarantees_Int_right: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   209
     "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   210
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   211
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   212
lemma guarantees_Int_right_I:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   213
     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   214
     ==> F \<in> Z guarantees (X \<inter> Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   215
by (simp add: guarantees_Int_right)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   216
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   217
lemma guarantees_INT_right_iff:
69313
b021008c5397 removed legacy input syntax
haftmann
parents: 67613
diff changeset
   218
     "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   219
by (simp add: guarantees_INT_right)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   220
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   221
lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   222
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   223
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   224
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   225
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   226
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   227
(** The following two can be expressed using intersection and subset, which
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   228
    is more faithful to the text but looks cryptic.
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   229
**)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   230
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   231
lemma combining1: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   232
    "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   233
     ==> F \<in> (V \<inter> Y) guarantees Z"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   234
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   235
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   236
lemma combining2: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   237
    "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   238
     ==> F \<in> V guarantees (X \<union> Z)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   239
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   240
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   241
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   242
    does not suit Isabelle... **)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   243
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   244
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   245
lemma all_guarantees: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   246
     "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   247
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   248
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   249
(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   250
lemma ex_guarantees: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   251
     "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   252
by (unfold guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   253
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   254
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   255
subsection\<open>Guarantees: Additional Laws (by lcp)\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   256
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   257
lemma guarantees_Join_Int: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   258
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   259
     ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   260
apply (simp add: guar_def, safe)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   261
 apply (simp add: Join_assoc)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   262
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   263
 apply (simp add: ok_commute)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   264
apply (simp add: Join_ac)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   265
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   266
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   267
lemma guarantees_Join_Un: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   268
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   269
     ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   270
apply (simp add: guar_def, safe)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   271
 apply (simp add: Join_assoc)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   272
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   273
 apply (simp add: ok_commute)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   274
apply (simp add: Join_ac)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   275
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   276
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   277
lemma guarantees_JN_INT: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   278
     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
69313
b021008c5397 removed legacy input syntax
haftmann
parents: 67613
diff changeset
   279
      ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   280
apply (unfold guar_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   281
apply (drule bspec, assumption)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   282
apply (rename_tac "i")
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   283
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   284
apply (auto intro: OK_imp_ok
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   285
            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   286
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   287
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   288
lemma guarantees_JN_UN: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   289
    "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
69313
b021008c5397 removed legacy input syntax
haftmann
parents: 67613
diff changeset
   290
     ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   291
apply (unfold guar_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   292
apply (drule bspec, assumption)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   293
apply (rename_tac "i")
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   294
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   295
apply (auto intro: OK_imp_ok
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   296
            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   297
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   298
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   299
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   300
subsection\<open>Guarantees Laws for Breaking Down the Program (by lcp)\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   301
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   302
lemma guarantees_Join_I1: 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   303
     "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   304
by (simp add: guar_def Join_assoc)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   305
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   306
lemma guarantees_Join_I2:         
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   307
     "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   308
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   309
apply (blast intro: guarantees_Join_I1)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   310
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   311
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   312
lemma guarantees_JN_I: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   313
     "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   314
      ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   315
apply (unfold guar_def, clarify)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   316
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
44871
fbfdc5ac86be misc tuning and clarification;
wenzelm
parents: 35416
diff changeset
   317
apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   318
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   319
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   320
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   321
(*** well-definedness ***)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   322
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   323
lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   324
by (unfold welldef_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   325
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   326
lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   327
by (unfold welldef_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   328
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   329
(*** refinement ***)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   330
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   331
lemma refines_refl: "F refines F wrt X"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   332
by (unfold refines_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   333
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   334
(*We'd like transitivity, but how do we get it?*)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   335
lemma refines_trans:
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   336
     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   337
apply (simp add: refines_def) 
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   338
oops
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   339
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   340
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   341
lemma strict_ex_refine_lemma: 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   342
     "strict_ex_prop X  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   343
      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   344
              = (F \<in> X --> G \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   345
by (unfold strict_ex_prop_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   346
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   347
lemma strict_ex_refine_lemma_v: 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   348
     "strict_ex_prop X  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   349
      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   350
          (F \<in> welldef \<inter> X --> G \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   351
apply (unfold strict_ex_prop_def, safe)
59807
22bc39064290 prefer local fixes;
wenzelm
parents: 58889
diff changeset
   352
apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   353
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   354
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   355
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   356
lemma ex_refinement_thm:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   357
     "[| strict_ex_prop X;   
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   358
         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]  
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   359
      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   360
apply (rule_tac x = SKIP in allE, assumption)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   361
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   362
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   363
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   364
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   365
lemma strict_uv_refine_lemma: 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   366
     "strict_uv_prop X ==> 
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   367
      (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   368
by (unfold strict_uv_prop_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   369
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   370
lemma strict_uv_refine_lemma_v: 
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   371
     "strict_uv_prop X  
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   372
      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   373
          (F \<in> welldef \<inter> X --> G \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   374
apply (unfold strict_uv_prop_def, safe)
59807
22bc39064290 prefer local fixes;
wenzelm
parents: 58889
diff changeset
   375
apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   376
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   377
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   378
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   379
lemma uv_refinement_thm:
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   380
     "[| strict_uv_prop X;   
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   381
         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> 
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   382
             G\<squnion>H \<in> welldef |]  
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   383
      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   384
apply (rule_tac x = SKIP in allE, assumption)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   385
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   386
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   387
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   388
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   389
lemma guarantees_equiv: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   390
    "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   391
by (unfold guar_def component_of_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   392
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   393
lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   394
by (unfold wg_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   395
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   396
lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   397
by (unfold wg_def guar_def, blast)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   398
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   399
lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   400
by (simp add: guarantees_equiv wg_def, blast)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   401
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   402
lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   403
by (simp add: wg_equiv)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   404
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   405
lemma wg_finite: 
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
   406
    "\<forall>FF. finite FF \<and> FF \<inter> X \<noteq> {} \<longrightarrow> OK FF (\<lambda>F. F)
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
   407
          \<longrightarrow> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F) \<in> wg F X) = ((\<Squnion>F \<in> FF. F) \<in> X))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   408
apply clarify
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   409
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   410
apply (drule_tac X = X in component_of_wg, simp)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   411
apply (simp add: component_of_def)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   412
apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   413
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   414
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   415
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   416
lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   417
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   418
apply blast
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   419
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   420
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   421
(** From Charpentier and Chandy "Theorems About Composition" **)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   422
(* Proposition 2 *)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   423
lemma wx_subset: "(wx X)<=X"
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   424
by (unfold wx_def, auto)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   425
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   426
lemma wx_ex_prop: "ex_prop (wx X)"
16647
c6d81ddebb0e Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
berghofe
parents: 16417
diff changeset
   427
apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   428
apply force 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   429
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   430
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   431
lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   432
by (auto simp add: wx_def)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   433
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   434
(* Proposition 6 *)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   435
lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   436
apply (unfold ex_prop_def, safe)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   437
 apply (drule_tac x = "G\<squnion>Ga" in spec)
44871
fbfdc5ac86be misc tuning and clarification;
wenzelm
parents: 35416
diff changeset
   438
 apply (force simp add: Join_assoc)
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   439
apply (drule_tac x = "F\<squnion>Ga" in spec)
44871
fbfdc5ac86be misc tuning and clarification;
wenzelm
parents: 35416
diff changeset
   440
apply (simp add: ok_commute  Join_ac) 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   441
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   442
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   443
text\<open>Equivalence with the other definition of wx\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   444
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   445
lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   446
apply (unfold wx_def, safe)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   447
 apply (simp add: ex_prop_def, blast) 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   448
apply (simp (no_asm))
13819
78f5885b76a9 minor revisions
paulson
parents: 13812
diff changeset
   449
apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   450
apply (rule_tac [2] wx'_ex_prop)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   451
apply (drule_tac x = SKIP in spec)+
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   452
apply auto 
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   453
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   454
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   455
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   456
text\<open>Propositions 7 to 11 are about this second definition of wx. 
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   457
   They are the same as the ones proved for the first definition of wx,
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
   458
 by equivalence\<close>
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   459
   
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   460
(* Proposition 12 *)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   461
(* Main result of the paper *)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   462
lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)"
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   463
by (simp add: guar_def wx_equiv)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   464
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   465
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   466
(* Rules given in section 7 of Chandy and Sander's
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   467
    Reasoning About Program composition paper *)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   468
lemma stable_guarantees_Always:
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   469
     "Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   470
apply (rule guaranteesI)
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   471
apply (simp add: Join_commute)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   472
apply (rule stable_Join_Always1)
44871
fbfdc5ac86be misc tuning and clarification;
wenzelm
parents: 35416
diff changeset
   473
 apply (simp_all add: invariant_def)
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   474
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   475
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   476
lemma constrains_guarantees_leadsTo:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   477
     "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   478
apply (rule guaranteesI)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   479
apply (rule leadsTo_Basis')
14112
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   480
 apply (drule constrains_weaken_R)
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   481
  prefer 2 apply assumption
95d51043d2a3 tidying
paulson
parents: 13819
diff changeset
   482
 apply blast
13792
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   483
apply (blast intro: Join_transient_I1)
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   484
done
d1811693899c converted more UNITY theories to new-style
paulson
parents: 12338
diff changeset
   485
7400
fbd5582761e6 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff changeset
   486
end