src/ZF/UNITY/SubstAx.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 51717 9e7d1c139569
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:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
     1
(*  Title:      ZF/UNITY/SubstAx.thy
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
Theory ported from HOL.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
     8
header{*Weak LeadsTo relation (restricted to the set of reachable states)*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
     9
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    10
theory SubstAx
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    11
imports WFair Constrains
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    12
begin
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    14
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    15
  (* The definitions below are not `conventional', but yield simpler rules *)
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    16
  Ensures :: "[i,i] => i"            (infixl "Ensures" 60)  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    17
  "A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    18
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    19
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    20
  LeadsTo :: "[i, i] => i"            (infixl "LeadsTo" 60)  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    21
  "A LeadsTo B == {F \<in> program. F:(reachable(F) \<inter> A) leadsTo (reachable(F) \<inter> B)}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    22
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    23
notation (xsymbols)
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    24
  LeadsTo  (infixl " \<longmapsto>w " 60)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    25
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    26
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    27
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    28
(*Resembles the previous definition of LeadsTo*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    29
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    30
(* Equivalence with the HOL-like definition *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    31
lemma LeadsTo_eq:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    32
"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) \<inter> A) leadsTo B}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    33
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    34
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    35
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    36
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    37
lemma LeadsTo_type: "A LeadsTo B <=program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    38
by (unfold LeadsTo_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    39
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    40
(*** Specialized laws for handling invariants ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    41
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    42
(** Conjoining an Always property **)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    43
lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) LeadsTo A') \<longleftrightarrow> (F \<in> A LeadsTo A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    44
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    45
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    46
lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I \<inter> A')) \<longleftrightarrow> (F \<in> A LeadsTo A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    47
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    48
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    49
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    50
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    51
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    52
lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    53
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    54
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    55
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    56
lemma Always_LeadsToD: "[| F \<in> Always(C);  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    57
by (blast intro: Always_LeadsTo_post [THEN iffD2])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    58
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    59
(*** Introduction rules \<in> Basis, Trans, Union ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    60
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    61
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    62
by (auto simp add: Ensures_def LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    63
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    64
lemma LeadsTo_Trans:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    65
     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    66
apply (simp (no_asm_use) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    67
apply (blast intro: leadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    68
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    69
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    70
lemma LeadsTo_Union:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    71
"[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> \<Union>(S) LeadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    72
apply (simp add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    73
apply (subst Int_Union_Union2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    74
apply (rule leadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    75
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    76
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    77
(*** Derived rules ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    78
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    79
lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    80
apply (frule leadsToD2, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    81
apply (simp (no_asm_simp) add: LeadsTo_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    82
apply (blast intro: leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    83
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    84
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    85
(*Useful with cancellation, disjunction*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    86
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: 12195
diff changeset
    87
by (simp add: Un_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    88
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    89
lemma LeadsTo_Un_duplicate2:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
    90
     "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: 12195
diff changeset
    91
by (simp add: Un_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    92
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    93
lemma LeadsTo_UN:
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    94
    "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    95
     ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    96
apply (simp add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    97
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    98
apply (rule leadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    99
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   100
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   101
(*Binary union introduction rule*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   102
lemma LeadsTo_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   103
     "[| 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: 12195
diff changeset
   104
apply (subst Un_eq_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   105
apply (rule LeadsTo_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   106
apply (auto dest: LeadsTo_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   107
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   108
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   109
(*Lets us look at the starting state*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   110
lemma single_LeadsTo_I:
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   111
    "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   112
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   113
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   114
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   115
lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A LeadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   116
apply (simp (no_asm_simp) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   117
apply (blast intro: subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   118
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   119
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   120
lemma empty_LeadsTo: "F \<in> 0 LeadsTo A \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   121
by (auto dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   122
            intro: empty_subsetI [THEN subset_imp_LeadsTo])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   123
declare empty_LeadsTo [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   124
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   125
lemma LeadsTo_state: "F \<in> A LeadsTo state \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   126
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   127
declare LeadsTo_state [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   128
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   129
lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A';  A'<=B'|] ==> F \<in> A LeadsTo B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   130
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   131
apply (auto intro: leadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   132
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   133
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   134
lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B \<subseteq> A |] ==> F \<in> B LeadsTo A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   135
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   136
apply (auto intro: leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   137
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   138
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   139
lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   140
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   141
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   142
lemma Always_LeadsTo_weaken:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   143
"[| F \<in> Always(C);  F \<in> A LeadsTo A'; C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   144
      ==> F \<in> B LeadsTo B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   145
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   146
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   147
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   148
(** Two theorems for "proof lattices" **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   149
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   150
lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A \<union> B) LeadsTo B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   151
by (blast dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   152
             intro: LeadsTo_Un subset_imp_LeadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   153
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   154
lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   155
      ==> F \<in> (A \<union> B) LeadsTo C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   156
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   157
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   158
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   159
(** Distributive laws **)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   160
lemma LeadsTo_Un_distrib: "(F \<in> (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: 12195
diff changeset
   161
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   162
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   163
lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) \<longleftrightarrow>  (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   164
by (blast dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   165
             intro: LeadsTo_UN LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   166
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   167
lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) LeadsTo B)  \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   168
by (blast dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   169
             intro: LeadsTo_Union LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   170
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   171
(** More rules using the premise "Always(I)" **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   172
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   173
lemma EnsuresI: "[| 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: 12195
diff changeset
   174
apply (simp add: Ensures_def Constrains_eq_constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   175
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   176
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   177
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   178
lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I \<inter> (A-A')) Co (A \<union> A');
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   179
         F \<in> transient (I \<inter> (A-A')) |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   180
  ==> F \<in> A LeadsTo A'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   181
apply (rule Always_LeadsToI, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   182
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   183
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   184
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   185
(*Set difference: maybe combine with leadsTo_weaken_L??
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   186
  This is the most useful form of the "disjunction" rule*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   187
lemma LeadsTo_Diff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   188
     "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |] ==> F \<in> A LeadsTo C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   189
by (blast intro: LeadsTo_Un LeadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   190
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   191
lemma LeadsTo_UN_UN:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   192
     "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   193
      ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   194
apply (rule LeadsTo_Union, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   195
apply (blast intro: LeadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   196
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   197
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   198
(*Binary union version*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   199
lemma LeadsTo_Un_Un:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   200
  "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A \<union> B) LeadsTo (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   201
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   202
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   203
(** The cancellation law **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   204
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   205
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: 12195
diff changeset
   206
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   207
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   208
lemma Un_Diff: "A \<union> (B - A) = A \<union> B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   209
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   210
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   211
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: 12195
diff changeset
   212
apply (rule LeadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   213
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   214
apply (simp (no_asm_simp) add: Un_Diff)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   215
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   216
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   217
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: 12195
diff changeset
   218
apply (simp add: Un_commute)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   219
apply (blast intro!: LeadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   220
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   221
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   222
lemma Diff_Un2: "(B - A) \<union> A = B \<union> A"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   223
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   224
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   225
lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   226
apply (rule LeadsTo_cancel1)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   227
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   228
apply (simp (no_asm_simp) add: Diff_Un2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   229
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   230
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   231
(** The impossibility law **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   232
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   233
(*The set "A" may be non-empty, but it contains no reachable states*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   234
lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   235
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   236
apply (cut_tac reachable_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   237
apply (auto dest!: leadsTo_empty)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   238
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   239
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   240
(** PSP \<in> Progress-Safety-Progress **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   241
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   242
(*Special case of PSP \<in> Misra's "stable conjunction"*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   243
lemma PSP_Stable: "[| 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: 12195
diff changeset
   244
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   245
apply (drule psp_stable, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   246
apply (simp add: Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   247
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   248
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   249
lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   250
apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   251
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   252
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   253
lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   254
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   255
apply (blast dest: psp intro: leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   256
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   257
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   258
lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   259
by (simp (no_asm_simp) add: PSP Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   260
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   261
lemma PSP_Unless:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   262
"[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   263
apply (unfold op_Unless_def)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   264
apply (drule PSP, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   265
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   266
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   267
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   268
(*** Induction rules ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   269
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   270
(** Meta or object quantifier ????? **)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   271
lemma LeadsTo_wf_induct: "[| wf(r);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   272
         \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) LeadsTo
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   273
                            ((A \<inter> f-``(converse(r) `` {m})) \<union> B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   274
         field(r)<=I; A<=f-``I; F \<in> program |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   275
      ==> F \<in> A LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   276
apply (simp (no_asm_use) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   277
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   278
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   279
apply (drule_tac [2] x = m in bspec, safe)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   280
apply (rule_tac [2] A' = "reachable (F) \<inter> (A \<inter> f -`` (converse (r) ``{m}) \<union> B) " in leadsTo_weaken_R)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   281
apply (auto simp add: Int_assoc)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   282
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   283
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   284
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   285
lemma LessThan_induct: "[| \<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: 12195
diff changeset
   286
      A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   287
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   288
apply (simp_all add: nat_measure_field)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   289
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   290
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   291
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   292
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   293
(******
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   294
 To be ported ??? I am not sure.
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   295
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   296
  integ_0_le_induct
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   297
  LessThan_bounded_induct
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   298
  GreaterThan_bounded_induct
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   299
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   300
*****)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   301
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   302
(*** Completion \<in> Binary and General Finite versions ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   303
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   304
lemma Completion: "[| F \<in> A LeadsTo (A' \<union> C);  F \<in> A' Co (A' \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   305
         F \<in> B LeadsTo (B' \<union> C);  F \<in> B' Co (B' \<union> C) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   306
      ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   307
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   308
apply (blast intro: completion leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   309
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   310
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   311
lemma Finite_completion_aux:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   312
     "[| I \<in> Fin(X);F \<in> program |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   313
      ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) \<union> C)) \<longrightarrow>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   314
          (\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   315
          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: 12195
diff changeset
   316
apply (erule Fin_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   317
apply (auto simp del: INT_simps simp add: Inter_0)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   318
apply (rule Completion, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   319
apply (simp del: INT_simps add: INT_extend_simps)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   320
apply (blast intro: Constrains_INT)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   321
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   322
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   323
lemma Finite_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   324
     "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   325
         !!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   326
         F \<in> program |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   327
      ==> 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: 12195
diff changeset
   328
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   329
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   330
lemma Stable_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   331
     "[| F \<in> A LeadsTo A';  F \<in> Stable(A');
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   332
         F \<in> B LeadsTo B';  F \<in> Stable(B') |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   333
    ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   334
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   335
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   336
    prefer 5
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   337
    apply blast
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   338
apply auto
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   339
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   340
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   341
lemma Finite_stable_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   342
     "[| I \<in> Fin(X);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   343
         (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   344
         (!!i. i \<in> I ==>F \<in> Stable(A'(i)));   F \<in> program  |]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   345
      ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   346
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   347
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   348
apply (rule_tac [3] subset_refl, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   349
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   350
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   351
ML {*
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   352
(*proves "ensures/leadsTo" properties when the program is specified*)
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 18371
diff changeset
   353
fun ensures_tac ctxt sact =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   354
  let val ss = simpset_of ctxt in
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   355
    SELECT_GOAL
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   356
      (EVERY [REPEAT (Always_Int_tac 1),
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   357
              etac @{thm Always_LeadsTo_Basis} 1
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   358
                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   359
                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   360
                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   361
              (*now there are two subgoals: co & transient*)
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   362
              simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   363
              res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   364
                 (*simplify the command's domain*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   365
              simp_tac (ss addsimps [@{thm domain_def}]) 3,
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   366
              (* proving the domain part *)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   367
             clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   368
             rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
35409
5c5bb83f2bae more antiquotations;
wenzelm
parents: 32960
diff changeset
   369
             asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   370
             REPEAT (rtac @{thm state_update_type} 3),
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 18371
diff changeset
   371
             constrains_tac ctxt 1,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   372
             ALLGOALS (clarify_tac ctxt),
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   373
             ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   374
                        ALLGOALS (clarify_tac ctxt),
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 18371
diff changeset
   375
            ALLGOALS (asm_lr_simp_tac ss)])
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 18371
diff changeset
   376
  end;
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   377
*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   378
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 42793
diff changeset
   379
method_setup ensures = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 27882
diff changeset
   380
    Args.goal_spec -- Scan.lift Args.name_source >>
d2d7874648bd simplified method setup;
wenzelm
parents: 27882
diff changeset
   381
    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
d2d7874648bd simplified method setup;
wenzelm
parents: 27882
diff changeset
   382
*} "for proving progress properties"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   383
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   384
end