# HG changeset patch
# User paulson
# Date 1056989751 -7200
# Node ID ccb48f3239f7394937bf72ee62f5ff7257ea30c6
# Parent  aed5d25c4a0cbd4b2a7a36ed189b0efa4738d3f6
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
Conversion of UNITY/State to Isar format.;

diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/IsaMakefile	Mon Jun 30 18:15:51 2003 +0200
@@ -117,9 +117,9 @@
 $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
   UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
   UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
-  UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
+  UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.thy \
   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy \
-  UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
+  UNITY/Union.ML UNITY/Union.thy \
   UNITY/AllocBase.thy UNITY/AllocImpl.thy\
   UNITY/ClientImpl.thy UNITY/Distributor.thy\
   UNITY/Follows.ML UNITY/Follows.thy\
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.thy	Mon Jun 30 18:15:51 2003 +0200
@@ -187,8 +187,11 @@
 
 lemma mem_Int_imp_lt_length:
      "[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
-apply (simp add: ltI)
-done
+by (simp add: ltI)
+
+lemma Int_succ_right:
+     "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)"
+by auto
 
 
 lemma bag_of_sublist_lemma:
@@ -349,18 +352,6 @@
 apply (rule var_infinite_lemma)
 done
 
-(*Surely a simpler proof uses lepoll_Finite and the following lemma:*)
-
-    (*????Cardinal*)
-    lemma nat_not_Finite: "~Finite(nat)"
-    apply (unfold Finite_def, clarify) 
-    apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) 
-    apply (insert Card_nat) 
-    apply (simp add: Card_def)
-    apply (drule le_imp_subset)
-    apply (blast elim: mem_irrefl)
-    done
-
 lemma var_not_Finite: "~Finite(var)"
 apply (insert nat_not_Finite) 
 apply (blast intro: lepoll_Finite [OF 	nat_lepoll_var]) 
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Mon Jun 30 18:15:51 2003 +0200
@@ -9,7 +9,7 @@
 
 theory ClientImpl = AllocBase + Guar:
 
-(*????MOVE UP*)
+(*move to Constrains.thy when the latter is converted to Isar format*)
 method_setup constrains = {*
     Method.ctxt_args (fn ctxt =>
         Method.METHOD (fn facts =>
@@ -17,13 +17,6 @@
                                Simplifier.get_local_simpset ctxt) 1)) *}
     "for proving safety properties"
 
