--- a/src/ZF/Arith.thy Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/Arith.thy Fri Jun 20 12:10:45 2003 +0200
@@ -78,12 +78,12 @@
nat_0_le [simp]
-lemma zero_lt_lemma: "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)"
+lemma zero_lt_lemma: "[| 0<k; k \<in> nat |] ==> \<exists>j\<in>nat. k = succ(j)"
apply (erule rev_mp)
apply (induct_tac "k", auto)
done
-(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
+(* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
@@ -98,21 +98,21 @@
lemma natify_0 [simp]: "natify(0) = 0"
by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
-lemma natify_non_succ: "ALL z. x ~= succ(z) ==> natify(x) = 0"
+lemma natify_non_succ: "\<forall>z. x ~= succ(z) ==> natify(x) = 0"
by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
-lemma natify_in_nat [iff,TC]: "natify(x) : nat"
+lemma natify_in_nat [iff,TC]: "natify(x) \<in> nat"
apply (rule_tac a=x in eps_induct)
-apply (case_tac "EX z. x = succ(z)")
+apply (case_tac "\<exists>z. x = succ(z)")
apply (auto simp add: natify_succ natify_non_succ)
done
-lemma natify_ident [simp]: "n : nat ==> natify(n) = n"
+lemma natify_ident [simp]: "n \<in> nat ==> natify(n) = n"
apply (induct_tac "n")
apply (auto simp add: natify_succ)
done
-lemma natify_eqE: "[|natify(x) = y; x: nat|] ==> x=y"
+lemma natify_eqE: "[|natify(x) = y; x \<in> nat|] ==> x=y"
by auto
@@ -167,29 +167,29 @@
(** Addition **)
-lemma raw_add_type: "[| m:nat; n:nat |] ==> raw_add (m, n) : nat"
+lemma raw_add_type: "[| m\<in>nat; n\<in>nat |] ==> raw_add (m, n) \<in> nat"
by (induct_tac "m", auto)
-lemma add_type [iff,TC]: "m #+ n : nat"
+lemma add_type [iff,TC]: "m #+ n \<in> nat"
by (simp add: add_def raw_add_type)
(** Multiplication **)
-lemma raw_mult_type: "[| m:nat; n:nat |] ==> raw_mult (m, n) : nat"
+lemma raw_mult_type: "[| m\<in>nat; n\<in>nat |] ==> raw_mult (m, n) \<in> nat"
apply (induct_tac "m")
apply (simp_all add: raw_add_type)
done
-lemma mult_type [iff,TC]: "m #* n : nat"
+lemma mult_type [iff,TC]: "m #* n \<in> nat"
by (simp add: mult_def raw_mult_type)
(** Difference **)
-lemma raw_diff_type: "[| m:nat; n:nat |] ==> raw_diff (m, n) : nat"
+lemma raw_diff_type: "[| m\<in>nat; n\<in>nat |] ==> raw_diff (m, n) \<in> nat"
by (induct_tac "n", auto)
-lemma diff_type [iff,TC]: "m #- n : nat"
+lemma diff_type [iff,TC]: "m #- n \<in> nat"
by (simp add: diff_def raw_diff_type)
lemma diff_0_eq_0 [simp]: "0 #- n = 0"
@@ -210,7 +210,7 @@
lemma diff_0 [simp]: "m #- 0 = natify(m)"
by (simp add: diff_def)
-lemma diff_le_self: "m:nat ==> (m #- n) le m"
+lemma diff_le_self: "m\<in>nat ==> (m #- n) le m"
apply (subgoal_tac " (m #- natify (n)) le m")
apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
apply (erule_tac [6] leE)
@@ -227,7 +227,7 @@
lemma add_succ [simp]: "succ(m) #+ n = succ(m #+ n)"
by (simp add: natify_succ add_def)
-lemma add_0: "m: nat ==> 0 #+ m = m"
+lemma add_0: "m \<in> nat ==> 0 #+ m = m"
by simp
(*Associative law for addition*)
@@ -252,7 +252,7 @@
apply (auto simp add: natify_succ)
done
-lemma add_0_right: "m: nat ==> m #+ 0 = m"
+lemma add_0_right: "m \<in> nat ==> m #+ 0 = m"
by auto
(*Commutative law for addition*)
@@ -274,7 +274,7 @@
(*Cancellation law on the left*)
lemma raw_add_left_cancel:
- "[| raw_add(k, m) = raw_add(k, n); k:nat |] ==> m=n"
+ "[| raw_add(k, m) = raw_add(k, n); k\<in>nat |] ==> m=n"
apply (erule rev_mp)
apply (induct_tac "k", auto)
done
@@ -285,7 +285,7 @@
done
lemma add_left_cancel:
- "[| i = j; i #+ m = j #+ n; m:nat; n:nat |] ==> m = n"
+ "[| i = j; i #+ m = j #+ n; m\<in>nat; n\<in>nat |] ==> m = n"
by (force dest!: add_left_cancel_natify)
(*Thanks to Sten Agerholm*)
@@ -295,7 +295,7 @@
apply auto
done
-lemma add_le_elim1: "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n"
+lemma add_le_elim1: "[| k#+m le k#+n; m \<in> nat; n \<in> nat |] ==> m le n"
by (drule add_le_elim1_natify, auto)
lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)"
@@ -304,29 +304,26 @@
apply auto
done
-lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n"
+lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
by (drule add_lt_elim1_natify, auto)
subsection{*Monotonicity of Addition*}
(*strict, in 1st argument; proof is by rule induction on 'less than'.
- Still need j:nat, for consider j = omega. Then we can have i<omega,
- which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
-lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k"
+ Still need j\<in>nat, for consider j = omega. Then we can have i<omega,
+ which is the same as i\<in>nat, but natify(j)=0, so the conclusion fails.*)
+lemma add_lt_mono1: "[| i<j; j\<in>nat |] ==> i#+k < j#+k"
apply (frule lt_nat_in_nat, assumption)
apply (erule succ_lt_induct)
apply (simp_all add: leI)
done
-(*strict, in both arguments*)
-lemma add_lt_mono:
- "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"
-apply (rule add_lt_mono1 [THEN lt_trans], assumption+)
-apply (subst add_commute, subst add_commute, rule add_lt_mono1, assumption+)
-done
+text{*strict, in second argument*}
+lemma add_lt_mono2: "[| i<j; j\<in>nat |] ==> k#+i < k#+j"
+by (simp add: add_commute [of k] add_lt_mono1)
-(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
+text{*A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity*}
lemma Ord_lt_mono_imp_le_mono:
assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
and ford: "!!i. i:k ==> Ord(f(i))"
@@ -337,18 +334,34 @@
apply (blast intro!: leCI lt_mono ford elim!: leE)
done
-(*le monotonicity, 1st argument*)
-lemma add_le_mono1: "[| i le j; j:nat |] ==> i#+k le j#+k"
+text{*@{text "\<le>"} monotonicity, 1st argument*}
+lemma add_le_mono1: "[| i le j; j\<in>nat |] ==> i#+k le j#+k"
apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
done
-(* le monotonicity, BOTH arguments*)
-lemma add_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"
+text{*@{text "\<le>"} monotonicity, both arguments*}
+lemma add_le_mono: "[| i le j; k le l; j\<in>nat; l\<in>nat |] ==> i#+k le j#+l"
apply (rule add_le_mono1 [THEN le_trans], assumption+)
apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
done
+text{*Combinations of less-than and less-than-or-equals*}
+
+lemma add_lt_le_mono: "[| i<j; k\<le>l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
+apply (rule add_lt_mono1 [THEN lt_trans2], assumption+)
+apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
+done
+
+lemma add_le_lt_mono: "[| i\<le>j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
+by (subst add_commute, subst add_commute, erule add_lt_le_mono, assumption+)
+
+text{*Less-than: in other words, strict in both arguments*}
+lemma add_lt_mono: "[| i<j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
+apply (rule add_lt_le_mono)
+apply (auto intro: leI)
+done
+
(** Subtraction is the inverse of addition. **)
lemma diff_add_inverse: "(n#+m) #- n = natify(m)"
@@ -474,10 +487,10 @@
lemma mult_1_right_natify [simp]: "n #* 1 = natify(n)"
by auto
-lemma mult_1: "n : nat ==> 1 #* n = n"
+lemma mult_1: "n \<in> nat ==> 1 #* n = n"
by simp
-lemma mult_1_right: "n : nat ==> n #* 1 = n"
+lemma mult_1_right: "n \<in> nat ==> n #* 1 = n"
by simp
(*Commutative law for multiplication*)
@@ -522,12 +535,12 @@
lemma lt_succ_eq_0_disj:
- "[| m:nat; n:nat |]
- ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))"
+ "[| m\<in>nat; n\<in>nat |]
+ ==> (m < succ(n)) <-> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
by (induct_tac "m", auto)
lemma less_diff_conv [rule_format]:
- "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
+ "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) <-> (i #+ k < j)"
by (erule_tac m = k in diff_induct, auto)
lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
@@ -586,6 +599,7 @@
val add_lt_elim1_natify = thm "add_lt_elim1_natify";
val add_lt_elim1 = thm "add_lt_elim1";
val add_lt_mono1 = thm "add_lt_mono1";
+val add_lt_mono2 = thm "add_lt_mono2";
val add_lt_mono = thm "add_lt_mono";
val Ord_lt_mono_imp_le_mono = thm "Ord_lt_mono_imp_le_mono";
val add_le_mono1 = thm "add_le_mono1";
--- a/src/ZF/ArithSimp.thy Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/ArithSimp.thy Fri Jun 20 12:10:45 2003 +0200
@@ -534,6 +534,34 @@
apply simp_all
done
+text{*Difference and less-than*}
+
+lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i"
+apply (erule rev_mp)
+apply (simp split add: nat_diff_split, auto)
+ apply (blast intro: add_le_self lt_trans1)
+apply (rule not_le_iff_lt [THEN iffD1], auto)
+apply (subgoal_tac "i #+ da < j #+ d", force)
+apply (blast intro: add_le_lt_mono)
+done
+
+lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)"
+apply (frule le_in_nat, assumption)
+apply (frule lt_nat_in_nat, assumption)
+apply (simp split add: nat_diff_split, auto)
+ apply (blast intro: lt_asym lt_trans2)
+ apply (blast intro: lt_irrefl lt_trans2)
+apply (rule not_le_iff_lt [THEN iffD1], auto)
+apply (subgoal_tac "j #+ d < i #+ da", force)
+apply (blast intro: add_lt_le_mono)
+done
+
+
+lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i"
+apply (frule le_in_nat, assumption)
+apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt)
+done
+
ML
{*
@@ -607,6 +635,8 @@
val add_lt_elim2 = thm "add_lt_elim2";
val add_le_elim2 = thm "add_le_elim2";
+
+val diff_lt_iff_lt = thm "diff_lt_iff_lt";
*}
end
--- a/src/ZF/IMP/Equiv.thy Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/IMP/Equiv.thy Fri Jun 20 12:10:45 2003 +0200
@@ -39,8 +39,6 @@
lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
apply (erule evalc.induct)
apply (simp_all (no_asm_simp))
- txt {* @{text skip} *}
- apply fast
txt {* @{text assign} *}
apply (simp add: update_type)
txt {* @{text comp} *}
@@ -48,7 +46,6 @@
txt {* @{text while} *}
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
apply (simp add: Gamma_def)
- apply force
txt {* recursive case of @{text while} *}
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
apply (auto simp add: Gamma_def)
--- a/src/ZF/IsaMakefile Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/IsaMakefile Fri Jun 20 12:10:45 2003 +0200
@@ -120,7 +120,7 @@
UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
- UNITY/AllocBase.ML UNITY/AllocBase.thy\
+ UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
UNITY/ClientImpl.ML UNITY/ClientImpl.thy\
UNITY/Distributor.ML UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
--- a/src/ZF/Perm.thy Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/Perm.thy Fri Jun 20 12:10:45 2003 +0200
@@ -195,8 +195,13 @@
apply (force intro!: lam_type dest: apply_type)
done
+text{*@{term id} as the identity relation*}
+lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
+by auto
-(*** Converse of a function ***)
+
+
+subsection{*Converse of a Function*}
lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A"
apply (unfold inj_def)
@@ -208,7 +213,7 @@
(** Equations for converse(f) **)
-(*The premises are equivalent to saying that f is injective...*)
+text{*The premises are equivalent to saying that f is injective...*}
lemma left_inverse_lemma:
"[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a"
by (blast intro: apply_Pair apply_equality converseI)
--- a/src/ZF/UNITY/AllocBase.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.ML Fri Jun 20 12:10:45 2003 +0200
@@ -15,20 +15,20 @@
qed "Nclients_NbT_gt_0";
Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
-Goal "Nclients ~= 0 & NbT ~= 0";
+Goal "Nclients \\<noteq> 0 & NbT \\<noteq> 0";
by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
by Auto_tac;
qed "Nclients_NbT_not_0";
Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0 RS conjunct2];
-Goal "Nclients:nat & NbT:nat";
+Goal "Nclients\\<in>nat & NbT\\<in>nat";
by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
by Auto_tac;
qed "Nclients_NbT_type";
Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
-Goal "b:Inter(RepFun(Nclients, B)) <-> (ALL x:Nclients. b:B(x))";
+Goal "b\\<in>Inter(RepFun(Nclients, B)) <-> (\\<forall>x\\<in>Nclients. b\\<in>B(x))";
by (auto_tac (claset(), simpset() addsimps [INT_iff]));
by (res_inst_tac [("x", "0")] exI 1);
by (rtac ltD 1);
@@ -38,15 +38,15 @@
val succ_def = thm "succ_def";
-Goal "n:nat ==> \
-\ (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
+Goal "n\\<in>nat ==> \
+\ (\\<forall>i\\<in>nat. i<n --> f(i) $<= g(i)) --> \
\ setsum(f, n) $<= setsum(g,n)";
by (induct_tac "n" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
+by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x\\<notin>x" 1);
by (Clarify_tac 1);
by (Asm_simp_tac 1);
-by (subgoal_tac "ALL i:nat. i<x--> f(i) $<= g(i)" 1);
+by (subgoal_tac "\\<forall>i\\<in>nat. i<x--> f(i) $<= g(i)" 1);
by (resolve_tac [zadd_zle_mono] 1);
by (thin_tac "succ(x)=cons(x,x)" 1);
by (ALLGOALS(Asm_simp_tac));
@@ -57,22 +57,22 @@
by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
qed_spec_mp "setsum_fun_mono";
-Goal "l:list(A) ==> tokens(l):nat";
+Goal "l\\<in>list(A) ==> tokens(l)\\<in>nat";
by (etac list.induct 1);
by Auto_tac;
qed "tokens_type";
AddTCs [tokens_type];
Addsimps [tokens_type];
-Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
-\ --> tokens(xs) le tokens(ys)";
+Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
+\ --> tokens(xs) \\<le> tokens(ys)";
by (induct_tac "xs" 1);
by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
simpset() addsimps [prefix_def]));
qed_spec_mp "tokens_mono_aux";
-Goal "[| <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
-\ tokens(xs) le tokens(ys)";
+Goal "<xs, ys>\\<in>prefix(A) ==> tokens(xs) \\<le> tokens(ys)";
+by (cut_facts_tac [prefix_type] 1);
by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
qed "tokens_mono";
@@ -84,13 +84,13 @@
AddIs [mono_tokens];
Goal
-"[| xs:list(A); ys:list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
+"[| xs\\<in>list(A); ys\\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "tokens_append";
Addsimps [tokens_append];
-Goal "l:list(A) ==> ALL n:nat. length(take(n, l))=min(n, length(l))";
+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;
by (ALLGOALS(Asm_simp_tac));
@@ -100,27 +100,27 @@
(** bag_of **)
-Goal "l:list(A) ==>bag_of(l):Mult(A)";
+Goal "l\\<in>list(A) ==>bag_of(l)\\<in>Mult(A)";
by (induct_tac "l" 1);
by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
qed "bag_of_type";
AddTCs [bag_of_type];
Addsimps [bag_of_type];
-Goal "l:list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
+Goal "l\\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
by (dtac bag_of_type 1);
by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
qed "bag_of_multiset";
-Goal "[| xs:list(A); ys:list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
+Goal "[| xs\\<in>list(A); ys\\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
by (induct_tac "xs" 1);
by (auto_tac (claset(), simpset()
addsimps [bag_of_multiset, munion_assoc]));
qed "bag_of_append";
Addsimps [bag_of_append];
-Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
-\ --> <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
+Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
+\ --> <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
by (induct_tac "xs" 1);
by (ALLGOALS(Clarify_tac));
by (ftac bag_of_multiset 1);
@@ -133,8 +133,8 @@
by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
qed_spec_mp "bag_of_mono_aux";
-Goal "[| <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
-\ <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
+Goal "[| <xs, ys>\\<in>prefix(A); xs\\<in>list(A); ys\\<in>list(A) |] ==> \
+\ <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
qed "bag_of_mono";
AddIs [bag_of_mono];
@@ -150,7 +150,7 @@
bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
-Goal "l : list(A) ==> C Int length(l) : Fin(length(l))";
+Goal "l \\<in> list(A) ==> C Int length(l) \\<in> Fin(length(l))";
by (dtac length_type 1);
by (rtac Fin_subset 1);
by (rtac Int_lower2 1);
@@ -182,7 +182,7 @@
by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1);
qed "bag_of_sublist_lemma";
-Goal "l:list(A) ==> \
+Goal "l\\<in>list(A) ==> \
\ C <= nat ==> \
\ bag_of(sublist(l, C)) = \
\ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
@@ -201,7 +201,7 @@
qed "nat_Int_length_eq";
(*eliminating the assumption C<=nat*)
-Goal "l:list(A) ==> \
+Goal "l\\<in>list(A) ==> \
\ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
by (subgoal_tac
" bag_of(sublist(l, C Int nat)) = \
@@ -211,7 +211,7 @@
qed "bag_of_sublist";
Goal
-"l:list(A) ==> \
+"l\\<in>list(A) ==> \
\ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
\ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
by (subgoal_tac
@@ -226,16 +226,16 @@
qed "bag_of_sublist_Un_Int";
-Goal "[| l:list(A); B Int C = 0 |]\
+Goal "[| l\\<in>list(A); B Int C = 0 |]\
\ ==> bag_of(sublist(l, B Un C)) = \
\ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym,
sublist_type, bag_of_multiset]) 1);
qed "bag_of_sublist_Un_disjoint";
-Goal "[| Finite(I); ALL i:I. ALL j:I. i~=j --> A(i) Int A(j) = 0; \
-\ l:list(B) |] \
-\ ==> bag_of(sublist(l, UN i:I. A(i))) = \
+Goal "[|Finite(I); \\<forall>i\\<in>I. \\<forall>j\\<in>I. i\\<noteq>j --> A(i) \\<inter> A(j) = 0; \
+\ l\\<in>list(B) |] \
+\ ==> bag_of(sublist(l, \\<Union>i\\<in>I. A(i))) = \
\ (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";
by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
addsimps [bag_of_sublist]) 1);
@@ -263,13 +263,13 @@
Goalw [all_distinct_def]
"all_distinct(Cons(a, l)) <-> \
-\ (a:set_of_list(l) --> False) & (a ~: set_of_list(l) --> all_distinct(l))";
+\ (a\\<in>set_of_list(l) --> False) & (a \\<notin> set_of_list(l) --> all_distinct(l))";
by (auto_tac (claset() addEs [list.elim], simpset()));
qed "all_distinct_Cons";
Addsimps [all_distinct_Nil, all_distinct_Cons];
(** state_of **)
-Goalw [state_of_def] "s:state ==> state_of(s)=s";
+Goalw [state_of_def] "s\\<in>state ==> state_of(s)=s";
by Auto_tac;
qed "state_of_state";
Addsimps [state_of_state];
@@ -281,7 +281,7 @@
Addsimps [state_of_idem];
-Goalw [state_of_def] "state_of(s):state";
+Goalw [state_of_def] "state_of(s)\\<in>state";
by Auto_tac;
qed "state_of_type";
Addsimps [state_of_type];
@@ -329,25 +329,25 @@
handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
handle THM _ => th;
-Goal "n:nat ==> nat_list_inj(n):list(nat)";
+Goal "n\\<in>nat ==> nat_list_inj(n)\\<in>list(nat)";
by (induct_tac "n" 1);
by Auto_tac;
qed "nat_list_inj_type";
-Goal "n:nat ==> length(nat_list_inj(n)) = n";
+Goal "n\\<in>nat ==> length(nat_list_inj(n)) = n";
by (induct_tac "n" 1);
by Auto_tac;
qed "length_nat_list_inj";
Goalw [nat_var_inj_def]
- "(lam x:nat. nat_var_inj(x)):inj(nat, var)";
+ "(\\<lambda>x\\<in>nat. nat_var_inj(x))\\<in>inj(nat, var)";
by (res_inst_tac [("d", "var_inj")] lam_injective 1);
by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
qed "var_infinite_lemma";
Goalw [lepoll_def] "nat lepoll var";
-by (res_inst_tac [("x", "(lam x:nat. nat_var_inj(x))")] exI 1);
+by (res_inst_tac [("x", "(\\<lambda>x\\<in>nat. nat_var_inj(x))")] exI 1);
by (rtac var_infinite_lemma 1);
qed "nat_lepoll_var";
@@ -369,15 +369,15 @@
by (blast_tac (claset() addEs [mem_irrefl]) 1);
qed "var_not_Finite";
-Goal "~Finite(A) ==> EX x. x:A";
+Goal "~Finite(A) ==> \\<exists>x. x\\<in>A";
by (etac swap 1);
by Auto_tac;
by (subgoal_tac "A=0" 1);
by (auto_tac (claset(), simpset() addsimps [Finite_0]));
qed "not_Finite_imp_exist";
-Goal "Finite(A) ==> b:(Inter(RepFun(var-A, B))) <-> (ALL x:var-A. b:B(x))";
-by (subgoal_tac "EX x. x:var-A" 1);
+Goal "Finite(A) ==> b\\<in>(Inter(RepFun(var-A, B))) <-> (\\<forall>x\\<in>var-A. b\\<in>B(x))";
+by (subgoal_tac "\\<exists>x. x\\<in>var-A" 1);
by Auto_tac;
by (subgoal_tac "~Finite(var-A)" 1);
by (dtac not_Finite_imp_exist 1);
@@ -388,38 +388,39 @@
by Auto_tac;
qed "Inter_Diff_var_iff";
-Goal "[| b:Inter(RepFun(var-A, B)); Finite(A); x:var-A |] ==> b:B(x)";
+Goal "[| b\\<in>Inter(RepFun(var-A, B)); Finite(A); x\\<in>var-A |] ==> b\\<in>B(x)";
by (rotate_tac 1 1);
by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
qed "Inter_var_DiffD";
-(* [| Finite(A); (ALL x:var-A. b:B(x)) |] ==> b:Inter(RepFun(var-A, B)) *)
+(* [| Finite(A); (\\<forall>x\\<in>var-A. b\\<in>B(x)) |] ==> b\\<in>Inter(RepFun(var-A, B)) *)
bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
AddSIs [Inter_var_DiffI];
Addsimps [Finite_0, Finite_cons];
-Goal "Acts(F)<= A Int Pow(state*state) <-> Acts(F)<=A";
+Goal "Acts(F)<= A \\<inter> Pow(state*state) <-> Acts(F)<=A";
by (cut_facts_tac [inst "F" "F" Acts_type] 1);
by Auto_tac;
qed "Acts_subset_Int_Pow_simp";
Addsimps [Acts_subset_Int_Pow_simp];
-Goal "cons(x, A Int B) = cons(x, A) Int cons(x, B)";
+(*for main zf?????*)
+Goal "cons(x, A \\<inter> B) = cons(x, A) \\<inter> cons(x, B)";
by Auto_tac;
qed "cons_Int_distrib";
(* Currently not used, but of potential interest *)
Goal
-"[| Finite(A); ALL x:A. g(x):nat |] ==> \
+"[| Finite(A); \\<forall>x\\<in>A. g(x)\\<in>nat |] ==> \
\ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
by (etac Finite_induct 1);
by (auto_tac (claset(), simpset() addsimps [int_of_add]));
qed "setsum_nsetsum_eq";
Goal
-"[| A=B; ALL x:A. f(x)=g(x); ALL x:A. g(x):nat; \
+"[| A=B; \\<forall>x\\<in>A. f(x)=g(x); \\<forall>x\\<in>A. g(x)\\<in>nat; \
\ Finite(A) |] ==> nsetsum(f, A) = nsetsum(g, B)";
by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
by (rtac trans 2);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/AllocImpl.thy Fri Jun 20 12:10:45 2003 +0200
@@ -0,0 +1,796 @@
+(*Title: ZF/UNITY/AllocImpl
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Single-client allocator implementation
+Charpentier and Chandy, section 7 (page 17).
+*)
+
+(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
+
+theory AllocImpl = ClientImpl:
+
+(*????MOVE UP*)
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
+ "for proving safety properties"
+
+consts
+
+ NbR :: i (*number of consumed messages*)
+ available_tok :: i (*number of free tokens (T in paper)*)
+
+translations
+ "NbR" == "Var([succ(2)])"
+ "available_tok" == "Var([succ(succ(2))])"
+
+axioms
+ alloc_type_assumes:
+ "type_of(NbR) = nat & type_of(available_tok)=nat"
+
+ alloc_default_val_assumes:
+ "default_val(NbR) = 0 & default_val(available_tok)=0"
+
+constdefs
+ alloc_giv_act :: i
+ "alloc_giv_act ==
+ {<s, t> : state*state.
+ \<exists>k. k = length(s`giv) &
+ t = s(giv := s`giv @ [nth(k, s`ask)],
+ available_tok := s`available_tok #- nth(k, s`ask)) &
+ k < length(s`ask) & nth(k, s`ask) le s`available_tok}"
+
+ alloc_rel_act :: i
+ "alloc_rel_act ==
+ {<s, t> : state*state.
+ t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
+ NbR := succ(s`NbR)) &
+ s`NbR < length(s`rel)}"
+
+ (*The initial condition s`giv=[] is missing from the
+ original definition -- S. O. Ehmety *)
+ alloc_prog :: i
+ "alloc_prog ==
+ mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
+ {alloc_giv_act, alloc_rel_act},
+ \<Union>G \<in> preserves(lift(available_tok)) \<inter>
+ preserves(lift(NbR)) \<inter>
+ preserves(lift(giv)). Acts(G))"
+
+
+
+
+(*????FIXME: sort out this mess
+FoldSet.cons_Int_right_lemma1:
+ ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
+FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
+Multiset.cons_Int_right_cases:
+ cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
+UNITYMisc.Int_cons_right:
+ ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
+UNITYMisc.Int_succ_right:
+ ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
+*)
+
+
+declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
+
+lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
+apply (unfold state_def)
+apply (drule_tac a = "available_tok" in apply_type)
+apply auto
+done
+
+lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
+apply (unfold state_def)
+apply (drule_tac a = "NbR" in apply_type)
+apply auto
+done
+
+(** The Alloc Program **)
+
+lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
+apply (simp add: alloc_prog_def)
+done
+
+declare alloc_prog_def [THEN def_prg_Init, simp]
+declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
+ML
+{*
+program_defs_ref := [thm"alloc_prog_def"]
+*}
+
+declare alloc_giv_act_def [THEN def_act_simp, simp]
+declare alloc_rel_act_def [THEN def_act_simp, simp]
+
+
+lemma alloc_prog_ok_iff:
+"\<forall>G \<in> program. (alloc_prog ok G) <->
+ (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) &
+ G \<in> preserves(lift(NbR)) & alloc_prog \<in> Allowed(G))"
+by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed])
+
+
+lemma alloc_prog_preserves:
+ "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
+apply (rule Inter_var_DiffI)
+apply (force );
+apply (rule ballI)
+apply (rule preservesI)
+apply (constrains)
+done
+
+(* As a special case of the rule above *)
+
+lemma alloc_prog_preserves_rel_ask_tok:
+ "alloc_prog \<in>
+ preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
+apply auto
+apply (insert alloc_prog_preserves)
+apply (drule_tac [3] x = "tok" in Inter_var_DiffD)
+apply (drule_tac [2] x = "ask" in Inter_var_DiffD)
+apply (drule_tac x = "rel" in Inter_var_DiffD)
+apply auto
+done
+
+lemma alloc_prog_Allowed:
+"Allowed(alloc_prog) =
+ preserves(lift(giv)) \<inter> preserves(lift(available_tok)) \<inter> preserves(lift(NbR))"
+apply (cut_tac v="lift(giv)" in preserves_type)
+apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
+ cons_Int_distrib safety_prop_Acts_iff)
+done
+
+(* In particular we have *)
+lemma alloc_prog_ok_client_prog: "alloc_prog ok client_prog"
+apply (auto simp add: ok_iff_Allowed)
+apply (cut_tac alloc_prog_preserves)
+apply (cut_tac [2] client_prog_preserves)
+apply (auto simp add: alloc_prog_Allowed client_prog_Allowed)
+apply (drule_tac [6] B = "preserves (lift (NbR))" in InterD)
+apply (drule_tac [5] B = "preserves (lift (available_tok))" in InterD)
+apply (drule_tac [4] B = "preserves (lift (giv))" in InterD)
+apply (drule_tac [3] B = "preserves (lift (tok))" in InterD)
+apply (drule_tac [2] B = "preserves (lift (ask))" in InterD)
+apply (drule_tac B = "preserves (lift (rel))" in InterD)
+apply auto
+done
+
+(** Safety property: (28) **)
+lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed)
+apply constrains+
+apply (auto dest: ActsD)
+apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
+apply auto
+done
+
+lemma giv_Bounded_lamma1:
+"alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
+ {s\<in>state. s`available_tok #+ tokens(s`giv) =
+ NbT #+ tokens(take(s`NbR, s`rel))})"
+apply (constrains)
+apply auto
+apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
+apply (simp (no_asm_simp) add: take_succ)
+done
+
+lemma giv_Bounded_lemma2:
+"[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
+ ==> alloc_prog Join G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
+ {s\<in>state. s`available_tok #+ tokens(s`giv) =
+ NbT #+ tokens(take(s`NbR, s`rel))})"
+apply (cut_tac giv_Bounded_lamma1)
+apply (cut_tac alloc_prog_preserves_rel_ask_tok)
+apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
+apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
+apply (rotate_tac -1)
+apply (cut_tac A = "nat * nat * list(nat)"
+ and P = "%<m,n,l> y. n \<le> length(y) &
+ m #+ tokens(l) = NbT #+ tokens(take(n,y))"
+ and g = "lift(rel)" and F = "alloc_prog"
+ in stable_Join_Stable)
+prefer 3 apply assumption;
+apply (auto simp add: Collect_conj_eq)
+apply (frule_tac g = "length" in imp_Increasing_comp)
+apply (blast intro: mono_length)
+apply (auto simp add: refl_prefix)
+apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
+apply assumption
+apply (auto simp add: Le_def length_type)
+apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def)
+apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
+apply assumption+
+apply (force dest: ActsD)
+apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) Un Acts (G). ?P(x)" in thin_rl)
+apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
+apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
+apply (auto simp add: Stable_def Constrains_def constrains_def)
+apply (drule bspec)
+apply force
+apply (drule subsetD)
+apply (rule imageI)
+apply assumption
+apply (auto simp add: prefix_take_iff)
+apply (rotate_tac -1)
+apply (erule ssubst)
+apply (auto simp add: take_take min_def)
+done
+
+(*Property (29), page 18:
+ the number of tokens in circulation never exceeds NbT*)
+lemma alloc_prog_giv_Bounded: "alloc_prog \<in> Incr(lift(rel))
+ guarantees Always({s\<in>state. tokens(s`giv) \<le> NbT #+ tokens(s`rel)})"
+apply (cut_tac NbT_pos)
+apply (auto simp add: guar_def)
+apply (rule Always_weaken)
+apply (rule AlwaysI)
+apply (rule_tac [2] giv_Bounded_lemma2)
+apply auto
+apply (rule_tac j = "NbT #+ tokens (take (x` NbR, x`rel))" in le_trans)
+apply (erule subst)
+apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
+done
+
+(*Property (30), page 18: the number of tokens given never exceeds the number
+ asked for*)
+lemma alloc_prog_ask_prefix_giv:
+ "alloc_prog \<in> Incr(lift(ask)) guarantees
+ Always({s\<in>state. <s`giv, s`ask>:prefix(tokbag)})"
+apply (auto intro!: AlwaysI simp add: guar_def)
+apply (subgoal_tac "G \<in> preserves (lift (giv))")
+ prefer 2 apply (simp add: alloc_prog_ok_iff)
+apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
+ in stable_Join_Stable)
+apply (constrains)
+ prefer 2 apply (simp add: lift_def);
+ apply (clarify );
+apply (drule_tac a = "k" in Increasing_imp_Stable)
+apply auto
+done
+
+(**** Towards proving the liveness property, (31) ****)
+
+(*** First, we lead up to a proof of Lemma 49, page 28. ***)
+
+lemma alloc_prog_transient_lemma:
+"G \<in> program ==> \<forall>k\<in>nat. alloc_prog Join G \<in>
+ transient({s\<in>state. k \<le> length(s`rel)}
+ \<inter> {s\<in>state. succ(s`NbR) = k})"
+apply auto
+apply (erule_tac V = "G\<notin>?u" in thin_rl)
+apply (rule_tac act = "alloc_rel_act" in transientI)
+apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
+apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
+apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
+apply (rule ReplaceI)
+apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
+ NbR:=succ (x`NbR))"
+ in exI)
+apply (auto intro!: state_update_type)
+done
+
+lemma alloc_prog_rel_Stable_NbR_lemma:
+"[| G \<in> program; alloc_prog ok G; k\<in>nat |] ==>
+ alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
+apply constrains
+apply auto
+apply (blast intro: le_trans leI)
+apply (drule_tac f = "lift (NbR)" and A = "nat" in preserves_imp_increasing)
+apply (drule_tac [2] g = "succ" in imp_increasing_comp)
+apply (rule_tac [2] mono_succ)
+apply (drule_tac [4] x = "k" in increasing_imp_stable)
+ prefer 5 apply (simp add: Le_def comp_def)
+apply auto
+done
+
+lemma alloc_prog_NbR_LeadsTo_lemma [rule_format (no_asm)]:
+"[| G \<in> program; alloc_prog ok G;
+ alloc_prog Join G \<in> Incr(lift(rel)) |] ==>
+ \<forall>k\<in>nat. alloc_prog Join G \<in>
+ {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
+ LeadsTo {s\<in>state. k \<le> s`NbR}"
+apply clarify
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
+apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (rule_tac [2] mono_length)
+ prefer 3 apply (simp add: );
+apply (simp_all add: refl_prefix Le_def comp_def length_type)
+apply (rule LeadsTo_weaken)
+apply (rule PSP_Stable)
+prefer 2 apply (assumption)
+apply (rule PSP_Stable)
+apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
+apply (rule alloc_prog_transient_lemma [THEN bspec, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo])
+apply assumption+
+apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
+done
+
+lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
+ "[| G :program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
+ ==> \<forall>k\<in>nat. \<forall>n \<in> nat. n < k -->
+ alloc_prog Join G \<in>
+ {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
+ LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
+ (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
+apply (unfold greater_than_def)
+apply clarify
+apply (rule_tac A' = "{x \<in> state. k \<le> length (x`rel) } \<inter> {x \<in> state. n < x`NbR}" in LeadsTo_weaken_R)
+apply safe
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
+apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (rule_tac [2] mono_length)
+ prefer 3 apply (simp add: );
+apply (simp_all add: refl_prefix Le_def comp_def length_type)
+apply (subst Int_commute)
+apply (rule_tac A = " ({s \<in> state . k \<le> length (s ` rel) } \<inter> {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length (s`rel) }" in LeadsTo_weaken_L)
+apply (rule PSP_Stable)
+apply safe
+apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
+apply (rule_tac [2] LeadsTo_weaken)
+apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
+apply (simp_all add: )
+apply (rule subset_imp_LeadsTo)
+apply auto
+apply (blast intro: lt_trans2)
+done
+
+lemma Collect_vimage_eq: "u\<in>nat ==> {<s, f(s)>. s \<in> state} -`` u = {s\<in>state. f(s) < u}"
+apply (force simp add: lt_def)
+done
+
+(* Lemma 49, page 28 *)
+
+lemma alloc_prog_NbR_LeadsTo_lemma3:
+ "[|G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+ k\<in>nat|]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
+(* Proof by induction over the difference between k and n *)
+apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
+apply (simp_all add: lam_def)
+apply auto
+apply (rule single_LeadsTo_I)
+apply auto
+apply (simp (no_asm_simp) add: Collect_vimage_eq)
+apply (rename_tac "s0")
+apply (case_tac "s0`NbR < k")
+apply (rule_tac [2] subset_imp_LeadsTo)
+apply safe
+apply (auto dest!: not_lt_imp_le)
+apply (rule LeadsTo_weaken)
+apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2)
+apply safe
+prefer 3 apply (assumption)
+apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
+apply (blast dest: lt_asym)
+apply (force dest: add_lt_elim2)
+done
+
+(** Towards proving lemma 50, page 29 **)
+
+lemma alloc_prog_giv_Ensures_lemma:
+"[| G \<in> program; k\<in>nat; alloc_prog ok G;
+ alloc_prog Join G \<in> Incr(lift(ask)) |] ==>
+ alloc_prog Join G \<in>
+ {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
+ {s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
+ Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
+apply (rule EnsuresI)
+apply auto
+apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
+apply (rule_tac [2] act = "alloc_giv_act" in transientI)
+ prefer 2
+ apply (simp add: alloc_prog_def [THEN def_prg_Acts])
+ apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
+apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
+apply (erule_tac [2] swap)
+apply (rule_tac [2] ReplaceI)
+apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length (x`giv), x ` ask))" in exI)
+apply (auto intro!: state_update_type simp add: app_type)
+apply (rule_tac A = "{s\<in>state . nth (length (s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length (s ` ask) } \<inter> {s\<in>state. length (s`giv) =k}" and A' = "{s\<in>state . nth (length (s ` giv), s ` ask) \<le> s ` available_tok} Un {s\<in>state. ~ k < length (s`ask) } Un {s\<in>state . length (s ` giv) \<noteq> k}" in Constrains_weaken)
+apply safe
+apply (auto dest: ActsD simp add: Constrains_def constrains_def length_app alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
+apply (subgoal_tac "length (xa ` giv @ [nth (length (xa ` giv), xa ` ask) ]) = length (xa ` giv) #+ 1")
+apply (rule_tac [2] trans)
+apply (rule_tac [2] length_app)
+apply auto
+apply (rule_tac j = "xa ` available_tok" in le_trans)
+apply auto
+apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
+apply assumption+
+apply auto
+apply (drule_tac a = "xa ` ask" and r = "prefix(tokbag)" and A = "list(tokbag)"
+ in Increasing_imp_Stable)
+apply (auto simp add: prefix_iff)
+apply (drule StableD)
+apply (auto simp add: Constrains_def constrains_def)
+apply force
+done
+
+lemma alloc_prog_giv_Stable_lemma:
+"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
+ ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
+apply (constrains)
+apply (auto intro: leI simp add: length_app)
+apply (drule_tac f = "lift (giv)" and g = "length" in imp_preserves_comp)
+apply (drule_tac f = "length comp lift (giv)" and A = "nat" and r = "Le" in preserves_imp_increasing)
+apply (drule_tac [2] x = "k" in increasing_imp_stable)
+ prefer 3 apply (simp add: Le_def comp_def)
+apply (auto simp add: length_type)
+done
+
+(* Lemma 50, page 29 *)
+
+lemma alloc_prog_giv_LeadsTo_lemma:
+"[| G \<in> program; alloc_prog ok G;
+ alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |] ==>
+ alloc_prog Join G \<in>
+ {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
+ {s\<in>state. k < length(s`ask)} \<inter>
+ {s\<in>state. length(s`giv) = k}
+ LeadsTo {s\<in>state. k < length(s`giv)}"
+apply (subgoal_tac "alloc_prog Join G \<in> {s\<in>state. nth (length (s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length (s`ask) } \<inter> {s\<in>state. length (s`giv) = k} LeadsTo {s\<in>state. ~ k <length (s`ask) } Un {s\<in>state. length (s`giv) \<noteq> k}")
+prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length (s`ask) }) ")
+apply (drule PSP_Stable)
+apply assumption
+apply (rule LeadsTo_weaken)
+apply (rule PSP_Stable)
+apply (rule_tac [2] k = "k" in alloc_prog_giv_Stable_lemma)
+apply (auto simp add: le_iff)
+apply (drule_tac a = "succ (k)" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (rule mono_length)
+ prefer 2 apply (simp add: );
+apply (simp_all add: refl_prefix Le_def comp_def length_type)
+done
+
+(* Lemma 51, page 29.
+ This theorem states as invariant that if the number of
+ tokens given does not exceed the number returned, then the upper limit
+ (NbT) does not exceed the number currently available.*)
+lemma alloc_prog_Always_lemma:
+"[| G \<in> program; alloc_prog ok G;
+ alloc_prog Join G \<in> Incr(lift(ask));
+ alloc_prog Join G \<in> Incr(lift(rel)) |]
+ ==> alloc_prog Join G \<in>
+ Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
+ NbT \<le> s`available_tok})"
+apply (subgoal_tac "alloc_prog Join G \<in> Always ({s\<in>state. s`NbR \<le> length (s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens (s`giv) = NbT #+ tokens (take (s`NbR, s`rel))}) ")
+apply (rule_tac [2] AlwaysI)
+apply (rule_tac [3] giv_Bounded_lemma2)
+apply auto
+apply (rule Always_weaken)
+apply assumption
+apply auto
+apply (subgoal_tac "0 \<le> tokens (take (x ` NbR, x ` rel)) #- tokens (x`giv) ")
+apply (rule_tac [2] nat_diff_split [THEN iffD2])
+ prefer 2 apply (force );
+apply (subgoal_tac "x`available_tok =
+ NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens (x`giv))")
+apply (simp (no_asm_simp))
+apply (rule nat_diff_split [THEN iffD2])
+apply auto
+apply (drule_tac j = "tokens (x ` giv)" in lt_trans2)
+apply assumption
+apply auto
+done
+
+(* Main lemmas towards proving property (31) *)
+
+lemma LeadsTo_strength_R:
+ "[| F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo B"
+by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
+
+lemma PSP_StableI:
+"[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
+ F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo B"
+apply (rule_tac A = " (A-C) Un (A \<inter> C)" in LeadsTo_weaken_L)
+ prefer 2 apply (blast)
+apply (rule LeadsTo_Un)
+apply assumption
+apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
+done
+
+lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
+apply auto
+done
+
+(*needed?*)
+lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
+apply auto
+done
+
+
+(*First step in proof of (31) -- the corrected version from Charpentier.
+ This lemma implies that if a client releases some tokens then the Allocator
+ will eventually recognize that they've been released.*)
+lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ G \<in> program; alloc_prog ok G; k \<in> tokbag |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. k \<le> tokens(s`rel)}
+ LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
+apply (rule single_LeadsTo_I)
+apply safe
+apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
+apply (rule_tac [4] k1 = "length (s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
+apply (rule_tac [8] subset_imp_LeadsTo)
+apply auto
+apply (rule_tac j = "tokens (take (length (s`rel), x`rel))" in le_trans)
+apply (rule_tac j = "tokens (take (length (s`rel), s`rel))" in le_trans)
+apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
+done
+
+(*** Rest of proofs done by lcp ***)
+
+(*Second step in proof of (31): by LHS of the guarantee and transivity of
+ LeadsTo *)
+lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma2:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ G \<in> program; alloc_prog ok G; k \<in> tokbag;
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. tokens(s`giv) = k}
+ LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
+apply (rule LeadsTo_Trans)
+apply (rule_tac [2] alloc_prog_LeadsTo_tokens_take_NbR_lemma)
+apply (blast intro: LeadsTo_weaken_L nat_into_Ord)
+apply assumption+
+done
+
+(*Third step in proof of (31): by PSP with the fact that giv increases *)
+lemma alloc_prog_LeadsTo_length_giv_disj:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
+ k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
+apply (rule single_LeadsTo_I)
+apply safe
+apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
+apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
+apply (simp_all add: Int_cons_left)
+apply (rule LeadsTo_weaken)
+apply (rule_tac k = "tokens (s`giv)" in alloc_prog_LeadsTo_tokens_take_NbR_lemma2)
+apply simp_all
+apply safe
+apply (drule prefix_length_le [THEN le_iff [THEN iffD1]])
+apply (force simp add:)
+apply (simp add: not_lt_iff_le)
+apply (drule prefix_length_le_equal)
+apply assumption
+apply (simp add:)
+done
+
+(*Fourth step in proof of (31): we apply lemma (51) *)
+lemma alloc_prog_LeadsTo_length_giv_disj2:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
+ n < length(s`giv)}"
+apply (rule LeadsTo_weaken_R)
+apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma alloc_prog_LeadsTo_length_giv_disj])
+apply auto
+done
+
+(*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)}"
+apply blast
+done
+
+
+(*Fifth step in proof of (31): from the fourth step, taking the union over all
+ k\<in>nat *)
+lemma alloc_prog_LeadsTo_length_giv_disj3:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; n \<in> nat;
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
+ n < length(s`giv)}"
+apply (rule LeadsTo_weaken_L)
+apply (rule_tac I = "nat" in LeadsTo_UN)
+apply (rule_tac k = "i" in alloc_prog_LeadsTo_length_giv_disj2)
+apply (simp_all add: UN_conj_eq)
+done
+
+(*Sixth step in proof of (31): from the fifth step, by PSP with the
+ assumption that ask increases *)
+lemma alloc_prog_LeadsTo_length_ask_giv:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+ LeadsTo
+ {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
+ length(s`giv) = n) |
+ n < length(s`giv)}"
+apply (rule single_LeadsTo_I)
+apply safe
+apply (rule_tac a1 = "s`ask" and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI])
+apply assumption
+apply simp_all
+apply (rule LeadsTo_weaken)
+apply (rule_tac n = "length (s ` giv)" in alloc_prog_LeadsTo_length_giv_disj3)
+apply simp_all
+apply (blast intro:)
+apply clarify
+apply (simp add:)
+apply (blast dest!: prefix_length_le intro: lt_trans2)
+done
+
+
+(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
+lemma alloc_prog_LeadsTo_length_ask_giv2:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
+ alloc_prog Join G \<in>
+ Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+ LeadsTo
+ {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
+ length(s`giv) < length(s`ask) & length(s`giv) = n) |
+ n < length(s`giv)}"
+apply (rule LeadsTo_weaken_R)
+apply (erule Always_LeadsToD [OF asm_rl alloc_prog_LeadsTo_length_ask_giv])
+apply assumption+
+apply clarify
+apply (simp add: INT_iff)
+apply clarify
+apply (drule_tac x = "length (x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
+apply (simp add:)
+apply (blast intro: le_trans)
+done
+
+(*Eighth step in proof of (31): by (50), we get |giv| > n. *)
+lemma alloc_prog_LeadsTo_extend_giv:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
+ alloc_prog Join G \<in>
+ Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+ LeadsTo {s\<in>state. n < length(s`giv)}"
+apply (rule LeadsTo_Un_duplicate)
+apply (rule LeadsTo_cancel1)
+apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
+apply safe;
+ prefer 2 apply (simp add: lt_nat_in_nat)
+apply (rule LeadsTo_weaken_R)
+apply (rule alloc_prog_LeadsTo_length_ask_giv2)
+apply auto
+done
+
+(*Ninth and tenth steps in proof of (31): by (50), we get |giv| > n.
+ The report has an error: putting |ask|=k for the precondition fails because
+ we can't expect |ask| to remain fixed until |giv| increases.*)
+lemma alloc_prog_ask_LeadsTo_giv:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; k \<in> nat;
+ alloc_prog Join G \<in>
+ Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
+(* Proof by induction over the difference between k and n *)
+apply (rule_tac f = "\<lambda>s\<in>state. k #- length (s`giv)" in LessThan_induct)
+apply (simp_all add: lam_def)
+ prefer 2 apply (force)
+apply clarify
+apply (simp add: Collect_vimage_eq)
+apply (rule single_LeadsTo_I)
+apply safe
+apply simp
+apply (rename_tac "s0")
+apply (case_tac "length (s0 ` giv) < length (s0 ` ask) ")
+ apply (rule_tac [2] subset_imp_LeadsTo)
+ apply safe
+ prefer 2
+ apply (simp add: not_lt_iff_le)
+ apply (blast dest: le_imp_not_lt intro: lt_trans2)
+apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
+ in Increasing_imp_Stable [THEN PSP_StableI])
+apply assumption
+apply (simp add:)
+apply (force simp add:)
+apply (rule LeadsTo_weaken)
+apply (rule_tac n = "length (s0 ` giv)" and k = "length (s0 ` ask)"
+ in alloc_prog_LeadsTo_extend_giv)
+apply simp_all
+ apply (force simp add:)
+apply clarify
+apply (simp add:)
+apply (erule disjE)
+ apply (blast dest!: prefix_length_le intro: lt_trans2)
+apply (rule not_lt_imp_le)
+apply clarify
+apply (simp_all add: leI diff_lt_iff_lt)
+done
+
+(*Final lemma: combine previous result with lemma (30)*)
+lemma alloc_prog_progress_lemma:
+"[| alloc_prog Join G \<in> Incr(lift(rel));
+ alloc_prog Join G \<in> Incr(lift(ask));
+ G \<in> program; alloc_prog ok G; h \<in> list(tokbag);
+ alloc_prog Join G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
+ alloc_prog Join G \<in>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ {s\<in>state. k \<le> tokens(s`rel)}) |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
+apply (rule single_LeadsTo_I)
+ prefer 2 apply (simp)
+apply (rename_tac s0)
+apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
+ in Increasing_imp_Stable [THEN PSP_StableI])
+ apply assumption
+ prefer 2 apply (force simp add:)
+apply (simp_all add: Int_cons_left)
+apply (rule LeadsTo_weaken)
+apply (rule_tac k1 = "length (s0 ` ask)"
+ in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
+ alloc_prog_ask_LeadsTo_giv])
+apply simp_all
+apply (force simp add:)
+apply (force simp add:)
+apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le lt_trans2)
+done
+
+(** alloc_prog liveness property (31), page 18 **)
+
+(*missing the LeadsTo assumption on the lhs!?!?!*)
+lemma alloc_prog_progress:
+"alloc_prog \<in>
+ Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
+ Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ {s\<in>state. k \<le> tokens(s`rel)})
+ guarantees (\<Inter>h \<in> list(tokbag).
+ {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
+apply (rule guaranteesI)
+apply (rule INT_I)
+apply (rule alloc_prog_progress_lemma)
+apply simp_all
+apply (blast intro:)
+done
+
+
+end
--- a/src/ZF/UNITY/ClientImpl.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.ML Fri Jun 20 12:10:45 2003 +0200
@@ -191,7 +191,7 @@
by (auto_tac (claset(),
simpset() addsimps [prefix_def, Ge_def]));
by (dtac strict_prefix_length_lt 1);
-by (dres_inst_tac [("x", "length(x`rel)")] bspec 1);
+by (dres_inst_tac [("x", "length(x`rel)")] spec 1);
by Auto_tac;
by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
by (auto_tac (claset(), simpset() addsimps [id_def, lam_def]));
--- a/src/ZF/UNITY/Constrains.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/Constrains.ML Fri Jun 20 12:10:45 2003 +0200
@@ -434,7 +434,7 @@
(*proves "co" properties when the program is specified*)
-fun constrains_tac i =
+fun gen_constrains_tac(cs,ss) i =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac Always_ConstrainsI 1
@@ -445,14 +445,16 @@
(* Three subgoals *)
rewrite_goal_tac [st_set_def] 3,
REPEAT (Force_tac 2),
- full_simp_tac (simpset() addsimps !program_defs_ref) 1,
- ALLGOALS Clarify_tac,
+ full_simp_tac (ss addsimps !program_defs_ref) 1,
+ ALLGOALS (clarify_tac cs),
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS Clarify_tac,
- ALLGOALS Asm_full_simp_tac,
- ALLGOALS Clarify_tac]) i;
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_full_simp_tac ss),
+ ALLGOALS (clarify_tac cs)]) i;
+
+fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
(*For proving invariants*)
fun always_tac i =
--- a/src/ZF/UNITY/GenPrefix.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.ML Fri Jun 20 12:10:45 2003 +0200
@@ -12,13 +12,13 @@
*)
Goalw [refl_def]
- "[| refl(A, r); x:A |] ==> <x,x>:r";
+ "[| refl(A, r); x \\<in> A |] ==> <x,x>:r";
by Auto_tac;
qed "reflD";
(*** preliminary lemmas ***)
-Goal "xs:list(A) ==> <[], xs>:gen_prefix(A, r)";
+Goal "xs \\<in> list(A) ==> <[], xs> \\<in> gen_prefix(A, r)";
by (dtac (rotate_prems 1 gen_prefix.append) 1);
by (rtac gen_prefix.Nil 1);
by Auto_tac;
@@ -26,19 +26,19 @@
Addsimps [Nil_gen_prefix];
-Goal "<xs,ys>:gen_prefix(A, r) ==> length(xs) le length(ys)";
+Goal "<xs,ys> \\<in> gen_prefix(A, r) ==> length(xs) \\<le> length(ys)";
by (etac gen_prefix.induct 1);
-by (subgoal_tac "ys:list(A)" 3);
+by (subgoal_tac "ys \\<in> list(A)" 3);
by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
addIs [le_trans],
simpset() addsimps [length_app]));
qed "gen_prefix_length_le";
-Goal "[| <xs', ys'>:gen_prefix(A, r) |] \
-\ ==> (ALL x xs. x:A --> xs'= Cons(x,xs) --> \
-\ (EX y ys. y:A & ys' = Cons(y,ys) &\
-\ <x,y>:r & <xs, ys>:gen_prefix(A, r)))";
+Goal "[| <xs', ys'> \\<in> gen_prefix(A, r) |] \
+\ ==> (\\<forall>x xs. x \\<in> A --> xs'= Cons(x,xs) --> \
+\ (\\<exists>y ys. y \\<in> A & ys' = Cons(y,ys) &\
+\ <x,y>:r & <xs, ys> \\<in> gen_prefix(A, r)))";
by (etac gen_prefix.induct 1);
by (force_tac (claset() addIs [gen_prefix.append],
simpset()) 3);
@@ -47,9 +47,9 @@
(*As usual converting it to an elimination rule is tiresome*)
val major::prems =
-Goal "[| <Cons(x,xs), zs>:gen_prefix(A, r); \
-\ !!y ys. [|zs = Cons(y, ys); y:A; x:A; <x,y>:r; \
-\ <xs,ys>:gen_prefix(A, r) |] ==> P \
+Goal "[| <Cons(x,xs), zs> \\<in> gen_prefix(A, r); \
+\ !!y ys. [|zs = Cons(y, ys); y \\<in> A; x \\<in> A; <x,y>:r; \
+\ <xs,ys> \\<in> gen_prefix(A, r) |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
@@ -65,8 +65,8 @@
AddSEs [Cons_gen_prefixE];
Goal
-"(<Cons(x,xs),Cons(y,ys)>:gen_prefix(A, r)) \
-\ <-> (x:A & y:A & <x,y>:r & <xs,ys>:gen_prefix(A, r))";
+"(<Cons(x,xs),Cons(y,ys)> \\<in> gen_prefix(A, r)) \
+\ <-> (x \\<in> A & y \\<in> A & <x,y>:r & <xs,ys> \\<in> gen_prefix(A, r))";
by (auto_tac (claset() addIs [gen_prefix.prepend], simpset()));
qed"Cons_gen_prefix_Cons";
AddIffs [Cons_gen_prefix_Cons];
@@ -88,8 +88,8 @@
by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
by (Clarify_tac 1);
by (etac rev_mp 1);
-by (eres_inst_tac [("P", "y:list(A)")] rev_mp 1);
-by (eres_inst_tac [("P", "xa:list(A)")] rev_mp 1);
+by (eres_inst_tac [("P", "y \\<in> list(A)")] rev_mp 1);
+by (eres_inst_tac [("P", "xa \\<in> list(A)")] rev_mp 1);
by (etac gen_prefix.induct 1);
by (Asm_simp_tac 1);
by (Clarify_tac 1);
@@ -119,8 +119,8 @@
(* Transitivity *)
(* A lemma for proving gen_prefix_trans_comp *)
-Goal "xs:list(A) ==> \
-\ ALL zs. <xs @ ys, zs>:gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
+Goal "xs \\<in> list(A) ==> \
+\ \\<forall>zs. <xs @ ys, zs> \\<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
by (etac list.induct 1);
by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
qed_spec_mp "append_gen_prefix";
@@ -128,10 +128,10 @@
(* Lemma proving transitivity and more*)
Goal "<x, y>: gen_prefix(A, r) ==> \
-\ (ALL z:list(A). <y,z>:gen_prefix(A, s)--><x, z>:gen_prefix(A, s O r))";
+\ (\\<forall>z \\<in> list(A). <y,z> \\<in> gen_prefix(A, s)--><x, z> \\<in> gen_prefix(A, s O r))";
by (etac gen_prefix.induct 1);
by (auto_tac (claset() addEs [ConsE], simpset() addsimps [Nil_gen_prefix]));
-by (subgoal_tac "ys:list(A)" 1);
+by (subgoal_tac "ys \\<in> list(A)" 1);
by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
by (dres_inst_tac [("xs", "ys"), ("r", "s")] append_gen_prefix 1);
by Auto_tac;
@@ -158,9 +158,9 @@
qed "trans_on_gen_prefix";
Goalw [prefix_def]
-"[| <x,y>:prefix(A); <y, z>:gen_prefix(A, r); r<=A*A |] \
-\ ==> <x, z>:gen_prefix(A, r)";
-by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")]
+"[| <x,y> \\<in> prefix(A); <y, z> \\<in> gen_prefix(A, r); r<=A*A |] \
+\ ==> <x, z> \\<in> gen_prefix(A, r)";
+by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")]
(right_comp_id RS subst) 1);
by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
gen_prefix.dom_subset RS subsetD]) 1));
@@ -168,16 +168,16 @@
Goalw [prefix_def]
-"[| <x,y>:gen_prefix(A,r); <y, z>:prefix(A); r<=A*A |] \
-\ ==> <x, z>:gen_prefix(A, r)";
-by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")] (left_comp_id RS subst) 1);
+"[| <x,y> \\<in> gen_prefix(A,r); <y, z> \\<in> prefix(A); r<=A*A |] \
+\ ==> <x, z> \\<in> gen_prefix(A, r)";
+by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")] (left_comp_id RS subst) 1);
by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
gen_prefix.dom_subset RS subsetD]) 1));
qed_spec_mp "gen_prefix_prefix_trans";
(** Antisymmetry **)
-Goal "n:nat ==> ALL b:nat. n #+ b le n --> b = 0";
+Goal "n \\<in> nat ==> \\<forall>b \\<in> nat. n #+ b \\<le> n --> b = 0";
by (induct_tac "n" 1);
by Auto_tac;
qed_spec_mp "nat_le_lemma";
@@ -192,11 +192,11 @@
(*append case is hardest*)
by (Clarify_tac 1);
by (subgoal_tac "length(zs) = 0" 1);
-by (subgoal_tac "ys:list(A)" 1);
+by (subgoal_tac "ys \\<in> list(A)" 1);
by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
-by (dres_inst_tac [("psi", "<ys @ zs, xs>:gen_prefix(A,r)")] asm_rl 1);
+by (dres_inst_tac [("psi", "<ys @ zs, xs> \\<in> gen_prefix(A,r)")] asm_rl 1);
by (Asm_full_simp_tac 1);
-by (subgoal_tac "length(ys @ zs) = length(ys) #+ length(zs) &ys:list(A)&xs:list(A)" 1);
+by (subgoal_tac "length(ys @ zs) = length(ys) #+ length(zs) &ys \\<in> list(A)&xs \\<in> list(A)" 1);
by (blast_tac (claset() addIs [length_app]
addDs [gen_prefix.dom_subset RS subsetD]) 2);
by (REPEAT (dtac gen_prefix_length_le 1));
@@ -209,41 +209,41 @@
(*** recursion equations ***)
-Goal "xs:list(A) ==> <xs, []>:gen_prefix(A,r) <-> (xs = [])";
+Goal "xs \\<in> list(A) ==> <xs, []> \\<in> gen_prefix(A,r) <-> (xs = [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "gen_prefix_Nil";
Addsimps [gen_prefix_Nil];
Goalw [refl_def]
- "[| refl(A, r); xs:list(A) |] ==> \
-\ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs>:gen_prefix(A, r)";
+ "[| refl(A, r); xs \\<in> list(A) |] ==> \
+\ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \\<in> gen_prefix(A, r)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "same_gen_prefix_gen_prefix";
Addsimps [same_gen_prefix_gen_prefix];
-Goal "[| xs:list(A); ys:list(A); y:A |] ==> \
+Goal "[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
\ <xs, Cons(y,ys)> : gen_prefix(A,r) <-> \
-\ (xs=[] | (EX z zs. xs=Cons(z,zs) & z:A & <z,y>:r & <zs,ys>:gen_prefix(A,r)))";
+\ (xs=[] | (\\<exists>z zs. xs=Cons(z,zs) & z \\<in> A & <z,y>:r & <zs,ys> \\<in> gen_prefix(A,r)))";
by (induct_tac "xs" 1);
by Auto_tac;
qed "gen_prefix_Cons";
-Goal "[| refl(A,r); <xs,ys>:gen_prefix(A, r); zs:list(A) |] \
+Goal "[| refl(A,r); <xs,ys> \\<in> gen_prefix(A, r); zs \\<in> list(A) |] \
\ ==> <xs@zs, take(length(xs), ys) @ zs> : gen_prefix(A, r)";
by (etac gen_prefix.induct 1);
by (Asm_simp_tac 1);
by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD]));
by Auto_tac;
by (ftac gen_prefix_length_le 1);
-by (subgoal_tac "take(length(xs), ys):list(A)" 1);
+by (subgoal_tac "take(length(xs), ys) \\<in> list(A)" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps
[diff_is_0_iff RS iffD2, take_type ])));
qed "gen_prefix_take_append";
-Goal "[| refl(A, r); <xs,ys>:gen_prefix(A,r); \
-\ length(xs) = length(ys); zs:list(A) |] \
+Goal "[| refl(A, r); <xs,ys> \\<in> gen_prefix(A,r); \
+\ length(xs) = length(ys); zs \\<in> list(A) |] \
\ ==> <xs@zs, ys @ zs> : gen_prefix(A, r)";
by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1);
by (REPEAT(assume_tac 1));
@@ -254,13 +254,13 @@
qed "gen_prefix_append_both";
(*NOT suitable for rewriting since [y] has the form y#ys*)
-Goal "xs:list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
+Goal "xs \\<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
by (auto_tac (claset(), simpset() addsimps [app_assoc]));
qed "append_cons_conv";
-Goal "[| <xs,ys>:gen_prefix(A, r); refl(A, r) |] \
+Goal "[| <xs,ys> \\<in> gen_prefix(A, r); refl(A, r) |] \
\ ==> length(xs) < length(ys) --> \
-\ <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
+\ <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
by (etac gen_prefix.induct 1);
by (Blast_tac 1);
by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
@@ -290,51 +290,52 @@
val append_one_gen_prefix_lemma = result() RS mp;
Goal "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] \
-\ ==> <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
+\ ==> <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
by (blast_tac (claset() addIs [append_one_gen_prefix_lemma]) 1);
qed "append_one_gen_prefix";
(** Proving the equivalence with Charpentier's definition **)
-Goal "xs:list(A) ==> \
-\ ALL ys:list(A). ALL i:nat. i < length(xs) \
+Goal "xs \\<in> list(A) ==> \
+\ \\<forall>ys \\<in> list(A). \\<forall>i \\<in> nat. i < length(xs) \
\ --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r";
by (induct_tac "xs" 1);
by (ALLGOALS(Clarify_tac));
by (ALLGOALS(Asm_full_simp_tac));
by (etac natE 1);
by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "gen_prefix_imp_nth";
+qed_spec_mp "gen_prefix_imp_nth_lemma";
-Goal "xs:list(A) ==> \
-\ ALL ys:list(A). length(xs) le length(ys) \
-\ --> (ALL i:nat. i < length(xs)--> <nth(i, xs), nth(i,ys)>:r) \
-\ --> <xs, ys> : gen_prefix(A, r)";
+Goal "[| <xs,ys> \\<in> gen_prefix(A,r); i < length(xs)|] \
+\ ==> <nth(i, xs), nth(i, ys)>:r";
+by (cut_inst_tac [("A","A")] gen_prefix.dom_subset 1);
+by (rtac gen_prefix_imp_nth_lemma 1);
+by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat]));
+qed "gen_prefix_imp_nth";
+
+Goal "xs \\<in> list(A) ==> \
+\ \\<forall>ys \\<in> list(A). length(xs) \\<le> length(ys) \
+\ --> (\\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r) \
+\ --> <xs, ys> \\<in> gen_prefix(A, r)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj])));
+by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
-by (eres_inst_tac [("a","ys")] list.elim 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (Clarify_tac 1);
-by (rename_tac "zs" 1);
-by (dres_inst_tac [("x", "zs")] bspec 1);
-by (ALLGOALS(Clarify_tac));
-(*Faster than Auto_tac*)
-by (rtac conjI 1);
-by (REPEAT (Force_tac 1));
+by (eres_inst_tac [("a","ys")] list.elim 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (force_tac (claset() addSIs [nat_0_le], simpset() addsimps [lt_nat_in_nat]) 1);
qed_spec_mp "nth_imp_gen_prefix";
-Goal "(<xs,ys>: gen_prefix(A,r)) <-> \
-\ (xs:list(A) & ys:list(A) & length(xs) le length(ys) & \
-\ (ALL i:nat. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
+Goal "(<xs,ys> : gen_prefix(A,r)) <-> \
+\ (xs \\<in> list(A) & ys \\<in> list(A) & length(xs) \\<le> length(ys) & \
+\ (\\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
by (rtac iffI 1);
by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
by (ftac gen_prefix_length_le 1);
by (ALLGOALS(Clarify_tac));
by (rtac nth_imp_gen_prefix 2);
-by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1);
-by Auto_tac;
+by (dtac gen_prefix_imp_nth 1);
+by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat]));
qed "gen_prefix_iff_nth";
(** prefix is a partial order: **)
@@ -363,44 +364,44 @@
(* Monotonicity of "set" operator WRT prefix *)
Goalw [prefix_def]
-"<xs,ys>:prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
+"<xs,ys> \\<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
by (etac gen_prefix.induct 1);
-by (subgoal_tac "xs:list(A)&ys:list(A)" 3);
+by (subgoal_tac "xs \\<in> list(A)&ys \\<in> list(A)" 3);
by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 4);
by (auto_tac (claset(), simpset() addsimps [set_of_list_append]));
qed "set_of_list_prefix_mono";
(** recursion equations **)
-Goalw [prefix_def] "xs:list(A) ==> <[],xs>:prefix(A)";
+Goalw [prefix_def] "xs \\<in> list(A) ==> <[],xs> \\<in> prefix(A)";
by (asm_simp_tac (simpset() addsimps [Nil_gen_prefix]) 1);
qed "Nil_prefix";
Addsimps[Nil_prefix];
-Goalw [prefix_def] "<xs, []>:prefix(A) <-> (xs = [])";
+Goalw [prefix_def] "<xs, []> \\<in> prefix(A) <-> (xs = [])";
by Auto_tac;
by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (dres_inst_tac [("psi", "<xs, []>:gen_prefix(A, id(A))")] asm_rl 1);
+by (dres_inst_tac [("psi", "<xs, []> \\<in> gen_prefix(A, id(A))")] asm_rl 1);
by (asm_full_simp_tac (simpset() addsimps [gen_prefix_Nil]) 1);
qed "prefix_Nil";
AddIffs [prefix_Nil];
Goalw [prefix_def]
-"<Cons(x,xs), Cons(y,ys)>:prefix(A) <-> (x=y & <xs,ys>:prefix(A) & y:A)";
+"<Cons(x,xs), Cons(y,ys)> \\<in> prefix(A) <-> (x=y & <xs,ys> \\<in> prefix(A) & y \\<in> A)";
by Auto_tac;
qed"Cons_prefix_Cons";
AddIffs [Cons_prefix_Cons];
Goalw [prefix_def]
-"xs:list(A)==> <xs@ys,xs@zs>:prefix(A) <-> (<ys,zs>:prefix(A))";
+"xs \\<in> list(A)==> <xs@ys,xs@zs> \\<in> prefix(A) <-> (<ys,zs> \\<in> prefix(A))";
by (subgoal_tac "refl(A,id(A))" 1);
by (Asm_simp_tac 1);
by (auto_tac (claset(), simpset() addsimps[refl_def]));
qed "same_prefix_prefix";
Addsimps [same_prefix_prefix];
-Goal "xs:list(A) ==> <xs@ys,xs>:prefix(A) <-> (<ys,[]>:prefix(A))";
+Goal "xs \\<in> list(A) ==> <xs@ys,xs> \\<in> prefix(A) <-> (<ys,[]> \\<in> prefix(A))";
by (res_inst_tac [("P", "%x. <?u, x>:?v <-> ?w(x)")] (app_right_Nil RS subst) 1);
by (rtac same_prefix_prefix 2);
by Auto_tac;
@@ -408,37 +409,37 @@
Addsimps [same_prefix_prefix_Nil];
Goalw [prefix_def]
-"[| <xs,ys>:prefix(A); zs:list(A) |] ==> <xs,ys@zs>:prefix(A)";
+"[| <xs,ys> \\<in> prefix(A); zs \\<in> list(A) |] ==> <xs,ys@zs> \\<in> prefix(A)";
by (etac gen_prefix.append 1);
by (assume_tac 1);
qed "prefix_appendI";
Addsimps [prefix_appendI];
Goalw [prefix_def]
-"[| xs:list(A); ys:list(A); y:A |] ==> \
-\ <xs,Cons(y,ys)>:prefix(A) <-> \
-\ (xs=[] | (EX zs. xs=Cons(y,zs) & <zs,ys>:prefix(A)))";
+"[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
+\ <xs,Cons(y,ys)> \\<in> prefix(A) <-> \
+\ (xs=[] | (\\<exists>zs. xs=Cons(y,zs) & <zs,ys> \\<in> prefix(A)))";
by (auto_tac (claset(), simpset() addsimps [gen_prefix_Cons]));
qed "prefix_Cons";
Goalw [prefix_def]
- "[| <xs,ys>:prefix(A); length(xs) < length(ys) |] \
-\ ==> <xs @ [nth(length(xs),ys)], ys>:prefix(A)";
+ "[| <xs,ys> \\<in> prefix(A); length(xs) < length(ys) |] \
+\ ==> <xs @ [nth(length(xs),ys)], ys> \\<in> prefix(A)";
by (subgoal_tac "refl(A, id(A))" 1);
by (asm_simp_tac (simpset() addsimps [append_one_gen_prefix]) 1);
by (auto_tac (claset(), simpset() addsimps [refl_def]));
qed "append_one_prefix";
Goalw [prefix_def]
-"<xs,ys>:prefix(A) ==> length(xs) le length(ys)";
+"<xs,ys> \\<in> prefix(A) ==> length(xs) \\<le> length(ys)";
by (blast_tac (claset() addDs [gen_prefix_length_le]) 1);
qed "prefix_length_le";
Goalw [prefix_def]
-"<xs,ys>:prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
+"<xs,ys> \\<in> prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
by (etac gen_prefix.induct 1);
by (Clarify_tac 1);
-by (ALLGOALS(subgoal_tac "ys:list(A)&xs:list(A)"));
+by (ALLGOALS(subgoal_tac "ys \\<in> list(A)&xs \\<in> list(A)"));
by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
simpset() addsimps [length_app, length_type]));
by (subgoal_tac "length(zs)=0" 1);
@@ -465,12 +466,11 @@
(*Equivalence to the definition used in Lex/Prefix.thy*)
Goalw [prefix_def]
-"<xs,zs>:prefix(A) <-> (EX ys:list(A). zs = xs@ys) & xs:list(A)";
+ "<xs,zs> \\<in> prefix(A) <-> (\\<exists>ys \\<in> list(A). zs = xs@ys) & xs \\<in> list(A)";
by (auto_tac (claset(),
- simpset() addsimps [gen_prefix_iff_nth,
+ simpset() addsimps [gen_prefix_iff_nth, lt_nat_in_nat,
nth_append, nth_type, app_type, length_app]));
-by (subgoal_tac "length(xs):nat&length(zs):nat & \
-\ drop(length(xs), zs):list(A)" 1);
+by (subgoal_tac "drop(length(xs), zs) \\<in> list(A)" 1);
by (res_inst_tac [("x", "drop(length(xs), zs)")] bexI 1);
by (ALLGOALS(Clarify_tac));
by (asm_simp_tac (simpset() addsimps [length_type, drop_type]) 2);
@@ -483,17 +483,14 @@
by (dres_inst_tac [("i", "length(zs)")] leI 1);
by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1);
by Safe_tac;
-by (Blast_tac 1);
by (subgoal_tac "length(xs) #+ (i #- length(xs)) = i" 1);
by (stac nth_drop 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI])));
-by (rtac (nat_diff_split RS iffD2) 1);
-by Auto_tac;
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI] addsplits [nat_diff_split])));
qed "prefix_iff";
Goal
-"[|xs:list(A); ys:list(A); y:A |] ==> \
-\ <xs, ys@[y]>:prefix(A) <-> (xs = ys@[y] | <xs,ys>:prefix(A))";
+"[|xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
+\ <xs, ys@[y]> \\<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \\<in> prefix(A))";
by (simp_tac (simpset() addsimps [prefix_iff]) 1);
by (rtac iffI 1);
by (Clarify_tac 1);
@@ -504,9 +501,9 @@
qed "prefix_snoc";
Addsimps [prefix_snoc];
-Goal "zs:list(A) ==> ALL xs:list(A). ALL ys:list(A). \
-\ (<xs, ys@zs>:prefix(A)) <-> \
-\ (<xs,ys>:prefix(A) | (EX us. xs = ys@us & <us,zs>:prefix(A)))";
+Goal "zs \\<in> list(A) ==> \\<forall>xs \\<in> list(A). \\<forall>ys \\<in> list(A). \
+\ (<xs, ys@zs> \\<in> prefix(A)) <-> \
+\ (<xs,ys> \\<in> prefix(A) | (\\<exists>us. xs = ys@us & <us,zs> \\<in> prefix(A)))";
by (etac list_append_induct 1);
by (Clarify_tac 2);
by (rtac iffI 2);
@@ -521,9 +518,9 @@
(*Although the prefix ordering is not linear, the prefixes of a list
are linearly ordered.*)
-Goal "[| zs:list(A); xs:list(A); ys:list(A) |] \
-\ ==> <xs, zs>:prefix(A) --> <ys,zs>:prefix(A) \
-\ --><xs,ys>:prefix(A) | <ys,xs>:prefix(A)";
+Goal "[| zs \\<in> list(A); xs \\<in> list(A); ys \\<in> list(A) |] \
+\ ==> <xs, zs> \\<in> prefix(A) --> <ys,zs> \\<in> prefix(A) \
+\ --><xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
by (etac list_append_induct 1);
by Auto_tac;
qed_spec_mp "common_prefix_linear";
@@ -562,7 +559,7 @@
qed "part_order_Le";
Addsimps [part_order_Le];
-Goal "x:list(nat) ==> x pfixLe x";
+Goal "x \\<in> list(nat) ==> x pfixLe x";
by (blast_tac (claset() addIs [refl_gen_prefix RS reflD, refl_Le]) 1);
qed "pfixLe_refl";
Addsimps[pfixLe_refl];
@@ -597,7 +594,7 @@
qed "trans_Ge";
AddIffs [trans_Ge];
-Goal "x:list(nat) ==> x pfixGe x";
+Goal "x \\<in> list(nat) ==> x pfixGe x";
by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1);
qed "pfixGe_refl";
Addsimps[pfixGe_refl];
@@ -618,7 +615,7 @@
(* Added by Sidi: prefix and take *)
Goalw [prefix_def]
-"<xs, ys>:prefix(A) ==> xs=take(length(xs), ys)";
+"<xs, ys> \\<in> prefix(A) ==> xs = take(length(xs), ys)";
by (etac gen_prefix.induct 1);
by (subgoal_tac "length(xs):nat" 3);
by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
@@ -630,8 +627,20 @@
by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_is_0_iff])));
qed "prefix_imp_take";
-Goalw [prefix_def]
-"xs:list(A) ==> ALL n:nat. <take(n, xs), xs>:prefix(A)";
+Goal "[|<xs,ys> \\<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys";
+by (cut_inst_tac [("A","A")] prefix_type 1);
+by (dtac subsetD 1);
+by Auto_tac;
+by (dtac prefix_imp_take 1);
+by (etac trans 1);
+by (Asm_full_simp_tac 1);
+qed "prefix_length_equal";
+
+Goal "[|<xs,ys> \\<in> prefix(A); length(ys) \\<le> length(xs)|] ==> xs = ys";
+by (blast_tac (claset() addIs [prefix_length_equal, le_anti_sym, prefix_length_le]) 1);
+qed "prefix_length_le_equal";
+
+Goalw [prefix_def] "xs \\<in> list(A) ==> \\<forall>n \\<in> nat. <take(n, xs), xs> \\<in> prefix(A)";
by (etac list.induct 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
@@ -639,7 +648,7 @@
by Auto_tac;
qed_spec_mp "take_prefix";
-Goal "<xs, ys>:prefix(A) <-> (xs=take(length(xs), ys) & xs:list(A) & ys:list(A))";
+Goal "<xs,ys> \\<in> prefix(A) <-> (xs=take(length(xs), ys) & xs \\<in> list(A) & ys \\<in> list(A))";
by (rtac iffI 1);
by (forward_tac [prefix_type RS subsetD] 1);
by (blast_tac (claset() addIs [prefix_imp_take]) 1);
@@ -647,3 +656,29 @@
by (etac ssubst 1);
by (blast_tac (claset() addIs [take_prefix, length_type]) 1);
qed "prefix_take_iff";
+
+Goal "[| <xs,ys> \\<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)";
+by (auto_tac (claset() addSDs [gen_prefix_imp_nth],
+ simpset() addsimps [prefix_def]));
+qed "prefix_imp_nth";
+
+val prems = Goal "[|xs \\<in> list(A); ys \\<in> list(A); length(xs) \\<le> length(ys); \
+\ !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|] \
+\ ==> <xs,ys> \\<in> prefix(A)";
+by (auto_tac (claset(), simpset() addsimps prems@[prefix_def, nth_imp_gen_prefix]));
+by (auto_tac (claset() addSIs [nth_imp_gen_prefix], simpset() addsimps prems@[prefix_def]));
+by (blast_tac (claset() addIs prems@[nth_type, lt_trans2]) 1);
+qed "nth_imp_prefix";
+
+
+Goal "[|length(xs) \\<le> length(ys); \
+\ <xs,zs> \\<in> prefix(A); <ys,zs> \\<in> prefix(A)|] ==> <xs,ys> \\<in> prefix(A)";
+by (cut_inst_tac [("A","A")] prefix_type 1);
+by (rtac nth_imp_prefix 1);
+ by (blast_tac (claset() addIs []) 1);
+ by (blast_tac (claset() addIs []) 1);
+ by (assume_tac 1);
+by (res_inst_tac [("b","nth(i,zs)")] trans 1);
+ by (blast_tac (claset() addIs [prefix_imp_nth]) 1);
+by (blast_tac (claset() addIs [sym, prefix_imp_nth, prefix_length_le, lt_trans2]) 1);
+qed "length_le_prefix_imp_prefix";
\ No newline at end of file
--- a/src/ZF/UNITY/ROOT.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/ROOT.ML Fri Jun 20 12:10:45 2003 +0200
@@ -20,3 +20,4 @@
time_use_thy "Distributor";
time_use_thy "Merge";
time_use_thy "ClientImpl";
+time_use_thy "AllocImpl";
--- a/src/ZF/UNITY/UNITY.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/UNITY.ML Fri Jun 20 12:10:45 2003 +0200
@@ -511,9 +511,9 @@
Goalw [constrains_def, st_set_def]
"[| F:A co A' |] ==> A <= A'";
-by Auto_tac;
-by (Blast_tac 1);
+by (Force_tac 1);
qed "constrains_imp_subset";
+
(*The reasoning is by subsets since "co" refers to single actions
only. So this rule isn't that useful.*)
--- a/src/ZF/UNITY/UNITYMisc.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.ML Fri Jun 20 12:10:45 2003 +0200
@@ -51,6 +51,8 @@
AddIffs [Collect_Int2, Collect_Int3];
+(*for main ZF????*)
+
Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
by Auto_tac;
qed "Collect_disj_eq";
@@ -70,3 +72,8 @@
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";
+
+Goal "cons(a,B) Int A = (if a : A then cons(a, A Int B) else A Int B)";
+by Auto_tac;
+qed "Int_cons_left";
+
--- a/src/ZF/UNITY/WFair.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML Fri Jun 20 12:10:45 2003 +0200
@@ -19,14 +19,12 @@
by Auto_tac;
qed "transientD2";
-Goalw [stable_def, constrains_def, transient_def]
- "[| F : stable(A); F : transient(A) |] ==> A = 0";
-by (Asm_full_simp_tac 1);
-by (Blast.depth_tac (claset()) 10 1);
+Goal "[| F : stable(A); F : transient(A) |] ==> A = 0";
+by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1);
+by (Fast_tac 1);
qed "stable_transient_empty";
-Goalw [transient_def, st_set_def]
-"[|F:transient(A); B<=A|] ==> F:transient(B)";
+Goalw [transient_def, st_set_def] "[|F:transient(A); B<=A|] ==> F:transient(B)";
by Safe_tac;
by (res_inst_tac [("x", "act")] bexI 1);
by (ALLGOALS(Asm_full_simp_tac));
@@ -609,7 +607,6 @@
\ F : (A1 - B) co (A1 Un B); \
\ F : (A2 - C) co (A2 Un C) |] \
\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
-by (Clarify_tac 1);
by (Blast_tac 1);
qed "leadsTo_123_aux";