src/ZF/UNITY/SubstAx.thy
author nipkow
Sun, 04 Nov 2018 12:07:24 +0100
changeset 69232 2b913054a9cf
parent 63120 629a4c5e953e
child 69587 53982d5ec0bb
permissions -rw-r--r--
Faster Braun tree functions
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
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
     8
section\<open>Weak LeadsTo relation (restricted to the set of reachable states)\<close>
15634
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
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    20
  LeadsTo :: "[i, i] => i"            (infixl "\<longmapsto>w" 60)  where
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    21
  "A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    22
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    23
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    24
(*Resembles the previous definition of LeadsTo*)
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
(* Equivalence with the HOL-like definition *)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    27
lemma LeadsTo_eq:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    28
"st_set(B)==> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    29
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    30
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    31
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    32
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    33
lemma LeadsTo_type: "A \<longmapsto>w B <=program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    34
by (unfold LeadsTo_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    35
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    36
(*** Specialized laws for handling invariants ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    37
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    38
(** Conjoining an Always property **)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    39
lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) \<longmapsto>w A') \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    40
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
    41
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    42
lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    43
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    44
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
    45
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    46
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    47
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    48
lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    49
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
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_post RS iffD2', but with premises in the good order *)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    52
lemma Always_LeadsToD: "[| F \<in> Always(C);  F \<in> A \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w (C \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    53
by (blast intro: Always_LeadsTo_post [THEN iffD2])
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
(*** Introduction rules \<in> Basis, Trans, Union ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    56
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    57
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    58
by (auto simp add: Ensures_def LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    59
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    60
lemma LeadsTo_Trans:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    61
     "[| F \<in> A \<longmapsto>w B;  F \<in> B \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    62
apply (simp (no_asm_use) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    63
apply (blast intro: leadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    64
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    65
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    66
lemma LeadsTo_Union:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    67
"[|(!!A. A \<in> S ==> F \<in> A \<longmapsto>w B); F \<in> program|]==>F \<in> \<Union>(S) \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    68
apply (simp add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    69
apply (subst Int_Union_Union2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    70
apply (rule leadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    71
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    72
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    73
(*** Derived rules ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    74
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    75
lemma leadsTo_imp_LeadsTo: "F \<in> A \<longmapsto> B ==> F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    76
apply (frule leadsToD2, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    77
apply (simp (no_asm_simp) add: LeadsTo_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    78
apply (blast intro: leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    79
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    80
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    81
(*Useful with cancellation, disjunction*)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    82
lemma LeadsTo_Un_duplicate: "F \<in> A \<longmapsto>w (A' \<union> A') ==> F \<in> A \<longmapsto>w A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    83
by (simp add: Un_ac)
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
lemma LeadsTo_Un_duplicate2:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    86
     "F \<in> A \<longmapsto>w (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto>w (A' \<union> C)"
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:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    90
    "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w B); F \<in> program|]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    91
     ==>F:(\<Union>i \<in> I. A(i)) \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    92
apply (simp add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    93
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    94
apply (rule leadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    95
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    96
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    97
(*Binary union introduction rule*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
    98
lemma LeadsTo_Un:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
    99
     "[| F \<in> A \<longmapsto>w C; F \<in> B \<longmapsto>w C |] ==> F \<in> (A \<union> B) \<longmapsto>w C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   100
apply (subst Un_eq_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   101
apply (rule LeadsTo_Union)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   102
apply (auto dest: LeadsTo_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   103
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   104
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   105
(*Lets us look at the starting state*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   106
lemma single_LeadsTo_I:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   107
    "[|(!!s. s \<in> A ==> F:{s} \<longmapsto>w B); F \<in> program|]==>F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   108
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   109
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   110
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   111
lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   112
apply (simp (no_asm_simp) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   113
apply (blast intro: subset_imp_leadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   114
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   115
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   116
lemma empty_LeadsTo: "F \<in> 0 \<longmapsto>w A \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   117
by (auto dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   118
            intro: empty_subsetI [THEN subset_imp_LeadsTo])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   119
declare empty_LeadsTo [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   120
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   121
lemma LeadsTo_state: "F \<in> A \<longmapsto>w state \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   122
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   123
declare LeadsTo_state [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   124
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   125
lemma LeadsTo_weaken_R: "[| F \<in> A \<longmapsto>w A';  A'<=B'|] ==> F \<in> A \<longmapsto>w B'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   126
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   127
apply (auto intro: leadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   128
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   129
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   130
lemma LeadsTo_weaken_L: "[| F \<in> A \<longmapsto>w A'; B \<subseteq> A |] ==> F \<in> B \<longmapsto>w A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   131
apply (unfold LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   132
apply (auto intro: leadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   133
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   134
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   135
lemma LeadsTo_weaken: "[| F \<in> A \<longmapsto>w A'; B<=A; A'<=B' |] ==> F \<in> B \<longmapsto>w B'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   136
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   137
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   138
lemma Always_LeadsTo_weaken:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   139
"[| F \<in> Always(C);  F \<in> A \<longmapsto>w A'; C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   140
      ==> F \<in> B \<longmapsto>w B'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   141
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   142
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   143
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   144
(** Two theorems for "proof lattices" **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   145
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   146
lemma LeadsTo_Un_post: "F \<in> A \<longmapsto>w B ==> F:(A \<union> B) \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   147
by (blast dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   148
             intro: LeadsTo_Un subset_imp_LeadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   149
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   150
lemma LeadsTo_Trans_Un: "[| F \<in> A \<longmapsto>w B;  F \<in> B \<longmapsto>w C |]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   151
      ==> F \<in> (A \<union> B) \<longmapsto>w C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   152
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
   153
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   154
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   155
(** Distributive laws **)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   156
lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C)  \<longleftrightarrow> (F \<in> A \<longmapsto>w C & F \<in> B \<longmapsto>w C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   157
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   158
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   159
lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow>  (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) & F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   160
by (blast dest: LeadsTo_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   161
             intro: LeadsTo_UN LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   162
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   163
lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B)  \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A \<longmapsto>w 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_Union LeadsTo_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   166
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   167
(** More rules using the premise "Always(I)" **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   168
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   169
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
   170
apply (simp add: Ensures_def Constrains_eq_constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   171
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   172
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   173
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   174
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
   175
         F \<in> transient (I \<inter> (A-A')) |]
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   176
  ==> F \<in> A \<longmapsto>w A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   177
apply (rule Always_LeadsToI, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   178
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
   179
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   180
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   181
(*Set difference: maybe combine with leadsTo_weaken_L??
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   182
  This is the most useful form of the "disjunction" rule*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   183
lemma LeadsTo_Diff:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   184
     "[| F \<in> (A-B) \<longmapsto>w C;  F \<in> (A \<inter> B) \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   185
by (blast intro: LeadsTo_Un LeadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   186
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   187
lemma LeadsTo_UN_UN:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   188
     "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i)); F \<in> program |]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   189
      ==> F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w (\<Union>i \<in> I. A'(i))"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   190
apply (rule LeadsTo_Union, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   191
apply (blast intro: LeadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   192
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   193
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   194
(*Binary union version*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   195
lemma LeadsTo_Un_Un:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   196
  "[| F \<in> A \<longmapsto>w A'; F \<in> B \<longmapsto>w B' |] ==> F:(A \<union> B) \<longmapsto>w (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   197
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   198
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   199
(** The cancellation law **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   200
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   201
lemma LeadsTo_cancel2: "[| F \<in> A \<longmapsto>w(A' \<union> B); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   202
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
   203
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   204
lemma Un_Diff: "A \<union> (B - A) = A \<union> B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   205
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   206
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   207
lemma LeadsTo_cancel_Diff2: "[| F \<in> A \<longmapsto>w (A' \<union> B); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   208
apply (rule LeadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   209
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   210
apply (simp (no_asm_simp) add: Un_Diff)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   211
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   212
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   213
lemma LeadsTo_cancel1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   214
apply (simp add: Un_commute)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   215
apply (blast intro!: LeadsTo_cancel2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   216
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   217
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   218
lemma Diff_Un2: "(B - A) \<union> A = B \<union> A"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   219
by auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   220
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   221
lemma LeadsTo_cancel_Diff1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   222
apply (rule LeadsTo_cancel1)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   223
prefer 2 apply assumption
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   224
apply (simp (no_asm_simp) add: Diff_Un2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   225
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   226
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   227
(** The impossibility law **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   228
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   229
(*The set "A" may be non-empty, but it contains no reachable states*)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   230
lemma LeadsTo_empty: "F \<in> A \<longmapsto>w 0 ==> F \<in> Always (state -A)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   231
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   232
apply (cut_tac reachable_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   233
apply (auto dest!: leadsTo_empty)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   234
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   235
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   236
(** PSP \<in> Progress-Safety-Progress **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   237
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   238
(*Special case of PSP \<in> Misra's "stable conjunction"*)
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   239
lemma PSP_Stable: "[| F \<in> A \<longmapsto>w A';  F \<in> Stable(B) |]==> F:(A \<inter> B) \<longmapsto>w (A' \<inter> B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   240
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   241
apply (drule psp_stable, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   242
apply (simp add: Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   243
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   244
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   245
lemma PSP_Stable2: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) \<longmapsto>w (B \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   246
apply (simp (no_asm_simp) add: PSP_Stable 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
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   249
lemma PSP: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') \<longmapsto>w ((A' \<inter> B) \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   250
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   251
apply (blast dest: psp intro: leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   252
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   253
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   254
lemma PSP2: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B' |]==> F:(B' \<inter> A) \<longmapsto>w ((B \<inter> A') \<union> (B' - B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   255
by (simp (no_asm_simp) add: PSP Int_ac)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   256
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   257
lemma PSP_Unless:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   258
"[| F \<in> A \<longmapsto>w A'; F \<in> B Unless B'|]==> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   259
apply (unfold op_Unless_def)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   260
apply (drule PSP, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   261
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   262
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   263
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   264
(*** Induction rules ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   265
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   266
(** Meta or object quantifier ????? **)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   267
lemma LeadsTo_wf_induct: "[| wf(r);
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   268
         \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>w
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   269
                            ((A \<inter> f-``(converse(r) `` {m})) \<union> B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   270
         field(r)<=I; A<=f-``I; F \<in> program |]
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   271
      ==> F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   272
apply (simp (no_asm_use) add: LeadsTo_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   273
apply auto
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   274
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
   275
apply (drule_tac [2] x = m in bspec, safe)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 42814
diff changeset
   276
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
   277
apply (auto simp add: Int_assoc)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   278
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   279
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   280
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   281
lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto>w ((A \<inter> f-``m) \<union> B);
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   282
      A<=f-``nat; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   283
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
   284
apply (simp_all add: nat_measure_field)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   285
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   286
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   287
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   288
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   289
(******
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   290
 To be ported ??? I am not sure.
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
  integ_0_le_induct
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   293
  LessThan_bounded_induct
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   294
  GreaterThan_bounded_induct
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
*****)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   297
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   298
(*** Completion \<in> Binary and General Finite versions ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   299
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   300
lemma Completion: "[| F \<in> A \<longmapsto>w (A' \<union> C);  F \<in> A' Co (A' \<union> C);
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   301
         F \<in> B \<longmapsto>w (B' \<union> C);  F \<in> B' Co (B' \<union> C) |]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   302
      ==> F \<in> (A \<inter> B) \<longmapsto>w ((A' \<inter> B') \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   303
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
   304
apply (blast intro: completion leadsTo_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   305
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   306
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   307
lemma Finite_completion_aux:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   308
     "[| I \<in> Fin(X);F \<in> program |]
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   309
      ==> (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto>w (A'(i) \<union> C)) \<longrightarrow>
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   310
          (\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow>
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   311
          F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   312
apply (erule Fin_induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   313
apply (auto simp del: INT_simps simp add: Inter_0)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   314
apply (rule Completion, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   315
apply (simp del: INT_simps add: INT_extend_simps)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   316
apply (blast intro: Constrains_INT)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   317
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   318
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   319
lemma Finite_completion:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   320
     "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w (A'(i) \<union> C);
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   321
         !!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   322
         F \<in> program |]
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   323
      ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   324
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   325
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   326
lemma Stable_completion:
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   327
     "[| F \<in> A \<longmapsto>w A';  F \<in> Stable(A');
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   328
         F \<in> B \<longmapsto>w B';  F \<in> Stable(B') |]
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   329
    ==> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   330
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   331
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   332
    prefer 5
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   333
    apply blast
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   334
apply auto
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   335
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   336
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   337
lemma Finite_stable_completion:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   338
     "[| I \<in> Fin(X);
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   339
         (!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i));
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   340
         (!!i. i \<in> I ==>F \<in> Stable(A'(i)));   F \<in> program  |]
61392
331be2820f90 tuned syntax -- more symbols;
wenzelm
parents: 60774
diff changeset
   341
      ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   342
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   343
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   344
apply (rule_tac [3] subset_refl, auto)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   345
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   346
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   347
ML \<open>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   348
(*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
   349
fun ensures_tac ctxt sact =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   350
  SELECT_GOAL
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58871
diff changeset
   351
    (EVERY [REPEAT (Always_Int_tac ctxt 1),
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   352
            eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   353
                ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
60774
6c28d8ed2488 proper context;
wenzelm
parents: 60770
diff changeset
   354
                REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   355
                                  @{thm EnsuresI}, @{thm ensuresI}] 1),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   356
            (*now there are two subgoals: co & transient*)
57945
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 55111
diff changeset
   357
            simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
   358
            Rule_Insts.res_inst_tac ctxt
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
   359
              [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   360
               (*simplify the command's domain*)
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   361
            simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   362
            (* proving the domain part *)
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   363
           clarify_tac ctxt 3,
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   364
           dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4,
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   365
           resolve_tac ctxt @{thms ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   366
           asm_full_simp_tac ctxt 3, resolve_tac ctxt @{thms conjI} 3, simp_tac ctxt 4,
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
   367
           REPEAT (resolve_tac ctxt @{thms state_update_type} 3),
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   368
           constrains_tac ctxt 1,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   369
           ALLGOALS (clarify_tac ctxt),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   370
           ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   371
                      ALLGOALS (clarify_tac ctxt),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46953
diff changeset
   372
          ALLGOALS (asm_lr_simp_tac ctxt)]);
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   373
\<close>
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   374
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   375
method_setup ensures = \<open>
63120
629a4c5e953e embedded content may be delimited via cartouches;
wenzelm
parents: 61392
diff changeset
   376
    Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 27882
diff changeset
   377
    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 60754
diff changeset
   378
\<close> "for proving progress properties"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 12195
diff changeset
   379
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   380
end