-(*For using "disjunction" (union over an index set) to eliminate a variable.
-  ????move way up*)
-lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
-      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
-by blast
-
-
 consts
   ask :: i (* input history:  tokens requested *)
   giv :: i (* output history: tokens granted *)
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/State.ML
--- a/src/ZF/UNITY/State.ML	Mon Jun 30 12:23:00 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-(*  Title:      HOL/UNITY/State.ML
-    ID:         $Id$
-    Author:     Sidi O Ehmety, Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-Formalizes UNITY-program states.
-*)
-Goalw [state_def, st0_def] "st0:state";
-by Auto_tac;
-qed "st0_in_state";
-Addsimps [st0_in_state];
-AddTCs [st0_in_state];
-
-Goalw [st_set_def] "st_set({x:state. P(x)})";
-by Auto_tac;
-qed "st_set_Collect";
-AddIffs [st_set_Collect];
-
-Goalw [st_set_def] "st_set(0)";
-by (Simp_tac 1);
-qed "st_set_0";
-AddIffs [st_set_0];
-
-Goalw [st_set_def] "st_set(state)";
-by (Simp_tac 1);
-qed "st_set_state";
-AddIffs [st_set_state];
-
-(* Union *)
-
-Goalw [st_set_def] 
-"st_set(A Un B) <-> st_set(A) & st_set(B)";
-by Auto_tac;
-qed "st_set_Un_iff";
-AddIffs [st_set_Un_iff];
-
-Goalw [st_set_def] 
-"st_set(Union(S)) <-> (ALL A:S. st_set(A))";
-by Auto_tac;
-qed "st_set_Union_iff";
-AddIffs [st_set_Union_iff];
-
-(* Intersection *)
-
-Goalw [st_set_def] 
-"st_set(A) | st_set(B) ==> st_set(A Int B)";
-by Auto_tac;
-qed "st_set_Int";
-AddSIs [st_set_Int];
-
-Goalw [st_set_def, Inter_def]
-   "(S=0) | (EX A:S. st_set(A)) ==> st_set(Inter(S))";
-by Auto_tac;
-qed "st_set_Inter";
-AddSIs [st_set_Inter];
-
-(* Diff *)
-Goalw [st_set_def]
-"st_set(A) ==> st_set(A - B)";
-by Auto_tac;
-qed "st_set_DiffI";
-AddSIs [st_set_DiffI];
-
-Goal "{s:state. P(s)} Int state = {s:state. P(s)}";
-by Auto_tac;
-qed "Collect_Int_state";
-
-Goal "state Int {s:state. P(s)} = {s:state. P(s)}";
-by Auto_tac;
-qed "state_Int_Collect";
-AddIffs [Collect_Int_state, state_Int_Collect];
-
-(* Introduction and destruction rules for st_set *)
-
-Goalw [st_set_def]
- "A <= state ==> st_set(A)";
-by (assume_tac 1);
-qed "st_setI";
-
-Goalw [st_set_def]
- "st_set(A) ==> A<=state";
-by (assume_tac 1);
-qed "st_setD";
-
-Goalw [st_set_def]
-"[| st_set(A); B<=A |] ==> st_set(B)";
-by Auto_tac;
-qed "st_set_subset";
-
-
-Goalw [state_def]
-"[| s:state; x:var; y:type_of(x) |] ==> s(x:=y):state";
-by (blast_tac (claset() addIs [update_type]) 1);
-qed "state_update_type";
-
-Goalw [st_compl_def] "st_set(st_compl(A))";
-by Auto_tac;
-qed "st_set_compl";
-Addsimps [st_set_compl];
-
-Goalw [st_compl_def] "x:st_compl(A) <-> x:state & x ~:A";
-by Auto_tac;
-qed "st_compl_iff";
-Addsimps [st_compl_iff];
-
-Goalw [st_compl_def] "st_compl({s:state. P(s)}) = {s:state. ~P(s)}";
-by Auto_tac;
-qed "st_compl_Collect";
-Addsimps [st_compl_Collect];
-
-
-
-
-
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/UNITY/State.thy	Mon Jun 30 18:15:51 2003 +0200
@@ -9,27 +9,132 @@
  - variables can be quantified over.
 *)
 
-State = UNITYMisc +
+header{*UNITY Program States*}
+
+theory State = Main:
 
-consts var::i
-datatype var = Var("i:list(nat)")
-         type_intrs "[list_nat_into_univ]"
+consts var :: i
+datatype var = Var("i \<in> list(nat)")
+  type_intros  nat_subset_univ [THEN list_subset_univ, THEN subsetD]
+
 consts
-  type_of :: i=>i
-  default_val :: i=>i
+  type_of :: "i=>i"
+  default_val :: "i=>i"
 
 constdefs
   state   :: i
-  "state == PROD x:var. cons(default_val(x), type_of(x))"
+   "state == \<Pi>x \<in> var. cons(default_val(x), type_of(x))"
+
   st0     :: i
-  "st0 == lam x:var. default_val(x)"
+   "st0 == \<lambda>x \<in> var. default_val(x)"
   
