src/ZF/UNITY/Guar.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/Guar.thy
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
Guarantees, etc.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
From Chandy and Sanders, "Reasoning About Program Composition",
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     8
Technical Report 2000-003, University of Florida, 2000.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     9
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    10
Revised by Sidi Ehmety on January 2001
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    11
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    12
Added \<in> Compatibility, weakest guarantees, etc.
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    14
and Weakest existential property,
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    15
from Charpentier and Chandy "Theorems about Composition",
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    16
Fifth International Conference on Mathematics of Program, 2000.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    17
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    18
Theory ported from HOL.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    19
*)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    20
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    21
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    22
header{*The Chandy-Sanders Guarantees Operator*}
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    23
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14093
diff changeset
    24
theory Guar imports Comp begin 
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    25
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    26
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    27
(* To be moved to theory WFair???? *)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    28
lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |] ==> F \<in> A leadsTo B"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    29
apply (frule constrainsD2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    30
apply (drule_tac B = "A-B" in constrains_weaken_L, blast) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    31
apply (drule_tac B = "A-B" in transient_strengthen, blast) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    32
apply (blast intro: ensuresI [THEN leadsTo_Basis])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    33
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    34
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    35
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    36
  (*Existential and Universal properties.  We formalize the two-program
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    37
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    38
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    39
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    40
   ex_prop :: "i => o"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    41
   "ex_prop(X) == X<=program &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    42
    (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F Join G) \<in> X)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    43
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    44
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    45
  strict_ex_prop  :: "i => o"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    46
  "strict_ex_prop(X) == X<=program &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    47
   (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F Join G \<in> X))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    48
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    49
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    50
  uv_prop  :: "i => o"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    51
   "uv_prop(X) == X<=program &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    52
    (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F Join G) \<in> X))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    53
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    54
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    55
 strict_uv_prop  :: "i => o"  where
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    56
   "strict_uv_prop(X) == X<=program &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    57
    (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F Join G \<in> X)))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    58
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    59
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    60
  guar :: "[i, i] => i" (infixl "guarantees" 55)  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    61
              (*higher than membership, lower than Co*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    62
  "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X \<longrightarrow> F Join G \<in> Y}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    63
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    64
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    65
  (* Weakest guarantees *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    66
   wg :: "[i,i] => i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    67
  "wg(F,Y) == \<Union>({X \<in> Pow(program). F:(X guarantees Y)})"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    68
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    69
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    70
  (* Weakest existential property stronger than X *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    71
   wx :: "i =>i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    72
   "wx(X) == \<Union>({Y \<in> Pow(program). Y<=X & ex_prop(Y)})"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    73
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    74
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    75
  (*Ill-defined programs can arise through "Join"*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    76
  welldef :: i  where
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    77
  "welldef == {F \<in> program. Init(F) \<noteq> 0}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    78
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    79
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    80
  refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10)  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    81
  "G refines F wrt X ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    82
   \<forall>H \<in> program. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    83
    \<longrightarrow> (G Join H \<in> welldef \<inter> X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    84
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    85
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    86
  iso_refines :: "[i,i, i] => o"  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    87
  "G iso_refines F wrt X ==  F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    88
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    89
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    90
(*** existential properties ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    91
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    92
lemma ex_imp_subset_program: "ex_prop(X) ==> X\<subseteq>program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    93
by (simp add: ex_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    94
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    95
lemma ex1 [rule_format]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    96
 "GG \<in> Fin(program) 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    97
  ==> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (%G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    98
apply (unfold ex_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
    99
apply (erule Fin_induct)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   100
apply (simp_all add: OK_cons_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   101
apply (safe elim!: not_emptyE, auto) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   102
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   103
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   104
lemma ex2 [rule_format]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   105
"X \<subseteq> program ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   106
 (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X) 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   107
   \<longrightarrow> ex_prop(X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   108
apply (unfold ex_prop_def, clarify)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   109
apply (drule_tac x = "{F,G}" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   110
apply (simp_all add: OK_iff_ok)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   111
apply (auto intro: ok_sym)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   112
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   113
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   114
(*Chandy & Sanders take this as a definition*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   115
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   116
lemma ex_prop_finite:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   117
     "ex_prop(X) \<longleftrightarrow> (X\<subseteq>program &  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   118
  (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 & OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   119
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   120
apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   121
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   122
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   123
(* Equivalent definition of ex_prop given at the end of section 3*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   124
lemma ex_prop_equiv: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   125
"ex_prop(X) \<longleftrightarrow>  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   126
  X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X \<longleftrightarrow> (\<forall>H \<in> program. (G component_of H) \<longrightarrow> H \<in> X)))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   127
apply (unfold ex_prop_def component_of_def, safe, force, force, blast) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   128
apply (subst Join_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   129
apply (blast intro: ok_sym) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   130
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   131
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   132
(*** universal properties ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   133
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   134
lemma uv_imp_subset_program: "uv_prop(X)==> X\<subseteq>program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   135
apply (unfold uv_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   136
apply (simp (no_asm_simp))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   137
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   138
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   139
lemma uv1 [rule_format]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   140
     "GG \<in> Fin(program) ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   141
      (uv_prop(X)\<longrightarrow> GG \<subseteq> X & OK(GG, (%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   142
apply (unfold uv_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   143
apply (erule Fin_induct)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   144
apply (auto simp add: OK_cons_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   145
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   146
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   147
lemma uv2 [rule_format]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   148
     "X\<subseteq>program  ==> 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   149
      (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   150
      \<longrightarrow> uv_prop(X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   151
apply (unfold uv_prop_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   152
apply (drule_tac x = 0 in bspec, simp+) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   153
apply (drule_tac x = "{F,G}" in bspec, simp) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   154
apply (force dest: ok_sym simp add: OK_iff_ok) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   155
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   156
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   157
(*Chandy & Sanders take this as a definition*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   158
lemma uv_prop_finite: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   159
"uv_prop(X) \<longleftrightarrow> X\<subseteq>program &  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   160
  (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in>  X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   161
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   162
apply (blast dest: uv_imp_subset_program)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   163
apply (blast intro: uv1)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   164
apply (blast intro!: uv2 dest:)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   165
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   166
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   167
(*** guarantees ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   168
lemma guaranteesI: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   169
     "[| (!!G. [| F ok G; F Join G \<in> X; G \<in> program |] ==> F Join G \<in> Y); 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   170
         F \<in> program |]   
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   171
    ==> F \<in> X guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   172
by (simp add: guar_def component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   173
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   174
lemma guaranteesD: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   175
     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X; G \<in> program |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   176
      ==> F Join G \<in> Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   177
by (simp add: guar_def component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   178
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   179
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   180
(*This version of guaranteesD matches more easily in the conclusion
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   181
  The major premise can no longer be  F\<subseteq>H since we need to reason about G*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   182
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   183
lemma component_guaranteesD: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   184
     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G; G \<in> program |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   185
      ==> H \<in> Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   186
by (simp add: guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   187
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   188
lemma guarantees_weaken: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   189
     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   190
by (simp add: guar_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   191
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   192
lemma subset_imp_guarantees_program:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   193
     "X \<subseteq> Y ==> X guarantees Y = program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   194
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   195
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   196
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   197
lemma subset_imp_guarantees:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   198
     "[| X \<subseteq> Y; F \<in> program |] ==> F \<in> X guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   199
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   200
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   201
lemma component_of_Join1: "F ok G ==> F component_of (F Join G)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   202
by (unfold component_of_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   203
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   204
lemma component_of_Join2: "F ok G ==> G component_of (F Join G)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   205
apply (subst Join_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   206
apply (blast intro: ok_sym component_of_Join1)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   207
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   208
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   209
(*Remark at end of section 4.1 *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   210
lemma ex_prop_imp: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   211
     "ex_prop(Y) ==> (Y = (program guarantees Y))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   212
apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   213
apply clarify
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   214
apply (rule equalityI, blast, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   215
apply (drule_tac x = x in bspec, assumption, force) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   216
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   217
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   218
lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   219
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   220
apply (simp (no_asm_simp) add: ex_prop_equiv)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   221
apply safe
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   222
apply (blast intro: elim: equalityE) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   223
apply (simp_all (no_asm_use) add: component_of_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   224
apply (force elim: equalityE)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   225
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   226
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   227
lemma ex_prop_equiv2: "(ex_prop(Y)) \<longleftrightarrow> (Y = program guarantees Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   228
by (blast intro: ex_prop_imp guarantees_imp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   229
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   230
(** Distributive laws.  Re-orient to perform miniscoping **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   231
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   232
lemma guarantees_UN_left: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   233
     "i \<in> I ==>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   234
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   235
apply (rule equalityI, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   236
 prefer 2 apply force
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   237
apply blast+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   238
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   239
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   240
lemma guarantees_Un_left: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   241
     "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   242
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   243
apply (rule equalityI, safe, blast+)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   244
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   245
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   246
lemma guarantees_INT_right: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   247
     "i \<in> I ==> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   248
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   249
apply (rule equalityI, safe, blast+)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   250
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   251
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   252
lemma guarantees_Int_right: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   253
     "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   254
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   255
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   256
lemma guarantees_Int_right_I:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   257
     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   258
     ==> F \<in> Z guarantees (X \<inter> Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   259
by (simp (no_asm_simp) add: guarantees_Int_right)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   260
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   261
lemma guarantees_INT_right_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   262
     "i \<in> I==> (F \<in> X guarantees (\<Inter>i \<in> I. Y(i))) \<longleftrightarrow>  
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   263
      (\<forall>i \<in> I. F \<in> X guarantees Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   264
by (simp add: guarantees_INT_right INT_iff, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   265
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   266
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   267
lemma shunting: "(X guarantees Y) = (program guarantees ((program-X) \<union> Y))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   268
by (unfold guar_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   269
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   270
lemma contrapositive:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   271
     "(X guarantees Y) = (program - Y) guarantees (program -X)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   272
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   273
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   274
(** The following two can be expressed using intersection and subset, which
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   275
    is more faithful to the text but looks cryptic.
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   276
**)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   277
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   278
lemma combining1: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   279
    "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   280
     ==> F \<in> (V \<inter> Y) guarantees Z"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   281
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   282
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   283
lemma combining2: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   284
    "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   285
     ==> F \<in> V guarantees (X \<union> Z)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   286
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   287
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   288
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   289
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   290
    does not suit Isabelle... **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   291
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   292
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   293
lemma all_guarantees: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   294
     "[| \<forall>i \<in> I. F \<in> X guarantees Y(i); i \<in> I |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   295
    ==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   296
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   297
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   298
(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   299
lemma ex_guarantees: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   300
     "\<exists>i \<in> I. F \<in> X guarantees Y(i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   301
by (unfold guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   302
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   303
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   304
(*** Additional guarantees laws, by lcp ***)
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   305
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   306
lemma guarantees_Join_Int: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   307
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   308
     ==> F Join G: (U \<inter> X) guarantees (V \<inter> Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   309
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   310
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   311
apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   312
apply safe
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   313
apply (simp add: Join_assoc)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   314
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   315
apply (simp add: ok_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   316
apply (simp (no_asm_simp) add: Join_ac)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   317
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   318
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   319
lemma guarantees_Join_Un: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   320
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   321
     ==> F Join G: (U \<union> X) guarantees (V \<union> Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   322
apply (unfold guar_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   323
apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   324
apply safe
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   325
apply (simp add: Join_assoc)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   326
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   327
apply (rotate_tac 4)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   328
apply (drule_tac x = "F Join Ga" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   329
apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   330
apply (force simp add: ok_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   331
apply (simp (no_asm_simp) add: Join_ac)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   332
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   333
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   334
lemma guarantees_JN_INT: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   335
     "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i);  OK(I,F); i \<in> I |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   336
      ==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   337
apply (unfold guar_def, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   338
 prefer 2 apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   339
apply (drule_tac x = xa in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   340
apply (simp_all add: INT_iff, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   341
apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) Join G" and A=program in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   342
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   343
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   344
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   345
lemma guarantees_JN_UN: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   346
    "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i);  OK(I,F) |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   347
     ==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   348
apply (unfold guar_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   349
apply (drule_tac x = y in bspec, simp_all, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   350
apply (rename_tac G y)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   351
apply (drule_tac x = "JOIN (I-{y}, F) Join G" and A=program in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   352
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   353
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   354
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   355
(*** guarantees laws for breaking down the program, by lcp ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   356
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   357
lemma guarantees_Join_I1: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   358
     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   359
apply (simp add: guar_def, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   360
apply (simp add: Join_assoc)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   361
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   362
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   363
lemma guarantees_Join_I2:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   364
     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   365
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   366
apply (blast intro: guarantees_Join_I1)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   367
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   368
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   369
lemma guarantees_JN_I: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   370
     "[| i \<in> I; F(i) \<in>  X guarantees Y;  OK(I,F) |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   371
      ==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   372
apply (unfold guar_def, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   373
apply (drule_tac x = "JOIN (I-{i},F) Join G" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   374
apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   375
apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   376
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   377
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   378
(*** well-definedness ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   379
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   380
lemma Join_welldef_D1: "F Join G \<in> welldef ==> programify(F) \<in>  welldef"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   381
by (unfold welldef_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   382
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   383
lemma Join_welldef_D2: "F Join G \<in> welldef ==> programify(G) \<in>  welldef"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   384
by (unfold welldef_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   385
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   386
(*** refinement ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   387
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   388
lemma refines_refl: "F refines F wrt X"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   389
by (unfold refines_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   390
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   391
(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   392
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   393
lemma wg_type: "wg(F, X) \<subseteq> program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   394
by (unfold wg_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   395
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   396
lemma guarantees_type: "X guarantees Y \<subseteq> program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   397
by (unfold guar_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   398
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   399
lemma wgD2: "G \<in> wg(F, X) ==> G \<in> program & F \<in> program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   400
apply (unfold wg_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   401
apply (blast dest: guarantees_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   402
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   403
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   404
lemma guarantees_equiv: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   405
"(F \<in> X guarantees Y) \<longleftrightarrow>  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   406
   F \<in> program & (\<forall>H \<in> program. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   407
by (unfold guar_def component_of_def, force) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   408
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   409
lemma wg_weakest:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   410
     "!!X. [| F \<in> (X guarantees Y); X \<subseteq> program |] ==> X \<subseteq> wg(F,Y)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   411
by (unfold wg_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   412
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   413
lemma wg_guarantees: "F \<in> program ==> F \<in> wg(F,Y) guarantees Y"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   414
by (unfold wg_def guar_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   415
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   416
lemma wg_equiv:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   417
     "H \<in> wg(F,X) \<longleftrightarrow> 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   418
      ((F component_of H \<longrightarrow> H \<in> X) & F \<in> program & H \<in> program)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   419
apply (simp add: wg_def guarantees_equiv)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   420
apply (rule iffI, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   421
apply (rule_tac [4] x = "{H}" in bexI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   422
apply (rule_tac [3] x = "{H}" in bexI, blast+)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   423
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   424
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   425
lemma component_of_wg: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   426
    "F component_of H ==> H \<in> wg(F,X) \<longleftrightarrow> (H \<in> X & F \<in> program & H \<in> program)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   427
by (simp (no_asm_simp) add: wg_equiv)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   428
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   429
lemma wg_finite [rule_format]: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   430
"\<forall>FF \<in> Fin(program). FF \<inter> X \<noteq> 0 \<longrightarrow> OK(FF, %F. F)  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   431
   \<longrightarrow> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in>  wg(F,X)) \<longleftrightarrow> ((\<Squnion>F \<in> FF. F) \<in> X))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   432
apply clarify
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   433
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   434
apply (drule_tac X = X in component_of_wg)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   435
apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   436
apply (simp_all add: component_of_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   437
apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   438
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   439
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   440
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   441
lemma wg_ex_prop:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   442
     "ex_prop(X) ==> (F \<in> X) \<longleftrightarrow> (\<forall>H \<in> program. H \<in> wg(F,X) & F \<in> program)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   443
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   444
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   445
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   446
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   447
(** From Charpentier and Chandy "Theorems About Composition" **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   448
(* Proposition 2 *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   449
lemma wx_subset: "wx(X)\<subseteq>X"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   450
by (unfold wx_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   451
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   452
lemma wx_ex_prop: "ex_prop(wx(X))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   453
apply (simp (no_asm_use) add: ex_prop_def wx_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   454
apply safe
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   455
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   456
apply (rule_tac x=x in bexI, force, simp)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   457
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   458
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   459
lemma wx_weakest: "\<forall>Z. Z\<subseteq>program \<longrightarrow> Z\<subseteq> X \<longrightarrow> ex_prop(Z) \<longrightarrow> Z \<subseteq> wx(X)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   460
by (unfold wx_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   461
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   462
(* Proposition 6 *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   463
lemma wx'_ex_prop: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   464
 "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X})"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   465
apply (unfold ex_prop_def, safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   466
 apply (drule_tac x = "G Join Ga" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   467
  apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   468
 apply (force simp add: Join_assoc)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   469
apply (drule_tac x = "F Join Ga" in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   470
 apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   471
apply (simp (no_asm_use))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   472
apply safe
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   473
 apply (simp (no_asm_simp) add: ok_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   474
apply (subgoal_tac "F Join G = G Join F")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   475
 apply (simp (no_asm_simp) add: Join_assoc)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   476
apply (simp (no_asm) add: Join_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   477
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   478
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   479
(* Equivalence with the other definition of wx *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   480
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   481
lemma wx_equiv: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   482
     "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F Join G) \<in> X}"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   483
apply (unfold wx_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   484
apply (rule equalityI, safe, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   485
 apply (simp (no_asm_use) add: ex_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   486
apply blast 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   487
apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X}" 
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   488
         in UnionI, 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   489
       safe)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   490
apply (rule_tac [2] wx'_ex_prop)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   491
apply (drule_tac x=SKIP in bspec, simp)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   492
apply auto 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   493
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   494
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   495
(* Propositions 7 to 11 are all about this second definition of wx. And
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   496
   by equivalence between the two definition, they are the same as the ones proved *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   497
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   498
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   499
(* Proposition 12 *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   500
(* Main result of the paper *)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   501
lemma guarantees_wx_eq: "(X guarantees Y) = wx((program-X) \<union> Y)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   502
by (auto simp add: guar_def wx_equiv)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   503
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   504
(* 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   505
{* Corollary, but this result has already been proved elsewhere *}
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   506
 "ex_prop(X guarantees Y)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   507
*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   508
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   509
(* Rules given in section 7 of Chandy and Sander's
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   510
    Reasoning About Program composition paper *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   511
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   512
lemma stable_guarantees_Always:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   513
     "[| Init(F) \<subseteq> A; F \<in> program |] ==> F \<in> stable(A) guarantees Always(A)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   514
apply (rule guaranteesI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   515
 prefer 2 apply assumption
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   516
apply (simp (no_asm) add: Join_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   517
apply (rule stable_Join_Always1)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   518
apply (simp_all add: invariant_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   519
apply (auto simp add: programify_def initially_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   520
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   521
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   522
lemma constrains_guarantees_leadsTo:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   523
     "[| F \<in> transient(A); st_set(B) |] 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   524
      ==> F: (A co A \<union> B) guarantees (A leadsTo (B-A))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   525
apply (rule guaranteesI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   526
 prefer 2 apply (blast dest: transient_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   527
apply (rule leadsTo_Basis')
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   528
  apply (blast intro: constrains_weaken_R) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   529
 apply (blast intro!: Join_transient_I1, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 12195
diff changeset
   530
done
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   531
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   532
end