src/ZF/UNITY/State.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 32960
diff changeset
     1
(*  Title:      ZF/UNITY/State.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
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
     5
Formalizes UNITY-program states using dependent types so that:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
 - variables are typed.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
 - the state space is uniform, common to all defined programs.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     8
 - variables can be quantified over.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     9
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    10
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    11
header{*UNITY Program States*}
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    12
26060
cd89870aa92f imports Main;
wenzelm
parents: 26056
diff changeset
    13
theory State imports Main begin
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    14
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    15
consts var :: i
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    16
datatype var = Var("i \<in> list(nat)")
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    17
  type_intros  nat_subset_univ [THEN list_subset_univ, THEN subsetD]
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    18
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    19
consts
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    20
  type_of :: "i=>i"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    21
  default_val :: "i=>i"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    22
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    24
  "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    26
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    27
  "st0 == \<lambda>x \<in> var. default_val(x)"
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    28
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    29
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    30
  st_set  :: "i=>o"  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    31
(* To prevent typing conditions like `A<=state' from
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    32
   being used in combination with the rules `constrains_weaken', etc. *)
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    33
  "st_set(A) == A<=state"
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    34
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    35
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    36
  st_compl :: "i=>i"  where
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    37
  "st_compl(A) == state-A"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    38
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    39
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    40
lemma st0_in_state [simp,TC]: "st0 \<in> state"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    41
by (simp add: state_def st0_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    42
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    43
lemma st_set_Collect [iff]: "st_set({x \<in> state. P(x)})"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    44
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    45
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    46
lemma st_set_0 [iff]: "st_set(0)"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    47
by (simp add: st_set_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    48
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    49
lemma st_set_state [iff]: "st_set(state)"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    50
by (simp add: st_set_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    51
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    52
(* Union *)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    53
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    54
lemma st_set_Un_iff [iff]: "st_set(A \<union> B) \<longleftrightarrow> st_set(A) & st_set(B)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    55
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    56
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    57
lemma st_set_Union_iff [iff]: "st_set(\<Union>(S)) \<longleftrightarrow> (\<forall>A \<in> S. st_set(A))"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    58
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    59
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    60
(* Intersection *)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    61
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    62
lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A \<inter> B)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    63
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    64
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    65
lemma st_set_Inter [intro!]: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    66
   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(\<Inter>(S))"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    67
apply (simp add: st_set_def Inter_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    68
done
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    69
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    70
(* Diff *)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    71
lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    72
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    73
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    74
lemma Collect_Int_state [simp]: "Collect(state,P) \<inter> state = Collect(state,P)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    75
by auto
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    76
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    77
lemma state_Int_Collect [simp]: "state \<inter> Collect(state,P) = Collect(state,P)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    78
by auto
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    79
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    80
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    81
(* Introduction and destruction rules for st_set *)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    82
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
    83
lemma st_setI: "A \<subseteq> state ==> st_set(A)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    84
by (simp add: st_set_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    85
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    86
lemma st_setD: "st_set(A) ==> A<=state"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    87
by (simp add: st_set_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    88
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    89
lemma st_set_subset: "[| st_set(A); B<=A |] ==> st_set(B)"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    90
by (simp add: st_set_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    91
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    92
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    93
lemma state_update_type: 
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    94
     "[| s \<in> state; x \<in> var; y \<in> type_of(x) |] ==> s(x:=y):state"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    95
apply (simp add: state_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    96
apply (blast intro: update_type)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    97
done
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    98
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
    99
lemma st_set_compl [simp]: "st_set(st_compl(A))"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   100
by (simp add: st_compl_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   101
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 37936
diff changeset
   102
lemma st_compl_iff [simp]: "x \<in> st_compl(A) \<longleftrightarrow> x \<in> state & x \<notin> A"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   103
by (simp add: st_compl_def)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   104
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   105
lemma st_compl_Collect [simp]:
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   106
     "st_compl({s \<in> state. P(s)}) = {s \<in> state. ~P(s)}"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   107
by (simp add: st_compl_def, auto)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   108
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   109
(*For using "disjunction" (union over an index set) to eliminate a variable.*)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   110
lemma UN_conj_eq:
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   111
     "\<forall>d\<in>D. f(d) \<in> A ==> (\<Union>k\<in>A. {d\<in>D. P(d) & f(d) = k}) = {d\<in>D. P(d)}"
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   112
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   113
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14046
diff changeset
   114
end