-  st_set  :: i =>o
+  st_set  :: "i=>o"
 (* To prevent typing conditions like `A<=state' from
    being used in combination with the rules `constrains_weaken', etc. *)
   "st_set(A) == A<=state"
 
-  st_compl :: i=>i
+  st_compl :: "i=>i"
   "st_compl(A) == state-A"
-  
-end
\ No newline at end of file
+
+
+lemma st0_in_state [simp,TC]: "st0 \<in> state"
+by (simp add: state_def st0_def)
+
+lemma st_set_Collect [iff]: "st_set({x \<in> state. P(x)})"
+by (simp add: st_set_def, auto)
+
+lemma st_set_0 [iff]: "st_set(0)"
+by (simp add: st_set_def)
+
+lemma st_set_state [iff]: "st_set(state)"
+by (simp add: st_set_def)
+
+(* Union *)
+
+lemma st_set_Un_iff [iff]: "st_set(A Un B) <-> st_set(A) & st_set(B)"
+by (simp add: st_set_def, auto)
+
+lemma st_set_Union_iff [iff]: "st_set(Union(S)) <-> (\<forall>A \<in> S. st_set(A))"
+by (simp add: st_set_def, auto)
+
+(* Intersection *)
+
+lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A Int B)"
+by (simp add: st_set_def, auto)
+
+lemma st_set_Inter [intro!]: 
+   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(Inter(S))"
+apply (simp add: st_set_def Inter_def, auto)
+done
+
+(* Diff *)
+lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"
+by (simp add: st_set_def, auto)
+
+lemma Collect_Int_state [simp]: "Collect(state,P) Int state = Collect(state,P)"
+by auto
+
+lemma state_Int_Collect [simp]: "state Int Collect(state,P) = Collect(state,P)"
+by auto
+
+
+(* Introduction and destruction rules for st_set *)
+
+lemma st_setI: "A <= state ==> st_set(A)"
+by (simp add: st_set_def)
+
+lemma st_setD: "st_set(A) ==> A<=state"
+by (simp add: st_set_def)
+
+lemma st_set_subset: "[| st_set(A); B<=A |] ==> st_set(B)"
+by (simp add: st_set_def, auto)
+
+
+lemma state_update_type: 
+     "[| s \<in> state; x \<in> var; y \<in> type_of(x) |] ==> s(x:=y):state"
+apply (simp add: state_def)
+apply (blast intro: update_type)
+done
+
+lemma st_set_compl [simp]: "st_set(st_compl(A))"
+by (simp add: st_compl_def, auto)
+
+lemma st_compl_iff [simp]: "x \<in> st_compl(A) <-> x \<in> state & x \<notin> A"
+by (simp add: st_compl_def)
+
+lemma st_compl_Collect [simp]:
+     "st_compl({s \<in> state. P(s)}) = {s \<in> state. ~P(s)}"
+by (simp add: st_compl_def, auto)
+
+(*For using "disjunction" (union over an index set) to eliminate a variable.*)
+lemma UN_conj_eq:
+     "\<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)}"
+by blast
+
+
+ML
+{*
+val st_set_def = thm "st_set_def";
+val state_def = thm "state_def";
+
+val st0_in_state = thm "st0_in_state";
+val st_set_Collect = thm "st_set_Collect";
+val st_set_0 = thm "st_set_0";
+val st_set_state = thm "st_set_state";
+val st_set_Un_iff = thm "st_set_Un_iff";
+val st_set_Union_iff = thm "st_set_Union_iff";
+val st_set_Int = thm "st_set_Int";
+val st_set_Inter = thm "st_set_Inter";
+val st_set_DiffI = thm "st_set_DiffI";
+val Collect_Int_state = thm "Collect_Int_state";
+val state_Int_Collect = thm "state_Int_Collect";
+val st_setI = thm "st_setI";
+val st_setD = thm "st_setD";
+val st_set_subset = thm "st_set_subset";
+val state_update_type = thm "state_update_type";
+val st_set_compl = thm "st_set_compl";
+val st_compl_iff = thm "st_compl_iff";
+val st_compl_Collect = thm "st_compl_Collect";
+*}
+
+end
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/UNITYMisc.ML
--- a/src/ZF/UNITY/UNITYMisc.ML	Mon Jun 30 12:23:00 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(*  Title:      HOL/UNITY/UNITYMisc.ML
-    ID:         $Id$
-    Author:     Sidi O Ehmety, Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-Some miscellaneous and add-hoc set theory concepts.
-
-*)
-
-(** Ad-hoc set-theory rules **)
-
-Goal "Union(B) Int A = (UN b:B. b Int A)";
-by Auto_tac;
-qed "Int_Union_Union";
-
-Goal "A Int Union(B) = (UN b:B. A Int b)";
-by Auto_tac;
-qed "Int_Union_Union2";
-
-
-(** Needed in State theory for the current definition of variables 
-where they are indexed by lists  **)
-
-Goal "i:list(nat) ==> i:univ(0)";
-by (dres_inst_tac [("B", "0")] list_into_univ 1);
-by (blast_tac (claset() addIs [nat_into_univ]) 1);
-by (assume_tac 1);
-qed "list_nat_into_univ";
-
-
-(** Simplication rules for Collect **)
-
-(*Currently unused*)
-Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}";
-by Auto_tac;
-qed "Collect_Int_left";
-
-(*Currently unused*)
-Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}";
-by Auto_tac;
-qed "Collect_Int_right";
-
-Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
-by Auto_tac;
-qed "Collect_disj_eq";
-
-Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)";
-by Auto_tac;
-qed "Collect_conj_eq";
-
-Goal "Union(B) Int A = (UN C:B. C Int A)"; 
-by (Blast_tac 1);
-qed "Int_Union2";
-
-Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
-by Auto_tac;
-qed "Int_succ_right";
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/UNITYMisc.thy
--- a/src/ZF/UNITY/UNITYMisc.thy	Mon Jun 30 12:23:00 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      HOL/UNITY/UNITYMisc.thy
-    ID:         $Id$
-    Author:     Sidi O Ehmety, Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-Some miscellaneous and add-hoc set theory concepts.
-*)
-
-
-
-UNITYMisc = Main
\ No newline at end of file
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/UNITY/WFair.ML
--- a/src/ZF/UNITY/WFair.ML	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML	Mon Jun 30 18:15:51 2003 +0200
@@ -8,6 +8,16 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
+(** Ad-hoc set-theory rules **)
+
+Goal "Union(B) Int A = (UN b:B. b Int A)";
+by Auto_tac;
+qed "Int_Union_Union";
+
+Goal "A Int Union(B) = (UN b:B. A Int b)";
+by Auto_tac;
+qed "Int_Union_Union2";
+
 (*** transient ***)
 
 Goalw [transient_def] "transient(A)<=program";
