src/ZF/UNITY/Comp.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/Comp.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   1998  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
From Chandy and Sanders, "Reasoning About Program Composition",
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
Technical Report 2000-003, University of Florida, 2000.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     8
Revised by Sidi Ehmety on January  2001 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     9
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    10
Added: a strong form of the order relation over component and localize 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    11
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    12
Theory ported from HOL.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
  
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    14
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    15
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    16
header{*Composition*}
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    17
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14093
diff changeset
    18
theory Comp imports Union Increasing begin
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    19
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    20
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    21
  component :: "[i,i]=>o"  (infixl "component" 65)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    22
  "F component H == (\<exists>G. F Join G = H)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    23
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    24
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    25
  strict_component :: "[i,i]=>o" (infixl "strict'_component" 65)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    26
  "F strict_component H == F component H & F\<noteq>H"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    27
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    28
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    29
  (* A stronger form of the component relation *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    30
  component_of :: "[i,i]=>o"   (infixl "component'_of" 65)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    31
  "F component_of H  == (\<exists>G. F ok G & F Join G = H)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    32
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    33
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    34
  strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    35
  "F strict_component_of H  == F component_of H  & F\<noteq>H"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    36
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    37
definition
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    38
  (* Preserves a state function f, in particular a variable *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    39
  preserves :: "(i=>i)=>i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    40
  "preserves(f) == {F:program. \<forall>z. F: stable({s:state. f(s) = z})}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    41
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    42
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    43
  fun_pair :: "[i=>i, i =>i] =>(i=>i)"  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    44
  "fun_pair(f, g) == %x. <f(x), g(x)>"
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    45
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    46
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24327
diff changeset
    47
  localize  :: "[i=>i, i] => i"  where
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    48
  "localize(f,F) == mk_program(Init(F), Acts(F),
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    49
                       AllowedActs(F) \<inter> (\<Union>G\<in>preserves(f). Acts(G)))"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    50
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    51
  
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    52
(*** component and strict_component relations ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    53
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    54
lemma componentI: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    55
     "H component F | H component G ==> H component (F Join G)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    56
apply (unfold component_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    57
apply (rule_tac x = "Ga Join G" in exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    58
apply (rule_tac [2] x = "G Join F" in exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    59
apply (auto simp add: Join_ac)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    60
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    61
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    62
lemma component_eq_subset: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    63
     "G \<in> program ==> (F component G) \<longleftrightarrow>  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    64
   (Init(G) \<subseteq> Init(F) & Acts(F) \<subseteq> Acts(G) & AllowedActs(G) \<subseteq> AllowedActs(F))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    65
apply (unfold component_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    66
apply (rule exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    67
apply (rule program_equalityI, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    68
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    69
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    70
lemma component_SKIP [simp]: "F \<in> program ==> SKIP component F"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    71
apply (unfold component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    72
apply (rule_tac x = F in exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    73
apply (force intro: Join_SKIP_left)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    74
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    75
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    76
lemma component_refl [simp]: "F \<in> program ==> F component F"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    77
apply (unfold component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    78
apply (rule_tac x = F in exI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    79
apply (force intro: Join_SKIP_right)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    80
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    81
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    82
lemma SKIP_minimal: "F component SKIP ==> programify(F) = SKIP"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    83
apply (rule program_equalityI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    84
apply (simp_all add: component_eq_subset, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    85
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    86
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    87
lemma component_Join1: "F component (F Join G)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    88
by (unfold component_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    89
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    90
lemma component_Join2: "G component (F Join G)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    91
apply (unfold component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    92
apply (simp (no_asm) add: Join_commute)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    93
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    94
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    95
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    96
lemma Join_absorb1: "F component G ==> F Join G = G"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    97
by (auto simp add: component_def Join_left_absorb)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    98
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
    99
lemma Join_absorb2: "G component F ==> F Join G = F"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   100
by (auto simp add: Join_ac component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   101
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   102
lemma JN_component_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   103
     "H \<in> program==>(JOIN(I,F) component H) \<longleftrightarrow> (\<forall>i \<in> I. F(i) component H)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   104
apply (case_tac "I=0", force)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   105
apply (simp (no_asm_simp) add: component_eq_subset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   106
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   107
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   108
apply (rename_tac "y")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   109
apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   110
apply (blast elim!: not_emptyE)+
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   111
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   112
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   113
lemma component_JN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   114
apply (unfold component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   115
apply (blast intro: JN_absorb)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   116
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   117
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   118
lemma component_trans: "[| F component G; G component H |] ==> F component H"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   119
apply (unfold component_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   120
apply (blast intro: Join_assoc [symmetric])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   121
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   122
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   123
lemma component_antisym:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   124
     "[| F \<in> program; G \<in> program |] ==>(F component G & G  component F) \<longrightarrow> F = G"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   125
apply (simp (no_asm_simp) add: component_eq_subset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   126
apply clarify
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   127
apply (rule program_equalityI, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   128
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   129
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   130
lemma Join_component_iff:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   131
     "H \<in> program ==> 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   132
      ((F Join G) component H) \<longleftrightarrow> (F component H & G component H)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   133
apply (simp (no_asm_simp) add: component_eq_subset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   134
apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   135
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   136
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   137
lemma component_constrains:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   138
     "[| F component G; G \<in> A co B; F \<in> program |] ==> F \<in> A co B"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   139
apply (frule constrainsD2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   140
apply (auto simp add: constrains_def component_eq_subset)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   141
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   142
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   143
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   144
(*** preserves ***)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   145
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   146
lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   147
apply (unfold preserves_def safety_prop_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   148
apply (auto dest: ActsD simp add: stable_def constrains_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   149
apply (drule_tac c = act in subsetD, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   150
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   151
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   152
lemma preservesI [rule_format]: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   153
     "\<forall>z. F \<in> stable({s \<in> state. f(s) = z})  ==> F \<in> preserves(f)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   154
apply (auto simp add: preserves_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   155
apply (blast dest: stableD2)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   156
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   157
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   158
lemma preserves_imp_eq: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   159
     "[| F \<in> preserves(f);  act \<in> Acts(F);  <s,t> \<in> act |] ==> f(s) = f(t)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   160
apply (unfold preserves_def stable_def constrains_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   161
apply (subgoal_tac "s \<in> state & t \<in> state")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   162
 prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   163
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   164
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   165
lemma Join_preserves [iff]: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   166
"(F Join G \<in> preserves(v)) \<longleftrightarrow>   
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   167
      (programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   168
by (auto simp add: preserves_def INT_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   169
 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   170
lemma JN_preserves [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   171
     "(JOIN(I,F): preserves(v)) \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)):preserves(v))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   172
by (auto simp add: JN_stable preserves_def INT_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   173
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   174
lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   175
by (auto simp add: preserves_def INT_iff)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   176
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   177
lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   178
apply (unfold fun_pair_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   179
apply (simp (no_asm))
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   180
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   181
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   182
lemma preserves_fun_pair:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   183
     "preserves(fun_pair(v,w)) = preserves(v) \<inter> preserves(w)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   184
apply (rule equalityI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   185
apply (auto simp add: preserves_def stable_def constrains_def, blast+)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   186
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   187
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   188
lemma preserves_fun_pair_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   189
     "F \<in> preserves(fun_pair(v, w))  \<longleftrightarrow> F \<in> preserves(v) \<inter> preserves(w)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   190
by (simp add: preserves_fun_pair)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   191
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   192
lemma fun_pair_comp_distrib:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   193
     "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   194
by (simp add: fun_pair_def metacomp_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   195
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   196
lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   197
by (simp add: metacomp_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   198
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   199
lemma preserves_type: "preserves(v)<=program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   200
by (unfold preserves_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   201
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   202
lemma preserves_into_program [TC]: "F \<in> preserves(f) ==> F \<in> program"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   203
by (blast intro: preserves_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   204
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   205
lemma subset_preserves_comp: "preserves(f) \<subseteq> preserves(g comp f)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   206
apply (auto simp add: preserves_def stable_def constrains_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   207
apply (drule_tac x = "f (xb)" in spec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   208
apply (drule_tac x = act in bspec, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   209
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   210
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   211
lemma imp_preserves_comp: "F \<in> preserves(f) ==> F \<in> preserves(g comp f)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   212
by (blast intro: subset_preserves_comp [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   213
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   214
lemma preserves_subset_stable: "preserves(f) \<subseteq> stable({s \<in> state. P(f(s))})"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   215
apply (auto simp add: preserves_def stable_def constrains_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   216
apply (rename_tac s' s)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   217
apply (subgoal_tac "f (s) = f (s') ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   218
apply (force+)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   219
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   220
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   221
lemma preserves_imp_stable:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   222
     "F \<in> preserves(f) ==> F \<in> stable({s \<in> state. P(f(s))})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   223
by (blast intro: preserves_subset_stable [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   224
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   225
lemma preserves_imp_increasing: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   226
 "[| F \<in> preserves(f); \<forall>x \<in> state. f(x):A |] ==> F \<in> Increasing.increasing(A, r, f)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   227
apply (unfold Increasing.increasing_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   228
apply (auto intro: preserves_into_program)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   229
apply (rule_tac P = "%x. <k, x>:r" in preserves_imp_stable, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   230
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   231
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   232
lemma preserves_id_subset_stable: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   233
 "st_set(A) ==> preserves(%x. x) \<subseteq> stable(A)"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   234
apply (unfold preserves_def stable_def constrains_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   235
apply (drule_tac x = xb in spec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   236
apply (drule_tac x = act in bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   237
apply (auto dest: ActsD)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   238
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   239
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   240
lemma preserves_id_imp_stable:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   241
     "[| F \<in> preserves(%x. x); st_set(A) |] ==> F \<in> stable(A)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   242
by (blast intro: preserves_id_subset_stable [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   243
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   244
(** Added by Sidi **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   245
(** component_of **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   246
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   247
(*  component_of is stronger than component *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   248
lemma component_of_imp_component: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   249
"F component_of H ==> F component H"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   250
apply (unfold component_def component_of_def, blast)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   251
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   252
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   253
(* component_of satisfies many of component's properties *)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   254
lemma component_of_refl [simp]: "F \<in> program ==> F component_of F"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   255
apply (unfold component_of_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   256
apply (rule_tac x = SKIP in exI, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   257
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   258
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   259
lemma component_of_SKIP [simp]: "F \<in> program ==>SKIP component_of F"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   260
apply (unfold component_of_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   261
apply (rule_tac x = F in exI, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   262
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   263
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   264
lemma component_of_trans: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   265
     "[| F component_of G; G component_of H |] ==> F component_of H"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   266
apply (unfold component_of_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   267
apply (blast intro: Join_assoc [symmetric])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   268
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   269
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   270
(** localize **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   271
lemma localize_Init_eq [simp]: "Init(localize(v,F)) = Init(F)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   272
by (unfold localize_def, simp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   273
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   274
lemma localize_Acts_eq [simp]: "Acts(localize(v,F)) = Acts(F)"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   275
by (unfold localize_def, simp)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   276
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   277
lemma localize_AllowedActs_eq [simp]: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   278
 "AllowedActs(localize(v,F)) = AllowedActs(F) \<inter> (\<Union>G \<in> preserves(v). Acts(G))"
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   279
apply (unfold localize_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   280
apply (rule equalityI)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   281
apply (auto dest: Acts_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   282
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   283
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   284
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   285
(** Theorems used in ClientImpl **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   286
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   287
lemma stable_localTo_stable2: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   288
 "[| F \<in> stable({s \<in> state. P(f(s), g(s))});  G \<in> preserves(f);  G \<in> preserves(g) |]  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   289
      ==> F Join G \<in> stable({s \<in> state. P(f(s), g(s))})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   290
apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   291
apply (case_tac "act \<in> Acts (F) ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   292
apply auto
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   293
apply (drule preserves_imp_eq)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   294
apply (drule_tac [3] preserves_imp_eq, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   295
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   296
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   297
lemma Increasing_preserves_Stable:
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   298
     "[| F \<in> stable({s \<in> state. <f(s), g(s)>:r});  G \<in> preserves(f);    
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   299
         F Join G \<in> Increasing(A, r, g);  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   300
         \<forall>x \<in> state. f(x):A & g(x):A |]      
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   301
      ==> F Join G \<in> Stable({s \<in> state. <f(s), g(s)>:r})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   302
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   303
apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   304
apply (blast intro: constrains_weaken)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   305
(*The G case remains*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   306
apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   307
(*We have a G-action, so delete assumptions about F-actions*)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   308
apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   309
apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   310
apply (subgoal_tac "f (x) = f (xa) ")
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   311
apply (auto dest!: bspec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   312
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   313
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   314
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   315
(** Lemma used in AllocImpl **)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   316
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   317
lemma Constrains_UN_left: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   318
     "[| \<forall>x \<in> I. F \<in> A(x) Co B; F \<in> program |] ==> F:(\<Union>x \<in> I. A(x)) Co B"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   319
by (unfold Constrains_def constrains_def, auto)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   320
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   321
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   322
lemma stable_Join_Stable: 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   323
 "[| F \<in> stable({s \<in> state. P(f(s), g(s))});  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   324
     \<forall>k \<in> A. F Join G \<in> Stable({s \<in> state. P(k, g(s))});  
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   325
     G \<in> preserves(f); \<forall>s \<in> state. f(s):A|]
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   326
  ==> F Join G \<in> Stable({s \<in> state. P(f(s), g(s))})"
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   327
apply (unfold stable_def Stable_def preserves_def)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   328
apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   329
prefer 2 apply blast
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   330
apply (rule Constrains_UN_left, auto)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   331
apply (rule_tac A = "{s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))} \<inter> {s \<in> state. P (k, g (s))}" and A' = "({s \<in> state. f(s)=k} \<union> {s \<in> state. P (f (s), g (s))}) \<inter> {s \<in> state. P (k, g (s))}" in Constrains_weaken)
14093
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   332
 prefer 2 apply blast 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   333
 prefer 2 apply blast 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   334
apply (rule Constrains_Int)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   335
apply (rule constrains_imp_Constrains)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   336
apply (auto simp add: constrains_type [THEN subsetD])
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   337
apply (blast intro: constrains_weaken) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   338
apply (drule_tac x = k in spec)
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   339
apply (blast intro: constrains_weaken) 
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   340
done
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   341
24382760fd89 converting more theories to Isar scripts, and tidying
paulson
parents: 14046
diff changeset
   342
end