src/ZF/UNITY/Constrains.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
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/Constrains.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
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
     6
header{*Weak Safety Properties*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
     7
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
     8
theory Constrains
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
     9
imports UNITY
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    10
begin
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    11
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    12
consts traces :: "[i, i] => i"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
  (* Initial states and program => (final state, reversed trace to it)... 
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    14
      the domain may also be state*list(state) *)
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    15
inductive 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    16
  domains 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    17
     "traces(init, acts)" <=
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    18
         "(init \<union> (\<Union>act\<in>acts. field(act)))*list(\<Union>act\<in>acts. field(act))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    19
  intros 
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    20
         (*Initial trace is empty*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    21
    Init: "s: init ==> <s,[]> \<in> traces(init,acts)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    22
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    23
    Acts: "[| act:acts;  <s,evs> \<in> traces(init,acts);  <s,s'>: act |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    24
           ==> <s', Cons(s,evs)> \<in> traces(init, acts)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    25
  
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    26
  type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    27
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    28
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    29
consts reachable :: "i=>i"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    30
inductive
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    31
  domains
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    32
  "reachable(F)" \<subseteq> "Init(F) \<union> (\<Union>act\<in>Acts(F). field(act))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    33
  intros 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    34
    Init: "s:Init(F) ==> s:reachable(F)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    35
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    36
    Acts: "[| act: Acts(F);  s:reachable(F);  <s,s'>: act |]
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    37
           ==> s':reachable(F)"
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    38
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    39
  type_intros UnI1 UnI2 fieldI2 UN_I
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    40
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    41
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    42
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    43
  Constrains :: "[i,i] => i"  (infixl "Co" 60)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    44
  "A Co B == {F:program. F:(reachable(F) \<inter> A) co B}"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    45
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    46
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    47
  op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    48
  "A Unless B == (A-B) Co (A \<union> B)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    49
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    50
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    51
  Stable     :: "i => i"  where
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    52
  "Stable(A) == A Co A"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    53
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    54
definition
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    55
  (*Always is the weak form of "invariant"*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
    56
  Always :: "i => i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    57
  "Always(A) == initially(A) \<inter> Stable(A)"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    58
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    59
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    60
(*** traces and reachable ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    61
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    62
lemma reachable_type: "reachable(F) \<subseteq> state"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    63
apply (cut_tac F = F in Init_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    64
apply (cut_tac F = F in Acts_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    65
apply (cut_tac F = F in reachable.dom_subset, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    66
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    67
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    68
lemma st_set_reachable: "st_set(reachable(F))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    69
apply (unfold st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    70
apply (rule reachable_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    71
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    72
declare st_set_reachable [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    73
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    74
lemma reachable_Int_state: "reachable(F) \<inter> state = reachable(F)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    75
by (cut_tac reachable_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    76
declare reachable_Int_state [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    77
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    78
lemma state_Int_reachable: "state \<inter> reachable(F) = reachable(F)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    79
by (cut_tac reachable_type, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    80
declare state_Int_reachable [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    81
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    82
lemma reachable_equiv_traces: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    83
"F \<in> program ==> reachable(F)={s \<in> state. \<exists>evs. <s,evs>:traces(Init(F), Acts(F))}"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    84
apply (rule equalityI, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    85
apply (blast dest: reachable_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    86
apply (erule_tac [2] traces.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    87
apply (erule reachable.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    88
apply (blast intro: reachable.intros traces.intros)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    89
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    90
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    91
lemma Init_into_reachable: "Init(F) \<subseteq> reachable(F)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    92
by (blast intro: reachable.intros)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    93
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    94
lemma stable_reachable: "[| F \<in> program; G \<in> program;  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    95
    Acts(G) \<subseteq> Acts(F)  |] ==> G \<in> stable(reachable(F))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    96
apply (blast intro: stableI constrainsI st_setI
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    97
             reachable_type [THEN subsetD] reachable.intros)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    98
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
    99
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   100
declare stable_reachable [intro!]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   101
declare stable_reachable [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   102
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   103
(*The set of all reachable states is an invariant...*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   104
lemma invariant_reachable: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   105
   "F \<in> program ==> F \<in> invariant(reachable(F))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   106
apply (unfold invariant_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   107
apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   108
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   109
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   110
(*...in fact the strongest invariant!*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   111
lemma invariant_includes_reachable: "F \<in> invariant(A) ==> reachable(F) \<subseteq> A"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   112
apply (cut_tac F = F in Acts_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   113
apply (cut_tac F = F in Init_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   114
apply (cut_tac F = F in reachable_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   115
apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   116
apply (rule subsetI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   117
apply (erule reachable.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   118
apply (blast intro: reachable.intros)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   119
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   120
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   121
(*** Co ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   122
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   123
lemma constrains_reachable_Int: "F \<in> B co B'==>F:(reachable(F) \<inter> B) co (reachable(F) \<inter> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   124
apply (frule constrains_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   125
apply (frule stable_reachable [OF _ _ subset_refl])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   126
apply (simp_all add: stable_def constrains_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   127
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   128
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   129
(*Resembles the previous definition of Constrains*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   130
lemma Constrains_eq_constrains: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   131
"A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F)  \<inter>  B)}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   132
apply (unfold Constrains_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   133
apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   134
             intro: constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   135
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   136
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   137
lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   138
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   139
lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   140
apply (unfold Constrains_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   141
apply (blast intro: constrains_weaken_L dest: constrainsD2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   142
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   143
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   144
lemma ConstrainsI: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   145
    "[|!!act s s'. [| act \<in> Acts(F); <s,s'>:act; s \<in> A |] ==> s':A'; 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   146
       F \<in> program|]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   147
     ==> F \<in> A Co A'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   148
apply (auto simp add: Constrains_def constrains_def st_set_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   149
apply (blast dest: reachable_type [THEN subsetD])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   150
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   151
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   152
lemma Constrains_type: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   153
 "A Co B \<subseteq> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   154
apply (unfold Constrains_def, blast)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   155
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   156
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   157
lemma Constrains_empty: "F \<in> 0 Co B \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   158
by (auto dest: Constrains_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   159
            intro: constrains_imp_Constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   160
declare Constrains_empty [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   161
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   162
lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   163
apply (unfold Constrains_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   164
apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   165
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   166
declare Constrains_state [iff]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   167
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   168
lemma Constrains_weaken_R: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   169
        "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   170
apply (unfold Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   171
apply (blast intro: constrains_weaken_R)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   172
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   173
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   174
lemma Constrains_weaken_L: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   175
    "[| F \<in> A Co A'; B<=A |] ==> F \<in> B Co A'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   176
apply (unfold Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   177
apply (blast intro: constrains_weaken_L st_set_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   178
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   179
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   180
lemma Constrains_weaken: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   181
   "[| F \<in> A Co A'; B<=A; A'<=B' |] ==> F \<in> B Co B'"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   182
apply (unfold Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   183
apply (blast intro: constrains_weaken st_set_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   184
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   185
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   186
(** Union **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   187
lemma Constrains_Un: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   188
    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   189
apply (unfold Constrains_def2, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   190
apply (simp add: Int_Un_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   191
apply (blast intro: constrains_Un)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   192
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   193
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   194
lemma Constrains_UN: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   195
    "[|(!!i. i \<in> I==>F \<in> A(i) Co A'(i)); F \<in> program|] 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   196
     ==> F:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> I. A'(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   197
by (auto intro: constrains_UN simp del: UN_simps 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   198
         simp add: Constrains_def2 Int_UN_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   199
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   200
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   201
(** Intersection **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   202
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   203
lemma Constrains_Int: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   204
    "[| F \<in> A Co A'; F \<in> B Co B'|]==> F:(A \<inter> B) Co (A' \<inter> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   205
apply (unfold Constrains_def)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   206
apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ")
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   207
apply (auto intro: constrains_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   208
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   209
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   210
lemma Constrains_INT: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   211
    "[| (!!i. i \<in> I ==>F \<in> A(i) Co A'(i)); F \<in> program  |]  
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   212
     ==> F:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> I. A'(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   213
apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   214
apply (rule constrains_INT)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   215
apply (auto simp add: Constrains_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   216
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   217
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   218
lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable(F) \<inter> A \<subseteq> A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   219
apply (unfold Constrains_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   220
apply (blast dest: constrains_imp_subset)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   221
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   222
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   223
lemma Constrains_trans: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   224
 "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   225
apply (unfold Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   226
apply (blast intro: constrains_trans constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   227
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   228
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   229
lemma Constrains_cancel: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   230
"[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   231
apply (unfold Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   232
apply (simp (no_asm_use) add: Int_Un_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   233
apply (blast intro: constrains_cancel)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   234
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   235
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   236
(*** Stable ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   237
(* Useful because there's no Stable_weaken.  [Tanja Vos] *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   238
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   239
lemma stable_imp_Stable: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   240
"F \<in> stable(A) ==> F \<in> Stable(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   241
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   242
apply (unfold stable_def Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   243
apply (erule constrains_imp_Constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   244
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   245
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   246
lemma Stable_eq: "[| F \<in> Stable(A); A = B |] ==> F \<in> Stable(B)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   247
by blast
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   248
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   249
lemma Stable_eq_stable: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   250
"F \<in> Stable(A) \<longleftrightarrow>  (F \<in> stable(reachable(F) \<inter> A))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   251
apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   252
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   253
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   254
lemma StableI: "F \<in> A Co A ==> F \<in> Stable(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   255
by (unfold Stable_def, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   256
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   257
lemma StableD: "F \<in> Stable(A) ==> F \<in> A Co A"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   258
by (unfold Stable_def, assumption)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   259
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   260
lemma Stable_Un: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   261
    "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable(A \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   262
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   263
apply (blast intro: Constrains_Un)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   264
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   265
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   266
lemma Stable_Int: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   267
    "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable (A \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   268
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   269
apply (blast intro: Constrains_Int)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   270
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   271
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   272
lemma Stable_Constrains_Un: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   273
    "[| F \<in> Stable(C); F \<in> A Co (C \<union> A') |]    
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   274
     ==> F \<in> (C \<union> A) Co (C \<union> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   275
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   276
apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   277
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   278
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   279
lemma Stable_Constrains_Int: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   280
    "[| F \<in> Stable(C); F \<in> (C \<inter> A) Co A' |]    
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   281
     ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   282
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   283
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   284
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   285
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   286
lemma Stable_UN: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   287
    "[| (!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   288
     ==> F \<in> Stable (\<Union>i \<in> I. A(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   289
apply (simp add: Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   290
apply (blast intro: Constrains_UN)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   291
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   292
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   293
lemma Stable_INT: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   294
    "[|(!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   295
     ==> F \<in> Stable (\<Inter>i \<in> I. A(i))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   296
apply (simp add: Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   297
apply (blast intro: Constrains_INT)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   298
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   299
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   300
lemma Stable_reachable: "F \<in> program ==>F \<in> Stable (reachable(F))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   301
apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   302
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   303
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   304
lemma Stable_type: "Stable(A) \<subseteq> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   305
apply (unfold Stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   306
apply (rule Constrains_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   307
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   308
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   309
(*** The Elimination Theorem.  The "free" m has become universally quantified!
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   310
     Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   311
     in forward proof. ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   312
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   313
lemma Elimination: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   314
    "[| \<forall>m \<in> M. F \<in> ({s \<in> A. x(s) = m}) Co (B(m)); F \<in> program |]  
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   315
     ==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> M. B(m))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   316
apply (unfold Constrains_def, auto)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   317
apply (rule_tac A1 = "reachable (F) \<inter> A" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
   318
        in UNITY.elimination [THEN constrains_weaken_L])
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   319
apply (auto intro: constrains_weaken_L)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   320
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   321
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   322
(* As above, but for the special case of A=state *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   323
lemma Elimination2: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   324
 "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} Co B(m); F \<in> program |]  
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   325
     ==> F \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   326
apply (blast intro: Elimination)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   327
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   328
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   329
(** Unless **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   330
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   331
lemma Unless_type: "A Unless B <=program"
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   332
apply (unfold op_Unless_def)
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   333
apply (rule Constrains_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   334
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   335
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   336
(*** Specialized laws for handling Always ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   337
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   338
(** Natural deduction rules for "Always A" **)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   339
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   340
lemma AlwaysI: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   341
"[| Init(F)<=A;  F \<in> Stable(A) |] ==> F \<in> Always(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   342
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   343
apply (unfold Always_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   344
apply (frule Stable_type [THEN subsetD], auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   345
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   346
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   347
lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   348
by (simp add: Always_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   349
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 45294
diff changeset
   350
lemmas AlwaysE = AlwaysD [THEN conjE]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 45294
diff changeset
   351
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   352
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   353
(*The set of all reachable states is Always*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   354
lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) \<subseteq> A"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   355
apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   356
apply (rule subsetI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   357
apply (erule reachable.induct)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   358
apply (blast intro: reachable.intros)+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   359
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   360
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   361
lemma invariant_imp_Always: 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   362
     "F \<in> invariant(A) ==> F \<in> Always(A)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   363
apply (unfold Always_def invariant_def Stable_def stable_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   364
apply (blast intro: constrains_imp_Constrains)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   365
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   366
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 45294
diff changeset
   367
lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   368
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   369
lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) \<inter> A)}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   370
apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   371
apply (rule equalityI, auto) 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   372
apply (blast intro: reachable.intros reachable_type)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   373
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   374
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   375
(*the RHS is the traditional definition of the "always" operator*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   376
lemma Always_eq_includes_reachable: "Always(A) = {F \<in> program. reachable(F) \<subseteq> A}"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   377
apply (rule equalityI, safe)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   378
apply (auto dest: invariant_includes_reachable 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   379
   simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   380
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   381
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   382
lemma Always_type: "Always(A) \<subseteq> program"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   383
by (unfold Always_def initially_def, auto)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   384
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   385
lemma Always_state_eq: "Always(state) = program"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   386
apply (rule equalityI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   387
apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   388
            simp add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   389
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   390
declare Always_state_eq [simp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   391
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   392
lemma state_AlwaysI: "F \<in> program ==> F \<in> Always(state)"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   393
by (auto dest: reachable_type [THEN subsetD]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   394
            simp add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   395
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   396
lemma Always_eq_UN_invariant: "st_set(A) ==> Always(A) = (\<Union>I \<in> Pow(A). invariant(I))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   397
apply (simp (no_asm) add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   398
apply (rule equalityI, auto) 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   399
apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable] 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
   400
                    rev_subsetD [OF _ invariant_includes_reachable]  
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   401
             dest: invariant_type [THEN subsetD])+
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   402
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   403
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   404
lemma Always_weaken: "[| F \<in> Always(A); A \<subseteq> B |] ==> F \<in> Always(B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   405
by (auto simp add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   406
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   407
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   408
(*** "Co" rules involving Always ***)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   409
lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp]
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   410
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   411
lemma Always_Constrains_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) Co A') \<longleftrightarrow> (F \<in> A Co A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   412
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   413
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   414
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   415
lemma Always_Constrains_post: "F \<in> Always(I) ==> (F \<in> A Co (I \<inter> A')) \<longleftrightarrow>(F \<in> A Co A')"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   416
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   417
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   418
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   419
lemma Always_ConstrainsI: "[| F \<in> Always(I);  F \<in> (I \<inter> A) Co A' |] ==> F \<in> A Co A'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   420
by (blast intro: Always_Constrains_pre [THEN iffD1])
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   421
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   422
(* [| F \<in> Always(I);  F \<in> A Co A' |] ==> F \<in> A Co (I \<inter> A') *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 45294
diff changeset
   423
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   424
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   425
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   426
lemma Always_Constrains_weaken: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   427
"[|F \<in> Always(C); F \<in> A Co A'; C \<inter> B<=A; C \<inter> A'<=B'|]==>F \<in> B Co B'"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   428
apply (rule Always_ConstrainsI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   429
apply (drule_tac [2] Always_ConstrainsD, simp_all) 
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   430
apply (blast intro: Constrains_weaken)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   431
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   432
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   433
(** Conjoining Always properties **)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   434
lemma Always_Int_distrib: "Always(A \<inter> B) = Always(A) \<inter> Always(B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   435
by (auto simp add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   436
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   437
(* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   438
lemma Always_INT_distrib: "i \<in> I==>Always(\<Inter>i \<in> I. A(i)) = (\<Inter>i \<in> I. Always(A(i)))"
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   439
apply (rule equalityI)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   440
apply (auto simp add: Inter_iff Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   441
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   442
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   443
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   444
lemma Always_Int_I: "[| F \<in> Always(A);  F \<in> Always(B) |] ==> F \<in> Always(A \<inter> B)"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   445
apply (simp (no_asm_simp) add: Always_Int_distrib)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   446
done
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   447
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   448
(*Allows a kind of "implication introduction"*)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   449
lemma Always_Diff_Un_eq: "[| F \<in> Always(A) |] ==> (F \<in> Always(C-A \<union> B)) \<longleftrightarrow> (F \<in> Always(B))"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   450
by (auto simp add: Always_eq_includes_reachable)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   451
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   452
(*Delete the nearest invariance assumption (which will be the second one
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   453
  used by Always_Int_I) *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 45294
diff changeset
   454
lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   455
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   456
ML
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   457
{*
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   458
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   459
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin};
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   460
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   461
(*Combines a list of invariance THEOREMS into one.*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   462
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   463
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   464
(*To allow expansion of the program's definition when appropriate*)
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   465
structure Program_Defs = Named_Thms
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   466
(
45294
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 42793
diff changeset
   467
  val name = @{binding program}
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   468
  val description = "program definitions"
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   469
);
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   470
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   471
(*proves "co" properties when the program is specified*)
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   472
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23543
diff changeset
   473
fun constrains_tac ctxt =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   474
  let val ss = simpset_of ctxt in
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   475
   SELECT_GOAL
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   476
      (EVERY [REPEAT (Always_Int_tac 1),
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   477
              REPEAT (etac @{thm Always_ConstrainsI} 1
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   478
                      ORELSE
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   479
                      resolve_tac [@{thm StableI}, @{thm stableI},
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   480
                                   @{thm constrains_imp_Constrains}] 1),
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   481
              rtac @{thm constrainsI} 1,
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   482
              (* Three subgoals *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24051
diff changeset
   483
              rewrite_goal_tac [@{thm st_set_def}] 3,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   484
              REPEAT (force_tac ctxt 2),
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   485
              full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   486
              ALLGOALS (clarify_tac ctxt),
35409
5c5bb83f2bae more antiquotations;
wenzelm
parents: 32960
diff changeset
   487
              REPEAT (FIRSTGOAL (etac @{thm disjE})),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   488
              ALLGOALS (clarify_tac ctxt),
35409
5c5bb83f2bae more antiquotations;
wenzelm
parents: 32960
diff changeset
   489
              REPEAT (FIRSTGOAL (etac @{thm disjE})),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   490
              ALLGOALS (clarify_tac ctxt),
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   491
              ALLGOALS (asm_full_simp_tac ss),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   492
              ALLGOALS (clarify_tac ctxt)])
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23543
diff changeset
   493
  end;
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   494
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   495
(*For proving invariants*)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   496
fun always_tac ctxt i =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35409
diff changeset
   497
    rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   498
*}
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   499
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30549
diff changeset
   500
setup Program_Defs.setup
24051
896fb015079c replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents: 23894
diff changeset
   501
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   502
method_setup safety = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   503
  Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 16183
diff changeset
   504
  "for proving safety properties"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   505
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23543
diff changeset
   506
method_setup always = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   507
  Scan.succeed (SIMPLE_METHOD' o always_tac) *}
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23543
diff changeset
   508
  "for proving invariants"
15634
bca33c49b083 conversion of UNITY to Isar scripts
paulson
parents: 14046
diff changeset
   509
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   510
end