src/ZF/UNITY/WFair.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
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:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 32960
diff changeset
     1
(*  Title:      ZF/UNITY/WFair.thy
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi 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
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
     6
header{*Progress under Weak Fairness*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
     7
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
     8
theory WFair
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
     9
imports UNITY Main_ZFC
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    10
begin
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    11
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    12
text{*This theory defines the operators transient, ensures and leadsTo,
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    13
assuming weak fairness. From Misra, "A Logic for Concurrent Programming",
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    14
1994.*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    15
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    16
definition
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    17
  (* This definition specifies weak fairness.  The rest of the theory
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    18
    is generic to all forms of fairness.*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    19
  transient :: "i=>i"  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    20
  "transient(A) =={F \<in> program. (\<exists>act\<in>Acts(F). A<=domain(act) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    21
                               act``A \<subseteq> state-A) & st_set(A)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    22
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    23
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    24
  ensures :: "[i,i] => i"       (infixl "ensures" 60)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    25
  "A ensures B == ((A-B) co (A \<union> B)) \<inter> transient(A-B)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    26
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    27
consts
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    28
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    29
  (*LEADS-TO constant for the inductive definition*)
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    30
  leads :: "[i, i]=>i"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    31
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    32
inductive
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    33
  domains
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    34
     "leads(D, F)" \<subseteq> "Pow(D)*Pow(D)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    35
  intros
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    36
    Basis:  "[| F \<in> A ensures B;  A \<in> Pow(D); B \<in> Pow(D) |] ==> <A,B>:leads(D, F)"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    37
    Trans:  "[| <A,B> \<in> leads(D, F); <B,C> \<in> leads(D, F) |] ==>  <A,C>:leads(D, F)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    38
    Union:   "[| S \<in> Pow({A \<in> S. <A, B>:leads(D, F)}); B \<in> Pow(D); S \<in> Pow(Pow(D)) |] ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    39
              <\<Union>(S),B>:leads(D, F)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    40
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    41
  monos        Pow_mono
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    42
  type_intros  Union_Pow_iff [THEN iffD2] UnionI PowI
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    43
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    44
definition
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    45
  (* The Visible version of the LEADS-TO relation*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    46
  leadsTo :: "[i, i] => i"       (infixl "leadsTo" 60)  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    47
  "A leadsTo B == {F \<in> program. <A,B>:leads(state, F)}"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    48
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    49
definition
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    50
  (* wlt(F, B) is the largest set that leads to B*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    51
  wlt :: "[i, i] => i"  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    52
    "wlt(F, B) == \<Union>({A \<in> Pow(state). F \<in> A leadsTo B})"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    53
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    54
notation (xsymbols)
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 15634
diff changeset
    55
  leadsTo  (infixl "\<longmapsto>" 60)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    56
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    57
(** Ad-hoc set-theory rules **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    58
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    59
lemma Int_Union_Union: "\<Union>(B) \<inter> A = (\<Union>b \<in> B. b \<inter> A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    60
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    61
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    62
lemma Int_Union_Union2: "A \<inter> \<Union>(B) = (\<Union>b \<in> B. A \<inter> b)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    63
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    64
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    65
(*** transient ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    66
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    67
lemma transient_type: "transient(A)<=program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    68
by (unfold transient_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    69
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    70
lemma transientD2:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    71
"F \<in> transient(A) ==> F \<in> program & st_set(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    72
apply (unfold transient_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    73
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    74
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    75
lemma stable_transient_empty: "[| F \<in> stable(A); F \<in> transient(A) |] ==> A = 0"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    76
by (simp add: stable_def constrains_def transient_def, fast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    77
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    78
lemma transient_strengthen: "[|F \<in> transient(A); B<=A|] ==> F \<in> transient(B)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    79
apply (simp add: transient_def st_set_def, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    80
apply (blast intro!: rev_bexI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    81
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    82
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    83
lemma transientI:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    84
"[|act \<in> Acts(F); A \<subseteq> domain(act); act``A \<subseteq> state-A;
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    85
    F \<in> program; st_set(A)|] ==> F \<in> transient(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    86
by (simp add: transient_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    87
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    88
lemma transientE:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    89
     "[| F \<in> transient(A);
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    90
         !!act. [| act \<in> Acts(F);  A \<subseteq> domain(act); act``A \<subseteq> state-A|]==>P|]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    91
      ==>P"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    92
by (simp add: transient_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    93
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    94
lemma transient_state: "transient(state) = 0"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    95
apply (simp add: transient_def)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    96
apply (rule equalityI, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    97
apply (cut_tac F = x in Acts_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    98
apply (simp add: Diff_cancel)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
    99
apply (auto intro: st0_in_state)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   100
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   101
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   102
lemma transient_state2: "state<=B ==> transient(B) = 0"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   103
apply (simp add: transient_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   104
apply (rule equalityI, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   105
apply (cut_tac F = x in Acts_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   106
apply (subgoal_tac "B=state")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   107
apply (auto intro: st0_in_state)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   108
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   109
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   110
lemma transient_empty: "transient(0) = program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   111
by (auto simp add: transient_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   112
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   113
declare transient_empty [simp] transient_state [simp] transient_state2 [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   114
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   115
(*** ensures ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   116
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   117
lemma ensures_type: "A ensures B <=program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   118
by (simp add: ensures_def constrains_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   119
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   120
lemma ensuresI:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   121
"[|F:(A-B) co (A \<union> B); F \<in> transient(A-B)|]==>F \<in> A ensures B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   122
apply (unfold ensures_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   123
apply (auto simp add: transient_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   124
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   125
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   126
(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   127
lemma ensuresI2: "[| F \<in> A co A \<union> B; F \<in> transient(A) |] ==> F \<in> A ensures B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   128
apply (drule_tac B = "A-B" in constrains_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   129
apply (drule_tac [2] B = "A-B" in transient_strengthen)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   130
apply (auto simp add: ensures_def transient_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   131
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   132
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   133
lemma ensuresD: "F \<in> A ensures B ==> F:(A-B) co (A \<union> B) & F \<in> transient (A-B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   134
by (unfold ensures_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   135
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   136
lemma ensures_weaken_R: "[|F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   137
apply (unfold ensures_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   138
apply (blast intro: transient_strengthen constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   139
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   140
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   141
(*The L-version (precondition strengthening) fails, but we have this*)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   142
lemma stable_ensures_Int:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   143
     "[| F \<in> stable(C);  F \<in> A ensures B |] ==> F:(C \<inter> A) ensures (C \<inter> B)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   144
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   145
apply (unfold ensures_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   146
apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   147
apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   148
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   149
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   150
lemma stable_transient_ensures: "[|F \<in> stable(A);  F \<in> transient(C); A<=B \<union> C|] ==> F \<in> A ensures B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   151
apply (frule stable_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   152
apply (simp add: ensures_def stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   153
apply (blast intro: transient_strengthen constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   154
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   155
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   156
lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   157
by (auto simp add: ensures_def unless_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   158
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   159
lemma subset_imp_ensures: "[| F \<in> program; A<=B  |] ==> F \<in> A ensures B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   160
by (auto simp add: ensures_def constrains_def transient_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   161
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   162
(*** leadsTo ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   163
lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   164
lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   165
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   166
lemma leadsTo_type: "A leadsTo B \<subseteq> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   167
by (unfold leadsTo_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   168
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   169
lemma leadsToD2:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   170
"F \<in> A leadsTo B ==> F \<in> program & st_set(A) & st_set(B)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   171
apply (unfold leadsTo_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   172
apply (blast dest: leads_left leads_right)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   173
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   174
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   175
lemma leadsTo_Basis:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   176
    "[|F \<in> A ensures B; st_set(A); st_set(B)|] ==> F \<in> A leadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   177
apply (unfold leadsTo_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   178
apply (cut_tac ensures_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   179
apply (auto intro: leads.Basis)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   180
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   181
declare leadsTo_Basis [intro]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   182
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   183
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   184
(* [| F \<in> program; A<=B;  st_set(A); st_set(B) |] ==> A leadsTo B *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 37936
diff changeset
   185
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   186
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   187
lemma leadsTo_Trans: "[|F \<in> A leadsTo B;  F \<in> B leadsTo C |]==>F \<in> A leadsTo C"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   188
apply (unfold leadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   189
apply (auto intro: leads.Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   190
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   191
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   192
(* Better when used in association with leadsTo_weaken_R *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   193
lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A leadsTo (state-A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   194
apply (unfold transient_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   195
apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   196
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   197
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   198
(*Useful with cancellation, disjunction*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   199
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   200
by simp
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   201
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   202
lemma leadsTo_Un_duplicate2:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   203
     "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   204
by (simp add: Un_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   205
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   206
(*The Union introduction rule as we should have liked to state it*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   207
lemma leadsTo_Union:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   208
    "[|!!A. A \<in> S ==> F \<in> A leadsTo B; F \<in> program; st_set(B)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   209
     ==> F \<in> \<Union>(S) leadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   210
apply (unfold leadsTo_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   211
apply (blast intro: leads.Union dest: leads_left)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   212
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   213
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   214
lemma leadsTo_Union_Int:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   215
    "[|!!A. A \<in> S ==>F \<in> (A \<inter> C) leadsTo B; F \<in> program; st_set(B)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   216
     ==> F \<in> (\<Union>(S)Int C)leadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   217
apply (unfold leadsTo_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   218
apply (simp only: Int_Union_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   219
apply (blast dest: leads_left intro: leads.Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   220
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   221
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   222
lemma leadsTo_UN:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   223
    "[| !!i. i \<in> I ==> F \<in> A(i) leadsTo B; F \<in> program; st_set(B)|]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   224
     ==> F:(\<Union>i \<in> I. A(i)) leadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   225
apply (simp add: Int_Union_Union leadsTo_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   226
apply (blast dest: leads_left intro: leads.Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   227
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   228
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   229
(* Binary union introduction rule *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   230
lemma leadsTo_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   231
     "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   232
apply (subst Un_eq_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   233
apply (blast intro: leadsTo_Union dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   234
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   235
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   236
lemma single_leadsTo_I:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   237
    "[|!!x. x \<in> A==> F:{x} leadsTo B; F \<in> program; st_set(B) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   238
     ==> F \<in> A leadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   239
apply (rule_tac b = A in UN_singleton [THEN subst])
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   240
apply (rule leadsTo_UN, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   241
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   242
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   243
lemma leadsTo_refl: "[| F \<in> program; st_set(A) |] ==> F \<in> A leadsTo A"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   244
by (blast intro: subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   245
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   246
lemma leadsTo_refl_iff: "F \<in> A leadsTo A \<longleftrightarrow> F \<in> program & st_set(A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   247
by (auto intro: leadsTo_refl dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   248
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   249
lemma empty_leadsTo: "F \<in> 0 leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   250
by (auto intro: subset_imp_leadsTo dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   251
declare empty_leadsTo [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   252
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   253
lemma leadsTo_state: "F \<in> A leadsTo state \<longleftrightarrow> (F \<in> program & st_set(A))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   254
by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   255
declare leadsTo_state [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   256
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   257
lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \<in> A leadsTo B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   258
by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   259
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   260
lemma leadsTo_weaken_L: "[| F \<in> A leadsTo A'; B<=A |] ==> F \<in> B leadsTo A'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   261
apply (frule leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   262
apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   263
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   264
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   265
lemma leadsTo_weaken: "[| F \<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \<in> B leadsTo B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   266
apply (frule leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   267
apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   268
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   269
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   270
(* This rule has a nicer conclusion *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   271
lemma transient_imp_leadsTo2: "[| F \<in> transient(A); state-A<=B; st_set(B)|] ==> F \<in> A leadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   272
apply (frule transientD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   273
apply (rule leadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   274
apply (auto simp add: transient_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   275
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   276
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   277
(*Distributes over binary unions*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   278
lemma leadsTo_Un_distrib: "F:(A \<union> B) leadsTo C  \<longleftrightarrow>  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   279
by (blast intro: leadsTo_Un leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   280
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   281
lemma leadsTo_UN_distrib:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   282
"(F:(\<Union>i \<in> I. A(i)) leadsTo B)\<longleftrightarrow> ((\<forall>i \<in> I. F \<in> A(i) leadsTo B) & F \<in> program & st_set(B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   283
apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   284
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   285
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   286
lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) leadsTo B) \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A leadsTo B) & F \<in> program & st_set(B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   287
by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   288
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   289
text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   290
lemma leadsTo_Diff:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   291
     "[| F: (A-B) leadsTo C; F \<in> B leadsTo C; st_set(C) |]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   292
      ==> F \<in> A leadsTo C"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   293
by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   294
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   295
lemma leadsTo_UN_UN:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   296
    "[|!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i); F \<in> program |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   297
     ==> F: (\<Union>i \<in> I. A(i)) leadsTo (\<Union>i \<in> I. A'(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   298
apply (rule leadsTo_Union)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   299
apply (auto intro: leadsTo_weaken_R dest: leadsToD2)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   300
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   301
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   302
(*Binary union version*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   303
lemma leadsTo_Un_Un: "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |] ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   304
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   305
prefer 2 apply (blast dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   306
apply (blast intro: leadsTo_Un leadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   307
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   308
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   309
(** The cancellation law **)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   310
lemma leadsTo_cancel2: "[|F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B'|] ==> F \<in> A leadsTo (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   311
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F \<in> program")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   312
prefer 2 apply (blast dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   313
apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   314
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   315
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   316
lemma leadsTo_cancel_Diff2: "[|F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B'|]==> F \<in> A leadsTo (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   317
apply (rule leadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   318
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   319
apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   320
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   321
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   322
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   323
lemma leadsTo_cancel1: "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |] ==> F \<in> A leadsTo (B' \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   324
apply (simp add: Un_commute)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   325
apply (blast intro!: leadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   326
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   327
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   328
lemma leadsTo_cancel_Diff1:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   329
     "[|F \<in> A leadsTo (B \<union> A'); F: (B-A') leadsTo B'|]==> F \<in> A leadsTo (B' \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   330
apply (rule leadsTo_cancel1)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   331
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   332
apply (blast intro: leadsTo_weaken_R dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   333
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   334
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   335
(*The INDUCTION rule as we should have liked to state it*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   336
lemma leadsTo_induct:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   337
  assumes major: "F \<in> za leadsTo zb"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   338
      and basis: "!!A B. [|F \<in> A ensures B; st_set(A); st_set(B)|] ==> P(A,B)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   339
      and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   340
                              F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   341
      and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   342
                           st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   343
  shows "P(za, zb)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   344
apply (cut_tac major)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   345
apply (unfold leadsTo_def, clarify)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   346
apply (erule leads.induct)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   347
  apply (blast intro: basis [unfolded st_set_def])
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   348
 apply (blast intro: trans [unfolded leadsTo_def])
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   349
apply (force intro: union [unfolded st_set_def leadsTo_def])
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   350
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   351
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   352
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   353
(* Added by Sidi, an induction rule without ensures *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   354
lemma leadsTo_induct2:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   355
  assumes major: "F \<in> za leadsTo zb"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   356
      and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   357
      and basis2: "!!A B. [| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   358
                          ==> P(A, B)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   359
      and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   360
                              F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   361
      and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   362
                           st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   363
  shows "P(za, zb)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   364
apply (cut_tac major)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   365
apply (erule leadsTo_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   366
apply (auto intro: trans union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   367
apply (simp add: ensures_def, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   368
apply (frule constrainsD2)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   369
apply (drule_tac B' = " (A-B) \<union> B" in constrains_weaken_R)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   370
apply blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   371
apply (frule ensuresI2 [THEN leadsTo_Basis])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   372
apply (drule_tac [4] basis2, simp_all)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   373
apply (frule_tac A1 = A and B = B in Int_lower2 [THEN basis1])
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   374
apply (subgoal_tac "A=\<Union>({A - B, A \<inter> B}) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   375
prefer 2 apply blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   376
apply (erule ssubst)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   377
apply (rule union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   378
apply (auto intro: subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   379
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   380
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   381
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   382
(** Variant induction rule: on the preconditions for B **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   383
(*Lemma is the weak version: can't see how to do it in one step*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   384
lemma leadsTo_induct_pre_aux:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   385
  "[| F \<in> za leadsTo zb;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   386
      P(zb);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   387
      !!A B. [| F \<in> A ensures B;  P(B); st_set(A); st_set(B) |] ==> P(A);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   388
      !!S. [| \<forall>A \<in> S. P(A); \<forall>A \<in> S. st_set(A) |] ==> P(\<Union>(S))
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   389
   |] ==> P(za)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   390
txt{*by induction on this formula*}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   391
apply (subgoal_tac "P (zb) \<longrightarrow> P (za) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   392
txt{*now solve first subgoal: this formula is sufficient*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   393
apply (blast intro: leadsTo_refl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   394
apply (erule leadsTo_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   395
apply (blast+)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   396
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   397
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   398
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   399
lemma leadsTo_induct_pre:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   400
  "[| F \<in> za leadsTo zb;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   401
      P(zb);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   402
      !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P(B); st_set(A) |] ==> P(A);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   403
      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P(A) & st_set(A) ==> P(\<Union>(S))
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   404
   |] ==> P(za)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   405
apply (subgoal_tac " (F \<in> za leadsTo zb) & P (za) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   406
apply (erule conjunct2)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   407
apply (frule leadsToD2)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   408
apply (erule leadsTo_induct_pre_aux)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   409
prefer 3 apply (blast dest: leadsToD2 intro: leadsTo_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   410
prefer 2 apply (blast intro: leadsTo_Trans leadsTo_Basis)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   411
apply (blast intro: leadsTo_refl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   412
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   413
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   414
(** The impossibility law **)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   415
lemma leadsTo_empty:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   416
   "F \<in> A leadsTo 0 ==> A=0"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   417
apply (erule leadsTo_induct_pre)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   418
apply (auto simp add: ensures_def constrains_def transient_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   419
apply (drule bspec, assumption)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   420
apply blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   421
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   422
declare leadsTo_empty [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   423
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   424
subsection{*PSP: Progress-Safety-Progress*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   425
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   426
text{*Special case of PSP: Misra's "stable conjunction"*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   427
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   428
lemma psp_stable:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   429
   "[| F \<in> A leadsTo A'; F \<in> stable(B) |] ==> F:(A \<inter> B) leadsTo (A' \<inter> B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   430
apply (unfold stable_def)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   431
apply (frule leadsToD2)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   432
apply (erule leadsTo_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   433
prefer 3 apply (blast intro: leadsTo_Union_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   434
prefer 2 apply (blast intro: leadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   435
apply (rule leadsTo_Basis)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   436
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   437
apply (auto intro: transient_strengthen constrains_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   438
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   439
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   440
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   441
lemma psp_stable2: "[|F \<in> A leadsTo A'; F \<in> stable(B) |]==>F: (B \<inter> A) leadsTo (B \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   442
apply (simp (no_asm_simp) add: psp_stable Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   443
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   444
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   445
lemma psp_ensures:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   446
"[| F \<in> A ensures A'; F \<in> B co B' |]==> F: (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   447
apply (unfold ensures_def constrains_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   448
(*speeds up the proof*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   449
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   450
apply (blast intro: transient_strengthen)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   451
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   452
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   453
lemma psp:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   454
"[|F \<in> A leadsTo A'; F \<in> B co B'; st_set(B')|]==> F:(A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   455
apply (subgoal_tac "F \<in> program & st_set (A) & st_set (A') & st_set (B) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   456
prefer 2 apply (blast dest!: constrainsD2 leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   457
apply (erule leadsTo_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   458
prefer 3 apply (blast intro: leadsTo_Union_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   459
 txt{*Basis case*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   460
 apply (blast intro: psp_ensures leadsTo_Basis)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   461
txt{*Transitivity case has a delicate argument involving "cancellation"*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   462
apply (rule leadsTo_Un_duplicate2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   463
apply (erule leadsTo_cancel_Diff1)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   464
apply (simp add: Int_Diff Diff_triv)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   465
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   466
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   467
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   468
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   469
lemma psp2: "[| F \<in> A leadsTo A'; F \<in> B co B'; st_set(B') |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   470
    ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   471
by (simp (no_asm_simp) add: psp Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   472
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   473
lemma psp_unless:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   474
   "[| F \<in> A leadsTo A';  F \<in> B unless B'; st_set(B); st_set(B') |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   475
    ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   476
apply (unfold unless_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   477
apply (subgoal_tac "st_set (A) &st_set (A') ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   478
prefer 2 apply (blast dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   479
apply (drule psp, assumption, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   480
apply (blast intro: leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   481
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   482
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   483
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   484
subsection{*Proving the induction rules*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   485
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   486
(** The most general rule \<in> r is any wf relation; f is any variant function **)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   487
lemma leadsTo_wf_induct_aux: "[| wf(r);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   488
         m \<in> I;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   489
         field(r)<=I;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   490
         F \<in> program; st_set(B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   491
         \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) leadsTo
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   492
                    ((A \<inter> f-``(converse(r)``{m})) \<union> B) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   493
      ==> F \<in> (A \<inter> f-``{m}) leadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   494
apply (erule_tac a = m in wf_induct2, simp_all)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   495
apply (subgoal_tac "F \<in> (A \<inter> (f-`` (converse (r) ``{x}))) leadsTo B")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   496
 apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   497
apply (subst vimage_eq_UN)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   498
apply (simp del: UN_simps add: Int_UN_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   499
apply (auto intro: leadsTo_UN simp del: UN_simps simp add: Int_UN_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   500
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   501
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   502
(** Meta or object quantifier ? **)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   503
lemma leadsTo_wf_induct: "[| wf(r);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   504
         field(r)<=I;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   505
         A<=f-``I;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   506
         F \<in> program; st_set(A); st_set(B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   507
         \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) leadsTo
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   508
                    ((A \<inter> f-``(converse(r)``{m})) \<union> B) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   509
      ==> F \<in> A leadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   510
apply (rule_tac b = A in subst)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   511
 defer 1
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   512
 apply (rule_tac I = I in leadsTo_UN)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   513
 apply (erule_tac I = I in leadsTo_wf_induct_aux, assumption+, best)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   514
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   515
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   516
lemma nat_measure_field: "field(measure(nat, %x. x)) = nat"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   517
apply (unfold field_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   518
apply (simp add: measure_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   519
apply (rule equalityI, force, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   520
apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   521
apply (erule nat_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   522
apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   523
apply (rule_tac b = "succ (0) " in domainI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   524
apply simp_all
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   525
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   526
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   527
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   528
lemma Image_inverse_lessThan: "k<A ==> measure(A, %x. x) -`` {k} = k"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   529
apply (rule equalityI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   530
apply (auto simp add: measure_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   531
apply (blast intro: ltD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   532
apply (rule vimageI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   533
prefer 2 apply blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   534
apply (simp add: lt_Ord lt_Ord2 Ord_mem_iff_lt)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   535
apply (blast intro: lt_trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   536
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   537
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   538
(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   539
lemma lessThan_induct:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   540
 "[| A<=f-``nat;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   541
     F \<in> program; st_set(A); st_set(B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   542
     \<forall>m \<in> nat. F:(A \<inter> f-``{m}) leadsTo ((A \<inter> f -`` m) \<union> B) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   543
      ==> F \<in> A leadsTo B"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   544
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct])
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   545
apply (simp_all add: nat_measure_field)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   546
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   547
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   548
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   549
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   550
(*** wlt ****)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   551
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   552
(*Misra's property W3*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   553
lemma wlt_type: "wlt(F,B) <=state"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   554
by (unfold wlt_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   555
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   556
lemma wlt_st_set: "st_set(wlt(F, B))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   557
apply (unfold st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   558
apply (rule wlt_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   559
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   560
declare wlt_st_set [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   561
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   562
lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   563
apply (unfold wlt_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   564
apply (blast dest: leadsToD2 intro!: leadsTo_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   565
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   566
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   567
(* [| F \<in> program;  st_set(B) |] ==> F \<in> wlt(F, B) leadsTo B  *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 37936
diff changeset
   568
lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   569
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   570
lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt(F, B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   571
apply (unfold wlt_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   572
apply (frule leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   573
apply (auto simp add: st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   574
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   575
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   576
(*Misra's property W2*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   577
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B \<longleftrightarrow> (A \<subseteq> wlt(F,B) & F \<in> program & st_set(B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   578
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   579
apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   580
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   581
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   582
(*Misra's property W4*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   583
lemma wlt_increasing: "[| F \<in> program; st_set(B) |] ==> B \<subseteq> wlt(F,B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   584
apply (rule leadsTo_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   585
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [THEN iff_sym] subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   586
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   587
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   588
(*Used in the Trans case below*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   589
lemma leadsTo_123_aux:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   590
   "[| B \<subseteq> A2;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   591
       F \<in> (A1 - B) co (A1 \<union> B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   592
       F \<in> (A2 - C) co (A2 \<union> C) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   593
    ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   594
apply (unfold constrains_def st_set_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   595
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   596
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   597
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   598
(* slightly different from the HOL one \<in> B here is bounded *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   599
lemma leadsTo_123: "F \<in> A leadsTo A'
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   600
      ==> \<exists>B \<in> Pow(state). A<=B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   601
apply (frule leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   602
apply (erule leadsTo_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   603
  txt{*Basis*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   604
  apply (blast dest: ensuresD constrainsD2 st_setD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   605
 txt{*Trans*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   606
 apply clarify
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   607
 apply (rule_tac x = "Ba \<union> Bb" in bexI)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   608
 apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   609
txt{*Union*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   610
apply (clarify dest!: ball_conj_distrib [THEN iffD1])
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   611
apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba leadsTo B & F \<in> Ba - B co Ba \<union> B}) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   612
defer 1
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   613
apply (rule AC_ball_Pi, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   614
apply (rotate_tac 1)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   615
apply (drule_tac x = x in bspec, blast, blast)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   616
apply (rule_tac x = "\<Union>A \<in> S. y`A" in bexI, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   617
apply (rule_tac [3] I1 = S in constrains_UN [THEN constrains_weaken])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   618
apply (rule_tac [2] leadsTo_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   619
prefer 5 apply (blast dest!: apply_type, simp_all)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   620
apply (force dest!: apply_type)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   621
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   622
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   623
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   624
(*Misra's property W5*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   625
lemma wlt_constrains_wlt: "[| F \<in> program; st_set(B) |] ==>F \<in> (wlt(F, B) - B) co (wlt(F,B))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   626
apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], assumption, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   627
apply clarify
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   628
apply (subgoal_tac "Ba = wlt (F,B) ")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   629
prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   630
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   631
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   632
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   633
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   634
subsection{*Completion: Binary and General Finite versions*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   635
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   636
lemma completion_aux: "[| W = wlt(F, (B' \<union> C));
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   637
       F \<in> A leadsTo (A' \<union> C);  F \<in> A' co (A' \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   638
       F \<in> B leadsTo (B' \<union> C);  F \<in> B' co (B' \<union> C) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   639
    ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   640
apply (subgoal_tac "st_set (C) &st_set (W) &st_set (W-C) &st_set (A') &st_set (A) & st_set (B) & st_set (B') & F \<in> program")
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   641
 prefer 2
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   642
 apply simp
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   643
 apply (blast dest!: leadsToD2)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   644
apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   645
 prefer 2
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   646
 apply (blast intro!: constrains_weaken [OF constrains_Un [OF _ wlt_constrains_wlt]])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   647
apply (subgoal_tac "F \<in> (W-C) co W")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   648
 prefer 2
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   649
 apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   650
apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   651
 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   652
(** step 13 **)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   653
apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   654
apply (drule leadsTo_Diff)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   655
apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   656
apply (force simp add: st_set_def)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   657
apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   658
prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   659
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   660
txt{*last subgoal*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   661
apply (rule_tac leadsTo_Un_duplicate2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   662
apply (rule_tac leadsTo_Un_Un)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   663
 prefer 2 apply (blast intro: leadsTo_refl)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   664
apply (rule_tac A'1 = "B' \<union> C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken])
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   665
apply blast+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   666
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   667
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 37936
diff changeset
   668
lemmas completion = refl [THEN completion_aux]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   669
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   670
lemma finite_completion_aux:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   671
     "[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   672
       (\<forall>i \<in> I. F \<in> (A(i)) leadsTo (A'(i) \<union> C)) \<longrightarrow>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   673
                     (\<forall>i \<in> I. F \<in> (A'(i)) co (A'(i) \<union> C)) \<longrightarrow>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   674
                   F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   675
apply (erule Fin_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   676
apply (auto simp add: Inter_0)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   677
apply (rule completion)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   678
apply (auto simp del: INT_simps simp add: INT_extend_simps)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   679
apply (blast intro: constrains_INT)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   680
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   681
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   682
lemma finite_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   683
     "[| I \<in> Fin(X);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   684
         !!i. i \<in> I ==> F \<in> A(i) leadsTo (A'(i) \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   685
         !!i. i \<in> I ==> F \<in> A'(i) co (A'(i) \<union> C); F \<in> program; st_set(C)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   686
      ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   687
by (blast intro: finite_completion_aux [THEN mp, THEN mp])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   688
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   689
lemma stable_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   690
     "[| F \<in> A leadsTo A';  F \<in> stable(A');
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   691
         F \<in> B leadsTo B';  F \<in> stable(B') |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   692
    ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   693
apply (unfold stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   694
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   695
apply (blast dest: leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   696
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   697
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   698
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   699
lemma finite_stable_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   700
     "[| I \<in> Fin(X);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   701
         (!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i));
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   702
         (!!i. i \<in> I ==> F \<in> stable(A'(i)));  F \<in> program |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   703
      ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo (\<Inter>i \<in> I. A'(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   704
apply (unfold stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   705
apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   706
prefer 2 apply (blast dest: leadsToD2)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   707
apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   708
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14077
diff changeset
   709
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   710
end