diff -r aed5d25c4a0c -r ccb48f3239f7 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/equalities.thy	Mon Jun 30 18:15:51 2003 +0200
@@ -12,41 +12,9 @@
 text{*These cover union, intersection, converse, domain, range, etc.  Philippe
 de Groote proved many of the inclusions.*}
 
-(*FIXME: move to ZF.thy or even to FOL.thy??*)
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
-
-(*FIXME: move to ZF.thy or even to FOL.thy??*)
-lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
-by blast
-
-(** Monotonicity of implications -- some could go to FOL **)
-
 lemma in_mono: "A<=B ==> x:A --> x:B"
 by blast
 
-lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma imp_refl: "P-->P"
-by (rule impI, assumption)
-
-(*The quantifier monotonicity rules are also intuitionistically valid*)
-lemma ex_mono:
-    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"
-by blast
-
-lemma all_mono:
-    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"
-by blast
-
-
 lemma the_eq_0 [simp]: "(THE x. False) = 0"
 by (blast intro: the_0)
 
@@ -404,6 +372,9 @@
 lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
 by blast
 
+lemma Int_Union2: "Union(B) Int A = (UN C:B. C Int A)"
+by blast
+
 (** Big Intersection is the greatest lower bound of a nonempty set **)
 
 lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
@@ -978,6 +949,18 @@
      "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
 by blast
 
+lemma Collect_Int_left: "{x:A. P(x)} Int B = {x : A Int B. P(x)}"
+by blast
+
+lemma Collect_Int_right: "A Int {x:B. P(x)} = {x : A Int B. P(x)}"
+by blast
+
+lemma Collect_disj_eq: "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
+by blast
+
+lemma Collect_conj_eq: "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
+by blast
+
 lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
                     Union_least UN_least Un_least 
                     Inter_greatest Int_greatest RepFun_subset
@@ -1139,6 +1122,7 @@
 val Union_Int_subset = thm "Union_Int_subset";
 val Union_disjoint = thm "Union_disjoint";
 val Union_empty_iff = thm "Union_empty_iff";
+val Int_Union2 = thm "Int_Union2";
 val Inter_0 = thm "Inter_0";
 val Inter_Un_subset = thm "Inter_Un_subset";
 val Inter_Un_distrib = thm "Inter_Un_distrib";
@@ -1246,6 +1230,8 @@
 val Int_Collect_self_eq = thm "Int_Collect_self_eq";
 val Collect_Collect_eq = thm "Collect_Collect_eq";
 val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
+val Collect_disj_eq = thm "Collect_disj_eq";
+val Collect_conj_eq = thm "Collect_conj_eq";
 
 val Int_ac = thms "Int_ac";
 val Un_ac = thms "Un_ac";