--- a/src/ZF/IsaMakefile Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/IsaMakefile Thu Jun 26 15:48:33 2003 +0200
@@ -123,8 +123,7 @@
UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
UNITY/ClientImpl.thy UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
- UNITY/Increasing.ML UNITY/Increasing.thy\
- UNITY/Merge.ML UNITY/Merge.thy\
+ UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
UNITY/WFair.ML UNITY/WFair.thy
--- a/src/ZF/UNITY/AllocBase.ML Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.ML Thu Jun 26 15:48:33 2003 +0200
@@ -90,6 +90,7 @@
qed "tokens_append";
Addsimps [tokens_append];
+(*????????????????List.thy*)
Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
by (induct_tac "l" 1);
by Safe_tac;
--- a/src/ZF/UNITY/Merge.ML Wed Jun 25 13:17:26 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-(* Title: ZF/UNITY/Merge
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2002 University of Cambridge
-
-A multiple-client allocator from a single-client allocator:
-Merge specification
-*)
-Open_locale "Merge";
-val all_distinct_vars = thm "all_distinct_vars";
-val var_assumes = thm "var_assumes";
-val type_assumes = thm "type_assumes";
-val default_val_assumes = thm "default_val_assumes";
-
-Addsimps [var_assumes, default_val_assumes, type_assumes];
-
-Goalw [state_def]
-"s \\<in> state ==> s`In(n):list(A)";
-by (dres_inst_tac [("a", "In(n)")] apply_type 1);
-by Auto_tac;
-qed "In_value_type";
-AddTCs [In_value_type];
-Addsimps [In_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`Out \\<in> list(A)";
-by (dres_inst_tac [("a", "Out")] apply_type 1);
-by Auto_tac;
-qed "Out_value_type";
-AddTCs [Out_value_type];
-Addsimps [Out_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`iOut \\<in> list(nat)";
-by (dres_inst_tac [("a", "iOut")] apply_type 1);
-by Auto_tac;
-qed "Out_value_type";
-AddTCs [Out_value_type];
-Addsimps [Out_value_type];
-
-
-val merge = thm "merge_spec";
-
-Goal "M \\<in> program";
-by (cut_facts_tac [merge] 1);
-by (auto_tac (claset() addDs [guarantees_type RS subsetD],
- simpset() addsimps [merge_spec_def, merge_increasing_def]));
-qed "M_in_program";
-Addsimps [M_in_program];
-AddTCs [M_in_program];
-
-Goal
-"Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))";
-by (cut_facts_tac [merge, inst "v" "lift(Out)" preserves_type] 1);
-by (auto_tac (claset(), simpset() addsimps
- [merge_spec_def, merge_allowed_acts_def,
- Allowed_def, safety_prop_Acts_iff]));
-qed "merge_Allowed";
-
-Goal
-"G \\<in> program ==> \
-\ M ok G <-> (G \\<in> preserves(lift(Out)) & \
-\ G \\<in> preserves(lift(iOut)) & M \\<in> Allowed(G))";
-by (cut_facts_tac [merge] 1);
-by (auto_tac (claset(), simpset()
- addsimps [merge_Allowed, ok_iff_Allowed]));
-qed "M_ok_iff";
-
-Goal
-"[| G \\<in> preserves(lift(Out)); G \\<in> preserves(lift(iOut)); \
-\ M \\<in> Allowed(G) |] ==> \
-\ M Join G \\<in> Always({s \\<in> state. length(s`Out)=length(s`iOut)})";
-by (ftac (preserves_type RS subsetD) 1);
-by (subgoal_tac "G \\<in> program" 1);
-by (assume_tac 2);
-by (ftac M_ok_iff 1);
-by (cut_facts_tac [merge] 1);
-by (force_tac (claset() addDs [guaranteesD],
- simpset() addsimps [merge_spec_def, merge_eq_Out_def]) 1);
-qed "merge_Always_Out_eq_iOut";
-
-Goal
-"[| G \\<in> preserves(lift(iOut)); G \\<in> preserves(lift(Out)); \
-\ M \\<in> Allowed(G) |] ==> \
-\ M Join G: Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})";
-by (ftac (preserves_type RS subsetD) 1);
-by (ftac M_ok_iff 1);
-by (cut_facts_tac [merge] 1);
-by (force_tac (claset() addDs [guaranteesD],
- simpset() addsimps [merge_spec_def, merge_bounded_def]) 1);
-qed "merge_Bounded";
-
-Goal
-"[| G \\<in> preserves(lift(iOut)); \
-\ G: preserves(lift(Out)); M \\<in> Allowed(G) |] \
-\ ==> M Join G : Always \
-\ ({s \\<in> state. msetsum(%i. bag_of(sublist(s`Out, \
-\ {k \\<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
-\ Nclients, A) = bag_of(s`Out)})";
-by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
- state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
-;
-by Auto_tac;
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
-by (auto_tac (claset(), simpset()
- addsimps [nat_into_Finite, set_of_list_conv_nth]));
-by (subgoal_tac
- "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
-by Auto_tac;
-by (resolve_tac [equalityI] 1);
-by (blast_tac (claset() addDs [ltD]) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "length(x ` iOut) : nat" 1);
-by (Asm_full_simp_tac 2);
-by (subgoal_tac "xa : nat" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt])));
-by (blast_tac (claset() addIs [lt_trans]) 2);
-by (dres_inst_tac [("x", "nth(xa, x`iOut)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
-by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1);
-by (blast_tac (claset() addDs [ltD]) 1);
-qed "merge_bag_Follows_lemma";
-
-Goal
-"M : (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
-\ guarantees \
-\ (%s. bag_of(s`Out)) Fols \
-\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
-by (cut_facts_tac [merge] 1);
-by (rtac (merge_bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
-by (ALLGOALS(rotate_tac ~1 ));
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [M_ok_iff])));
-by Auto_tac;
-by (rtac Follows_state_ofD1 1);
-by (rtac Follows_msetsum_UN 1);
-by (ALLGOALS(Clarify_tac));
-by (resolve_tac [conjI] 2);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 2);
-by (resolve_tac [conjI] 3);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 3);
-by (resolve_tac [conjI] 4);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 4);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 5);
-by (ALLGOALS(Asm_simp_tac));
-by (resolve_tac [nat_into_Finite] 2);
-by (Asm_simp_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [INT_iff,
- merge_spec_def, merge_follows_def]) 1);
-by Auto_tac;
-by (cut_facts_tac [merge] 1);
-by (subgoal_tac "M ok G" 1);
-by (dtac guaranteesD 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs[M_ok_iff RS iffD2], simpset()) 4);
-by (rewrite_goal_tac [merge_spec_def, merge_follows_def] 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD),
- refl_prefix, trans_on_MultLe]
- addcongs [Follows_cong]) 1);
-qed "merge_bag_Follows";
-Close_locale "Merge";
-
--- a/src/ZF/UNITY/Merge.thy Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy Thu Jun 26 15:48:33 2003 +0200
@@ -7,72 +7,194 @@
Merge specification
*)
-Merge = AllocBase + Follows + Guar + GenPrefix +
+theory Merge = AllocBase + Follows + Guar + GenPrefix:
+
(** Merge specification (the number of inputs is Nclients) ***)
(** Parameter A represents the type of items to Merge **)
+
constdefs
(*spec (10)*)
- merge_increasing :: [i, i, i] =>i
+ merge_increasing :: "[i, i, i] =>i"
"merge_increasing(A, Out, iOut) == program guarantees
(lift(Out) IncreasingWrt prefix(A)/list(A)) Int
(lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
(*spec (11)*)
- merge_eq_Out :: [i, i] =>i
+ merge_eq_Out :: "[i, i] =>i"
"merge_eq_Out(Out, iOut) == program guarantees
- Always({s \\<in> state. length(s`Out) = length(s`iOut)})"
+ Always({s \<in> state. length(s`Out) = length(s`iOut)})"
(*spec (12)*)
- merge_bounded :: i=>i
+ merge_bounded :: "i=>i"
"merge_bounded(iOut) == program guarantees
- Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})"
+ Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
(*spec (13)*)
(* Parameter A represents the type of tokens *)
- merge_follows :: [i, i=>i, i, i] =>i
+ merge_follows :: "[i, i=>i, i, i] =>i"
"merge_follows(A, In, Out, iOut) ==
- (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+ (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
guarantees
- (\\<Inter>n \\<in> Nclients.
- (%s. sublist(s`Out, {k \\<in> nat. k < length(s`iOut) &
+ (\<Inter>n \<in> Nclients.
+ (%s. sublist(s`Out, {k \<in> nat. k < length(s`iOut) &
nth(k, s`iOut) = n})) Fols lift(In(n))
Wrt prefix(A)/list(A))"
(*spec: preserves part*)
- merge_preserves :: [i=>i] =>i
- "merge_preserves(In) == \\<Inter>n \\<in> nat. preserves(lift(In(n)))"
+ merge_preserves :: "[i=>i] =>i"
+ "merge_preserves(In) == \<Inter>n \<in> nat. preserves(lift(In(n)))"
(* environmental constraints*)
- merge_allowed_acts :: [i, i] =>i
+ merge_allowed_acts :: "[i, i] =>i"
"merge_allowed_acts(Out, iOut) ==
- {F \\<in> program. AllowedActs(F) =
- cons(id(state), (\\<Union>G \\<in> preserves(lift(Out)) \\<inter>
+ {F \<in> program. AllowedActs(F) =
+ cons(id(state), (\<Union>G \<in> preserves(lift(Out)) \<inter>
preserves(lift(iOut)). Acts(G)))}"
- merge_spec :: [i, i =>i, i, i]=>i
+ merge_spec :: "[i, i =>i, i, i]=>i"
"merge_spec(A, In, Out, iOut) ==
- merge_increasing(A, Out, iOut) \\<inter> merge_eq_Out(Out, iOut) \\<inter>
- merge_bounded(iOut) \\<inter> merge_follows(A, In, Out, iOut)
- \\<inter> merge_allowed_acts(Out, iOut) \\<inter> merge_preserves(In)"
+ merge_increasing(A, Out, iOut) \<inter> merge_eq_Out(Out, iOut) \<inter>
+ merge_bounded(iOut) \<inter> merge_follows(A, In, Out, iOut)
+ \<inter> merge_allowed_acts(Out, iOut) \<inter> merge_preserves(In)"
(** State definitions. OUTPUT variables are locals **)
-locale Merge =
- fixes In :: i=>i (*merge's INPUT histories: streams to merge*)
- Out :: i (*merge's OUTPUT history: merged items*)
- iOut :: i (*merge's OUTPUT history: origins of merged items*)
- A :: i (*the type of items being merged *)
- M :: i
- assumes
- var_assumes "(\\<forall>n. In(n):var) & Out \\<in> var & iOut \\<in> var"
- all_distinct_vars "\\<forall>n. all_distinct([In(n), Out, iOut])"
- type_assumes "(\\<forall>n. type_of(In(n))=list(A))&
- type_of(Out)=list(A) &
- type_of(iOut)=list(nat)"
- default_val_assumes "(\\<forall>n. default_val(In(n))=Nil) &
- default_val(Out)=Nil &
- default_val(iOut)=Nil"
+locale merge =
+ fixes In --{*merge's INPUT histories: streams to merge*}
+ and Out --{*merge's OUTPUT history: merged items*}
+ and iOut --{*merge's OUTPUT history: origins of merged items*}
+ and A --{*the type of items being merged *}
+ and M
+ assumes var_assumes [simp]:
+ "(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
+ and all_distinct_vars:
+ "\<forall>n. all_distinct([In(n), Out, iOut])"
+ and type_assumes [simp]:
+ "(\<forall>n. type_of(In(n))=list(A)) &
+ type_of(Out)=list(A) &
+ type_of(iOut)=list(nat)"
+ and default_val_assumes [simp]:
+ "(\<forall>n. default_val(In(n))=Nil) &
+ default_val(Out)=Nil &
+ default_val(iOut)=Nil"
+ and merge_spec: "M \<in> merge_spec(A, In, Out, iOut)"
+
+
+lemma (in merge) In_value_type [TC,simp]: "s \<in> state ==> s`In(n) \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "In (n)" in apply_type)
+apply auto
+done
+
+lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "Out" in apply_type)
+apply auto
+done
+
+lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = "iOut" in apply_type)
+apply auto
+done
+
+lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
+apply (cut_tac merge_spec)
+apply (auto dest: guarantees_type [THEN subsetD]
+ simp add: merge_spec_def merge_increasing_def)
+done
+
+lemma (in merge) merge_Allowed:
+ "Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))"
+apply (insert merge_spec preserves_type [of "lift (Out)"])
+apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
+done
+
+lemma (in merge) M_ok_iff:
+ "G \<in> program ==>
+ M ok G <-> (G \<in> preserves(lift(Out)) &
+ G \<in> preserves(lift(iOut)) & M \<in> Allowed(G))"
+apply (cut_tac merge_spec)
+apply (auto simp add: merge_Allowed ok_iff_Allowed)
+done
- merge_spec "M \\<in> merge_spec(A, In, Out, iOut)"
+lemma (in merge) merge_Always_Out_eq_iOut:
+ "[| G \<in> preserves(lift(Out)); G \<in> preserves(lift(iOut));
+ M \<in> Allowed(G) |]
+ ==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
+apply (frule preserves_type [THEN subsetD])
+apply (subgoal_tac "G \<in> program")
+ prefer 2 apply (assumption)
+apply (frule M_ok_iff)
+apply (cut_tac merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
+done
+
+lemma (in merge) merge_Bounded:
+ "[| G \<in> preserves(lift(iOut)); G \<in> preserves(lift(Out));
+ M \<in> Allowed(G) |] ==>
+ M \<squnion> G: Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
+apply (frule preserves_type [THEN subsetD])
+apply (frule M_ok_iff)
+apply (cut_tac merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
+done
+
+lemma (in merge) merge_bag_Follows_lemma:
+"[| G \<in> preserves(lift(iOut));
+ G: preserves(lift(Out)); M \<in> Allowed(G) |]
+ ==> M \<squnion> G \<in> Always
+ ({s \<in> state. msetsum(%i. bag_of(sublist(s`Out,
+ {k \<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})),
+ Nclients, A) = bag_of(s`Out)})"
+apply (rule Always_Diff_Un_eq [THEN iffD1])
+apply (rule_tac [2] state_AlwaysI [THEN Always_weaken])
+apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded])
+apply auto
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+apply (auto simp add: nat_into_Finite set_of_list_conv_nth [OF iOut_value_type])
+apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
+apply (auto simp add: sublist_upt_eq_take [OF Out_value_type]
+ length_type [OF iOut_value_type]
+ take_all [OF _ Out_value_type]
+ length_type [OF iOut_value_type])
+apply (rule equalityI)
+apply (blast dest: ltD)
+apply clarify
+apply (subgoal_tac "length (x ` iOut) \<in> nat")
+ prefer 2 apply (simp add: length_type [OF iOut_value_type]);
+apply (subgoal_tac "xa \<in> nat")
+apply (simp_all add: Ord_mem_iff_lt)
+prefer 2 apply (blast intro: lt_trans)
+apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
+apply (simp add: ltI nat_into_Ord)
+apply (blast dest: ltD)
+done
+
+theorem (in merge) merge_bag_Follows:
+ "M \<in> (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+ guarantees
+ (%s. bag_of(s`Out)) Fols
+ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)"
+apply (cut_tac merge_spec)
+apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
+ apply (simp_all add: M_ok_iff)
+apply clarify
+apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
+ apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
+apply (simp add: INT_iff merge_spec_def merge_follows_def)
+apply clarify
+apply (cut_tac merge_spec)
+apply (subgoal_tac "M ok G")
+ prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
+apply (drule guaranteesD)
+apply assumption
+ apply (simp add: merge_spec_def merge_follows_def)
+ apply blast
+apply (simp cong add: Follows_cong
+ add: refl_prefix
+ mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+done
+
end
\ No newline at end of file
--- a/src/ZF/UNITY/Monotonicity.ML Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/Monotonicity.ML Thu Jun 26 15:48:33 2003 +0200
@@ -25,26 +25,7 @@
(** Monotonicity of take **)
-Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
-\ take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]";
-by (induct_tac "xs" 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (etac natE 1);
-by Auto_tac;
-qed_spec_mp "take_succ";
-
-
-Goal "[|xs:list(A); j:nat|] ==> ALL i:nat. i #+ j le length(xs) --> \
-\ take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))";
-by (induct_tac "xs" 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Clarify_tac 1);
-by (eres_inst_tac [("n","i")] natE 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "take_add";
-
+(*????premises too strong*)
Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
by (case_tac "length(xs) le i" 1);
by (subgoal_tac "length(xs) le j" 1);