Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
authorpaulson
Fri Jun 20 12:10:45 2003 +0200 (2003-06-20)
changeset 14060c0c4af41fa3b
parent 14059 5c457e25c95f
child 14061 abcb32a7b212
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/IMP/Equiv.thy
src/ZF/IsaMakefile
src/ZF/Perm.thy
src/ZF/UNITY/AllocBase.ML
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/ClientImpl.ML
src/ZF/UNITY/Constrains.ML
src/ZF/UNITY/GenPrefix.ML
src/ZF/UNITY/ROOT.ML
src/ZF/UNITY/UNITY.ML
src/ZF/UNITY/UNITYMisc.ML
src/ZF/UNITY/WFair.ML
     1.1 --- a/src/ZF/Arith.thy	Thu Jun 19 18:40:39 2003 +0200
     1.2 +++ b/src/ZF/Arith.thy	Fri Jun 20 12:10:45 2003 +0200
     1.3 @@ -78,12 +78,12 @@
     1.4          nat_0_le [simp]
     1.5  
     1.6  
     1.7 -lemma zero_lt_lemma: "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)"
     1.8 +lemma zero_lt_lemma: "[| 0<k; k \<in> nat |] ==> \<exists>j\<in>nat. k = succ(j)"
     1.9  apply (erule rev_mp)
    1.10  apply (induct_tac "k", auto)
    1.11  done
    1.12  
    1.13 -(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.14 +(* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.15  lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
    1.16  
    1.17  
    1.18 @@ -98,21 +98,21 @@
    1.19  lemma natify_0 [simp]: "natify(0) = 0"
    1.20  by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
    1.21  
    1.22 -lemma natify_non_succ: "ALL z. x ~= succ(z) ==> natify(x) = 0"
    1.23 +lemma natify_non_succ: "\<forall>z. x ~= succ(z) ==> natify(x) = 0"
    1.24  by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
    1.25  
    1.26 -lemma natify_in_nat [iff,TC]: "natify(x) : nat"
    1.27 +lemma natify_in_nat [iff,TC]: "natify(x) \<in> nat"
    1.28  apply (rule_tac a=x in eps_induct)
    1.29 -apply (case_tac "EX z. x = succ(z)")
    1.30 +apply (case_tac "\<exists>z. x = succ(z)")
    1.31  apply (auto simp add: natify_succ natify_non_succ)
    1.32  done
    1.33  
    1.34 -lemma natify_ident [simp]: "n : nat ==> natify(n) = n"
    1.35 +lemma natify_ident [simp]: "n \<in> nat ==> natify(n) = n"
    1.36  apply (induct_tac "n")
    1.37  apply (auto simp add: natify_succ)
    1.38  done
    1.39  
    1.40 -lemma natify_eqE: "[|natify(x) = y;  x: nat|] ==> x=y"
    1.41 +lemma natify_eqE: "[|natify(x) = y;  x \<in> nat|] ==> x=y"
    1.42  by auto
    1.43  
    1.44  
    1.45 @@ -167,29 +167,29 @@
    1.46  
    1.47  (** Addition **)
    1.48  
    1.49 -lemma raw_add_type: "[| m:nat;  n:nat |] ==> raw_add (m, n) : nat"
    1.50 +lemma raw_add_type: "[| m\<in>nat;  n\<in>nat |] ==> raw_add (m, n) \<in> nat"
    1.51  by (induct_tac "m", auto)
    1.52  
    1.53 -lemma add_type [iff,TC]: "m #+ n : nat"
    1.54 +lemma add_type [iff,TC]: "m #+ n \<in> nat"
    1.55  by (simp add: add_def raw_add_type)
    1.56  
    1.57  (** Multiplication **)
    1.58  
    1.59 -lemma raw_mult_type: "[| m:nat;  n:nat |] ==> raw_mult (m, n) : nat"
    1.60 +lemma raw_mult_type: "[| m\<in>nat;  n\<in>nat |] ==> raw_mult (m, n) \<in> nat"
    1.61  apply (induct_tac "m")
    1.62  apply (simp_all add: raw_add_type)
    1.63  done
    1.64  
    1.65 -lemma mult_type [iff,TC]: "m #* n : nat"
    1.66 +lemma mult_type [iff,TC]: "m #* n \<in> nat"
    1.67  by (simp add: mult_def raw_mult_type)
    1.68  
    1.69  
    1.70  (** Difference **)
    1.71  
    1.72 -lemma raw_diff_type: "[| m:nat;  n:nat |] ==> raw_diff (m, n) : nat"
    1.73 +lemma raw_diff_type: "[| m\<in>nat;  n\<in>nat |] ==> raw_diff (m, n) \<in> nat"
    1.74  by (induct_tac "n", auto)
    1.75  
    1.76 -lemma diff_type [iff,TC]: "m #- n : nat"
    1.77 +lemma diff_type [iff,TC]: "m #- n \<in> nat"
    1.78  by (simp add: diff_def raw_diff_type)
    1.79  
    1.80  lemma diff_0_eq_0 [simp]: "0 #- n = 0"
    1.81 @@ -210,7 +210,7 @@
    1.82  lemma diff_0 [simp]: "m #- 0 = natify(m)"
    1.83  by (simp add: diff_def)
    1.84  
    1.85 -lemma diff_le_self: "m:nat ==> (m #- n) le m"
    1.86 +lemma diff_le_self: "m\<in>nat ==> (m #- n) le m"
    1.87  apply (subgoal_tac " (m #- natify (n)) le m")
    1.88  apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
    1.89  apply (erule_tac [6] leE)
    1.90 @@ -227,7 +227,7 @@
    1.91  lemma add_succ [simp]: "succ(m) #+ n = succ(m #+ n)"
    1.92  by (simp add: natify_succ add_def)
    1.93  
    1.94 -lemma add_0: "m: nat ==> 0 #+ m = m"
    1.95 +lemma add_0: "m \<in> nat ==> 0 #+ m = m"
    1.96  by simp
    1.97  
    1.98  (*Associative law for addition*)
    1.99 @@ -252,7 +252,7 @@
   1.100  apply (auto simp add: natify_succ)
   1.101  done
   1.102  
   1.103 -lemma add_0_right: "m: nat ==> m #+ 0 = m"
   1.104 +lemma add_0_right: "m \<in> nat ==> m #+ 0 = m"
   1.105  by auto
   1.106  
   1.107  (*Commutative law for addition*)
   1.108 @@ -274,7 +274,7 @@
   1.109  
   1.110  (*Cancellation law on the left*)
   1.111  lemma raw_add_left_cancel:
   1.112 -     "[| raw_add(k, m) = raw_add(k, n);  k:nat |] ==> m=n"
   1.113 +     "[| raw_add(k, m) = raw_add(k, n);  k\<in>nat |] ==> m=n"
   1.114  apply (erule rev_mp)
   1.115  apply (induct_tac "k", auto)
   1.116  done
   1.117 @@ -285,7 +285,7 @@
   1.118  done
   1.119  
   1.120  lemma add_left_cancel:
   1.121 -     "[| i = j;  i #+ m = j #+ n;  m:nat;  n:nat |] ==> m = n"
   1.122 +     "[| i = j;  i #+ m = j #+ n;  m\<in>nat;  n\<in>nat |] ==> m = n"
   1.123  by (force dest!: add_left_cancel_natify)
   1.124  
   1.125  (*Thanks to Sten Agerholm*)
   1.126 @@ -295,7 +295,7 @@
   1.127  apply auto
   1.128  done
   1.129  
   1.130 -lemma add_le_elim1: "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n"
   1.131 +lemma add_le_elim1: "[| k#+m le k#+n; m \<in> nat; n \<in> nat |] ==> m le n"
   1.132  by (drule add_le_elim1_natify, auto)
   1.133  
   1.134  lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)"
   1.135 @@ -304,29 +304,26 @@
   1.136  apply auto
   1.137  done
   1.138  
   1.139 -lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n"
   1.140 +lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
   1.141  by (drule add_lt_elim1_natify, auto)
   1.142  
   1.143  
   1.144  subsection{*Monotonicity of Addition*}
   1.145  
   1.146  (*strict, in 1st argument; proof is by rule induction on 'less than'.
   1.147 -  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   1.148 -  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   1.149 -lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k"
   1.150 +  Still need j\<in>nat, for consider j = omega.  Then we can have i<omega,
   1.151 +  which is the same as i\<in>nat, but natify(j)=0, so the conclusion fails.*)
   1.152 +lemma add_lt_mono1: "[| i<j; j\<in>nat |] ==> i#+k < j#+k"
   1.153  apply (frule lt_nat_in_nat, assumption)
   1.154  apply (erule succ_lt_induct)
   1.155  apply (simp_all add: leI)
   1.156  done
   1.157  
   1.158 -(*strict, in both arguments*)
   1.159 -lemma add_lt_mono:
   1.160 - "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"
   1.161 -apply (rule add_lt_mono1 [THEN lt_trans], assumption+)
   1.162 -apply (subst add_commute, subst add_commute, rule add_lt_mono1, assumption+)
   1.163 -done
   1.164 +text{*strict, in second argument*}
   1.165 +lemma add_lt_mono2: "[| i<j; j\<in>nat |] ==> k#+i < k#+j"
   1.166 +by (simp add: add_commute [of k] add_lt_mono1)
   1.167  
   1.168 -(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.169 +text{*A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity*}
   1.170  lemma Ord_lt_mono_imp_le_mono:
   1.171    assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
   1.172        and ford:    "!!i. i:k ==> Ord(f(i))"
   1.173 @@ -337,18 +334,34 @@
   1.174  apply (blast intro!: leCI lt_mono ford elim!: leE)
   1.175  done
   1.176  
   1.177 -(*le monotonicity, 1st argument*)
   1.178 -lemma add_le_mono1: "[| i le j; j:nat |] ==> i#+k le j#+k"
   1.179 +text{*@{text "\<le>"} monotonicity, 1st argument*}
   1.180 +lemma add_le_mono1: "[| i le j; j\<in>nat |] ==> i#+k le j#+k"
   1.181  apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck) 
   1.182  apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
   1.183  done
   1.184  
   1.185 -(* le monotonicity, BOTH arguments*)
   1.186 -lemma add_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"
   1.187 +text{*@{text "\<le>"} monotonicity, both arguments*}
   1.188 +lemma add_le_mono: "[| i le j; k le l; j\<in>nat; l\<in>nat |] ==> i#+k le j#+l"
   1.189  apply (rule add_le_mono1 [THEN le_trans], assumption+)
   1.190  apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
   1.191  done
   1.192  
   1.193 +text{*Combinations of less-than and less-than-or-equals*}
   1.194 +
   1.195 +lemma add_lt_le_mono: "[| i<j; k\<le>l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
   1.196 +apply (rule add_lt_mono1 [THEN lt_trans2], assumption+)
   1.197 +apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
   1.198 +done
   1.199 +
   1.200 +lemma add_le_lt_mono: "[| i\<le>j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
   1.201 +by (subst add_commute, subst add_commute, erule add_lt_le_mono, assumption+)
   1.202 +
   1.203 +text{*Less-than: in other words, strict in both arguments*}
   1.204 +lemma add_lt_mono: "[| i<j; k<l; j\<in>nat; l\<in>nat |] ==> i#+k < j#+l"
   1.205 +apply (rule add_lt_le_mono) 
   1.206 +apply (auto intro: leI) 
   1.207 +done
   1.208 +
   1.209  (** Subtraction is the inverse of addition. **)
   1.210  
   1.211  lemma diff_add_inverse: "(n#+m) #- n = natify(m)"
   1.212 @@ -474,10 +487,10 @@
   1.213  lemma mult_1_right_natify [simp]: "n #* 1 = natify(n)"
   1.214  by auto
   1.215  
   1.216 -lemma mult_1: "n : nat ==> 1 #* n = n"
   1.217 +lemma mult_1: "n \<in> nat ==> 1 #* n = n"
   1.218  by simp
   1.219  
   1.220 -lemma mult_1_right: "n : nat ==> n #* 1 = n"
   1.221 +lemma mult_1_right: "n \<in> nat ==> n #* 1 = n"
   1.222  by simp
   1.223  
   1.224  (*Commutative law for multiplication*)
   1.225 @@ -522,12 +535,12 @@
   1.226  
   1.227  
   1.228  lemma lt_succ_eq_0_disj:
   1.229 -     "[| m:nat; n:nat |]
   1.230 -      ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))"
   1.231 +     "[| m\<in>nat; n\<in>nat |]
   1.232 +      ==> (m < succ(n)) <-> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
   1.233  by (induct_tac "m", auto)
   1.234  
   1.235  lemma less_diff_conv [rule_format]:
   1.236 -     "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
   1.237 +     "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) <-> (i #+ k < j)"
   1.238  by (erule_tac m = k in diff_induct, auto)
   1.239  
   1.240  lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
   1.241 @@ -586,6 +599,7 @@
   1.242  val add_lt_elim1_natify = thm "add_lt_elim1_natify";
   1.243  val add_lt_elim1 = thm "add_lt_elim1";
   1.244  val add_lt_mono1 = thm "add_lt_mono1";
   1.245 +val add_lt_mono2 = thm "add_lt_mono2";
   1.246  val add_lt_mono = thm "add_lt_mono";
   1.247  val Ord_lt_mono_imp_le_mono = thm "Ord_lt_mono_imp_le_mono";
   1.248  val add_le_mono1 = thm "add_le_mono1";
     2.1 --- a/src/ZF/ArithSimp.thy	Thu Jun 19 18:40:39 2003 +0200
     2.2 +++ b/src/ZF/ArithSimp.thy	Fri Jun 20 12:10:45 2003 +0200
     2.3 @@ -534,6 +534,34 @@
     2.4  apply simp_all
     2.5  done
     2.6  
     2.7 +text{*Difference and less-than*}
     2.8 +
     2.9 +lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i"
    2.10 +apply (erule rev_mp)
    2.11 +apply (simp split add: nat_diff_split, auto)
    2.12 + apply (blast intro: add_le_self lt_trans1)
    2.13 +apply (rule not_le_iff_lt [THEN iffD1], auto)
    2.14 +apply (subgoal_tac "i #+ da < j #+ d", force)
    2.15 +apply (blast intro: add_le_lt_mono) 
    2.16 +done
    2.17 +
    2.18 +lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)" 
    2.19 +apply (frule le_in_nat, assumption)
    2.20 +apply (frule lt_nat_in_nat, assumption)
    2.21 +apply (simp split add: nat_diff_split, auto)
    2.22 +  apply (blast intro: lt_asym lt_trans2)
    2.23 + apply (blast intro: lt_irrefl lt_trans2)
    2.24 +apply (rule not_le_iff_lt [THEN iffD1], auto)
    2.25 +apply (subgoal_tac "j #+ d < i #+ da", force)
    2.26 +apply (blast intro: add_lt_le_mono) 
    2.27 +done
    2.28 +
    2.29 +
    2.30 +lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i"
    2.31 +apply (frule le_in_nat, assumption)
    2.32 +apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt) 
    2.33 +done
    2.34 +
    2.35  
    2.36  ML
    2.37  {*
    2.38 @@ -607,6 +635,8 @@
    2.39  
    2.40  val add_lt_elim2 = thm "add_lt_elim2";
    2.41  val add_le_elim2 = thm "add_le_elim2";
    2.42 +
    2.43 +val diff_lt_iff_lt = thm "diff_lt_iff_lt";
    2.44  *}
    2.45  
    2.46  end
     3.1 --- a/src/ZF/IMP/Equiv.thy	Thu Jun 19 18:40:39 2003 +0200
     3.2 +++ b/src/ZF/IMP/Equiv.thy	Fri Jun 20 12:10:45 2003 +0200
     3.3 @@ -39,8 +39,6 @@
     3.4  lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
     3.5    apply (erule evalc.induct)
     3.6          apply (simp_all (no_asm_simp))
     3.7 -      txt {* @{text skip} *}
     3.8 -      apply fast
     3.9       txt {* @{text assign} *}
    3.10       apply (simp add: update_type)
    3.11      txt {* @{text comp} *}
    3.12 @@ -48,7 +46,6 @@
    3.13     txt {* @{text while} *}
    3.14     apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
    3.15     apply (simp add: Gamma_def)
    3.16 -   apply force
    3.17    txt {* recursive case of @{text while} *}
    3.18    apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
    3.19    apply (auto simp add: Gamma_def)
     4.1 --- a/src/ZF/IsaMakefile	Thu Jun 19 18:40:39 2003 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Fri Jun 20 12:10:45 2003 +0200
     4.3 @@ -120,7 +120,7 @@
     4.4    UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
     4.5    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     4.6    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
     4.7 -  UNITY/AllocBase.ML UNITY/AllocBase.thy\
     4.8 +  UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     4.9    UNITY/ClientImpl.ML UNITY/ClientImpl.thy\
    4.10    UNITY/Distributor.ML UNITY/Distributor.thy\
    4.11    UNITY/Follows.ML UNITY/Follows.thy\
     5.1 --- a/src/ZF/Perm.thy	Thu Jun 19 18:40:39 2003 +0200
     5.2 +++ b/src/ZF/Perm.thy	Fri Jun 20 12:10:45 2003 +0200
     5.3 @@ -195,8 +195,13 @@
     5.4  apply (force intro!: lam_type dest: apply_type)
     5.5  done
     5.6  
     5.7 +text{*@{term id} as the identity relation*}
     5.8 +lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
     5.9 +by auto
    5.10  
    5.11 -(*** Converse of a function ***)
    5.12 +
    5.13 +
    5.14 +subsection{*Converse of a Function*}
    5.15  
    5.16  lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A"
    5.17  apply (unfold inj_def)
    5.18 @@ -208,7 +213,7 @@
    5.19  
    5.20  (** Equations for converse(f) **)
    5.21  
    5.22 -(*The premises are equivalent to saying that f is injective...*) 
    5.23 +text{*The premises are equivalent to saying that f is injective...*}
    5.24  lemma left_inverse_lemma:
    5.25       "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a"
    5.26  by (blast intro: apply_Pair apply_equality converseI)
     6.1 --- a/src/ZF/UNITY/AllocBase.ML	Thu Jun 19 18:40:39 2003 +0200
     6.2 +++ b/src/ZF/UNITY/AllocBase.ML	Fri Jun 20 12:10:45 2003 +0200
     6.3 @@ -15,20 +15,20 @@
     6.4  qed "Nclients_NbT_gt_0";
     6.5  Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
     6.6  
     6.7 -Goal "Nclients ~= 0 & NbT ~= 0";
     6.8 +Goal "Nclients \\<noteq> 0 & NbT \\<noteq> 0";
     6.9  by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    6.10  by Auto_tac;
    6.11  qed "Nclients_NbT_not_0";
    6.12  Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0  RS conjunct2];
    6.13  
    6.14 -Goal "Nclients:nat & NbT:nat";
    6.15 +Goal "Nclients\\<in>nat & NbT\\<in>nat";
    6.16  by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    6.17  by Auto_tac;
    6.18  qed "Nclients_NbT_type";
    6.19  Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    6.20  AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    6.21  
    6.22 -Goal "b:Inter(RepFun(Nclients, B)) <-> (ALL x:Nclients. b:B(x))";
    6.23 +Goal "b\\<in>Inter(RepFun(Nclients, B)) <-> (\\<forall>x\\<in>Nclients. b\\<in>B(x))";
    6.24  by (auto_tac (claset(), simpset() addsimps [INT_iff]));
    6.25  by (res_inst_tac [("x", "0")] exI 1);
    6.26  by (rtac ltD 1); 
    6.27 @@ -38,15 +38,15 @@
    6.28  
    6.29  val succ_def = thm "succ_def";
    6.30  
    6.31 -Goal "n:nat ==> \
    6.32 -\     (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
    6.33 +Goal "n\\<in>nat ==> \
    6.34 +\     (\\<forall>i\\<in>nat. i<n --> f(i) $<= g(i)) --> \
    6.35  \     setsum(f, n) $<= setsum(g,n)";
    6.36  by (induct_tac "n" 1);
    6.37  by (ALLGOALS Asm_full_simp_tac);
    6.38 -by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
    6.39 +by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x\\<notin>x" 1);
    6.40  by (Clarify_tac 1);
    6.41  by (Asm_simp_tac 1);
    6.42 -by (subgoal_tac "ALL i:nat. i<x--> f(i) $<= g(i)" 1);
    6.43 +by (subgoal_tac "\\<forall>i\\<in>nat. i<x--> f(i) $<= g(i)" 1);
    6.44  by (resolve_tac [zadd_zle_mono] 1);
    6.45  by (thin_tac "succ(x)=cons(x,x)" 1);
    6.46  by (ALLGOALS(Asm_simp_tac));
    6.47 @@ -57,22 +57,22 @@
    6.48  by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
    6.49  qed_spec_mp "setsum_fun_mono";
    6.50  
    6.51 -Goal "l:list(A) ==> tokens(l):nat";
    6.52 +Goal "l\\<in>list(A) ==> tokens(l)\\<in>nat";
    6.53  by (etac list.induct 1);
    6.54  by Auto_tac;
    6.55  qed "tokens_type";
    6.56  AddTCs [tokens_type];
    6.57  Addsimps [tokens_type];
    6.58  
    6.59 -Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
    6.60 -\  --> tokens(xs) le tokens(ys)";
    6.61 +Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
    6.62 +\  --> tokens(xs) \\<le> tokens(ys)";
    6.63  by (induct_tac "xs" 1);
    6.64  by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], 
    6.65                simpset() addsimps [prefix_def]));
    6.66  qed_spec_mp "tokens_mono_aux";
    6.67  
    6.68 -Goal "[| <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
    6.69 -\     tokens(xs) le tokens(ys)";
    6.70 +Goal "<xs, ys>\\<in>prefix(A) ==> tokens(xs) \\<le> tokens(ys)";
    6.71 +by (cut_facts_tac [prefix_type] 1);
    6.72  by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
    6.73  qed "tokens_mono";
    6.74  
    6.75 @@ -84,13 +84,13 @@
    6.76  AddIs [mono_tokens];
    6.77  
    6.78  Goal 
    6.79 -"[| xs:list(A); ys:list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
    6.80 +"[| xs\\<in>list(A); ys\\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
    6.81  by (induct_tac "xs" 1);
    6.82  by Auto_tac;
    6.83  qed "tokens_append";
    6.84  Addsimps [tokens_append];
    6.85  
    6.86 -Goal "l:list(A) ==> ALL n:nat. length(take(n, l))=min(n, length(l))";
    6.87 +Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
    6.88  by (induct_tac "l" 1);
    6.89  by Safe_tac;
    6.90  by (ALLGOALS(Asm_simp_tac));
    6.91 @@ -100,27 +100,27 @@
    6.92  
    6.93  (** bag_of **)
    6.94  
    6.95 -Goal "l:list(A) ==>bag_of(l):Mult(A)";
    6.96 +Goal "l\\<in>list(A) ==>bag_of(l)\\<in>Mult(A)";
    6.97  by (induct_tac "l" 1);
    6.98  by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
    6.99  qed "bag_of_type";
   6.100  AddTCs [bag_of_type];
   6.101  Addsimps [bag_of_type];
   6.102  
   6.103 -Goal "l:list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
   6.104 +Goal "l\\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
   6.105  by (dtac bag_of_type 1);
   6.106  by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   6.107  qed "bag_of_multiset";
   6.108  
   6.109 -Goal "[| xs:list(A); ys:list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
   6.110 +Goal "[| xs\\<in>list(A); ys\\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
   6.111  by (induct_tac "xs" 1);
   6.112  by (auto_tac (claset(), simpset() 
   6.113         addsimps [bag_of_multiset, munion_assoc]));
   6.114  qed "bag_of_append";
   6.115  Addsimps [bag_of_append];
   6.116  
   6.117 -Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
   6.118 -\  --> <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
   6.119 +Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
   6.120 +\  --> <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
   6.121  by (induct_tac "xs" 1);
   6.122  by (ALLGOALS(Clarify_tac));
   6.123  by (ftac bag_of_multiset 1);
   6.124 @@ -133,8 +133,8 @@
   6.125  by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
   6.126  qed_spec_mp "bag_of_mono_aux";
   6.127  
   6.128 -Goal "[|  <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
   6.129 -\  <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
   6.130 +Goal "[|  <xs, ys>\\<in>prefix(A); xs\\<in>list(A); ys\\<in>list(A) |] ==> \
   6.131 +\  <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
   6.132  by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
   6.133  qed "bag_of_mono";
   6.134  AddIs [bag_of_mono];
   6.135 @@ -150,7 +150,7 @@
   6.136  
   6.137  bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
   6.138  
   6.139 -Goal "l : list(A) ==> C Int length(l) : Fin(length(l))";
   6.140 +Goal "l \\<in> list(A) ==> C Int length(l) \\<in> Fin(length(l))";
   6.141  by (dtac length_type 1); 
   6.142  by (rtac Fin_subset 1); 
   6.143  by (rtac Int_lower2 1);
   6.144 @@ -182,7 +182,7 @@
   6.145  by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   6.146  qed "bag_of_sublist_lemma";
   6.147  
   6.148 -Goal "l:list(A) ==> \
   6.149 +Goal "l\\<in>list(A) ==> \
   6.150  \ C <= nat ==> \
   6.151  \ bag_of(sublist(l, C)) = \
   6.152  \     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   6.153 @@ -201,7 +201,7 @@
   6.154  qed "nat_Int_length_eq";
   6.155  
   6.156  (*eliminating the assumption C<=nat*)
   6.157 -Goal "l:list(A) ==> \
   6.158 +Goal "l\\<in>list(A) ==> \
   6.159  \ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   6.160  by (subgoal_tac
   6.161        " bag_of(sublist(l, C Int nat)) = \
   6.162 @@ -211,7 +211,7 @@
   6.163  qed "bag_of_sublist";
   6.164  
   6.165  Goal 
   6.166 -"l:list(A) ==> \
   6.167 +"l\\<in>list(A) ==> \
   6.168  \ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
   6.169  \     bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
   6.170  by (subgoal_tac
   6.171 @@ -226,16 +226,16 @@
   6.172  qed "bag_of_sublist_Un_Int";
   6.173  
   6.174  
   6.175 -Goal "[| l:list(A); B Int C = 0  |]\
   6.176 +Goal "[| l\\<in>list(A); B Int C = 0  |]\
   6.177  \     ==> bag_of(sublist(l, B Un C)) = \
   6.178  \         bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; 
   6.179  by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym, 
   6.180                    sublist_type,  bag_of_multiset]) 1);
   6.181  qed "bag_of_sublist_Un_disjoint";
   6.182  
   6.183 -Goal "[| Finite(I); ALL i:I. ALL j:I. i~=j --> A(i) Int A(j) = 0; \
   6.184 -\ l:list(B) |] \
   6.185 -\     ==> bag_of(sublist(l, UN i:I. A(i))) =  \
   6.186 +Goal "[|Finite(I); \\<forall>i\\<in>I. \\<forall>j\\<in>I. i\\<noteq>j --> A(i) \\<inter> A(j) = 0; \
   6.187 +\       l\\<in>list(B) |] \
   6.188 +\     ==> bag_of(sublist(l, \\<Union>i\\<in>I. A(i))) =  \
   6.189  \         (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";  
   6.190  by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
   6.191                              addsimps [bag_of_sublist]) 1);
   6.192 @@ -263,13 +263,13 @@
   6.193  
   6.194  Goalw [all_distinct_def] 
   6.195  "all_distinct(Cons(a, l)) <-> \
   6.196 -\ (a:set_of_list(l) --> False) & (a ~: set_of_list(l) --> all_distinct(l))";
   6.197 +\ (a\\<in>set_of_list(l) --> False) & (a \\<notin> set_of_list(l) --> all_distinct(l))";
   6.198  by (auto_tac (claset() addEs [list.elim], simpset()));
   6.199  qed "all_distinct_Cons";
   6.200  Addsimps [all_distinct_Nil, all_distinct_Cons];
   6.201  
   6.202  (** state_of **)
   6.203 -Goalw [state_of_def] "s:state ==> state_of(s)=s";
   6.204 +Goalw [state_of_def] "s\\<in>state ==> state_of(s)=s";
   6.205  by Auto_tac;
   6.206  qed "state_of_state";
   6.207  Addsimps [state_of_state];
   6.208 @@ -281,7 +281,7 @@
   6.209  Addsimps [state_of_idem];
   6.210  
   6.211  
   6.212 -Goalw [state_of_def] "state_of(s):state";
   6.213 +Goalw [state_of_def] "state_of(s)\\<in>state";
   6.214  by Auto_tac;
   6.215  qed "state_of_type";
   6.216  Addsimps [state_of_type];
   6.217 @@ -329,25 +329,25 @@
   6.218                  handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
   6.219       handle THM _ => th;
   6.220  
   6.221 -Goal "n:nat ==> nat_list_inj(n):list(nat)";
   6.222 +Goal "n\\<in>nat ==> nat_list_inj(n)\\<in>list(nat)";
   6.223  by (induct_tac "n" 1);
   6.224  by Auto_tac;
   6.225  qed "nat_list_inj_type";
   6.226  
   6.227 -Goal "n:nat ==> length(nat_list_inj(n)) = n";
   6.228 +Goal "n\\<in>nat ==> length(nat_list_inj(n)) = n";
   6.229  by (induct_tac "n" 1);
   6.230  by Auto_tac;
   6.231  qed "length_nat_list_inj";
   6.232  
   6.233  Goalw [nat_var_inj_def]
   6.234 -  "(lam x:nat. nat_var_inj(x)):inj(nat, var)";
   6.235 +  "(\\<lambda>x\\<in>nat. nat_var_inj(x))\\<in>inj(nat, var)";
   6.236  by (res_inst_tac [("d", "var_inj")] lam_injective 1); 
   6.237  by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
   6.238  by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
   6.239  qed "var_infinite_lemma";
   6.240  
   6.241  Goalw [lepoll_def] "nat lepoll var";
   6.242 -by (res_inst_tac [("x", "(lam x:nat. nat_var_inj(x))")] exI 1);
   6.243 +by (res_inst_tac [("x", "(\\<lambda>x\\<in>nat. nat_var_inj(x))")] exI 1);
   6.244  by (rtac var_infinite_lemma 1);
   6.245  qed "nat_lepoll_var";
   6.246  
   6.247 @@ -369,15 +369,15 @@
   6.248  by (blast_tac (claset() addEs [mem_irrefl]) 1);
   6.249  qed "var_not_Finite";
   6.250  
   6.251 -Goal "~Finite(A) ==> EX x. x:A";
   6.252 +Goal "~Finite(A) ==> \\<exists>x. x\\<in>A";
   6.253  by (etac swap 1);
   6.254  by Auto_tac;
   6.255  by (subgoal_tac "A=0" 1);
   6.256  by (auto_tac (claset(), simpset() addsimps [Finite_0]));
   6.257  qed "not_Finite_imp_exist";
   6.258  
   6.259 -Goal "Finite(A) ==> b:(Inter(RepFun(var-A, B))) <-> (ALL x:var-A. b:B(x))";
   6.260 -by (subgoal_tac "EX x. x:var-A" 1);
   6.261 +Goal "Finite(A) ==> b\\<in>(Inter(RepFun(var-A, B))) <-> (\\<forall>x\\<in>var-A. b\\<in>B(x))";
   6.262 +by (subgoal_tac "\\<exists>x. x\\<in>var-A" 1);
   6.263  by Auto_tac;
   6.264  by (subgoal_tac "~Finite(var-A)" 1);
   6.265  by (dtac not_Finite_imp_exist 1);
   6.266 @@ -388,38 +388,39 @@
   6.267  by Auto_tac;
   6.268  qed "Inter_Diff_var_iff";
   6.269  
   6.270 -Goal "[| b:Inter(RepFun(var-A, B)); Finite(A); x:var-A |] ==> b:B(x)";
   6.271 +Goal "[| b\\<in>Inter(RepFun(var-A, B)); Finite(A); x\\<in>var-A |] ==> b\\<in>B(x)";
   6.272  by (rotate_tac 1 1);
   6.273  by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
   6.274  qed "Inter_var_DiffD";
   6.275  
   6.276 -(* [| Finite(A); (ALL x:var-A. b:B(x)) |] ==> b:Inter(RepFun(var-A, B)) *)
   6.277 +(* [| Finite(A); (\\<forall>x\\<in>var-A. b\\<in>B(x)) |] ==> b\\<in>Inter(RepFun(var-A, B)) *)
   6.278  bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
   6.279  
   6.280  AddSIs [Inter_var_DiffI];
   6.281  Addsimps [Finite_0, Finite_cons];
   6.282  
   6.283 -Goal "Acts(F)<= A Int Pow(state*state)  <-> Acts(F)<=A";
   6.284 +Goal "Acts(F)<= A \\<inter> Pow(state*state)  <-> Acts(F)<=A";
   6.285  by (cut_facts_tac [inst "F" "F" Acts_type] 1);
   6.286  by Auto_tac;
   6.287  qed "Acts_subset_Int_Pow_simp";
   6.288  Addsimps [Acts_subset_Int_Pow_simp];
   6.289  
   6.290 -Goal "cons(x, A Int B) = cons(x, A) Int cons(x, B)";
   6.291 +(*for main zf?????*)
   6.292 +Goal "cons(x, A \\<inter> B) = cons(x, A) \\<inter> cons(x, B)";
   6.293  by Auto_tac;
   6.294  qed "cons_Int_distrib";
   6.295  
   6.296  
   6.297  (* Currently not used, but of potential interest *)
   6.298  Goal 
   6.299 -"[| Finite(A); ALL x:A. g(x):nat |] ==> \
   6.300 +"[| Finite(A); \\<forall>x\\<in>A. g(x)\\<in>nat |] ==> \
   6.301  \ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
   6.302  by (etac Finite_induct 1);
   6.303  by (auto_tac (claset(), simpset() addsimps [int_of_add]));
   6.304  qed "setsum_nsetsum_eq";
   6.305  
   6.306  Goal 
   6.307 -"[| A=B;  ALL x:A. f(x)=g(x);  ALL x:A. g(x):nat; \
   6.308 +"[| A=B;  \\<forall>x\\<in>A. f(x)=g(x);  \\<forall>x\\<in>A. g(x)\\<in>nat; \
   6.309  \     Finite(A) |]  ==> nsetsum(f, A) = nsetsum(g, B)";
   6.310  by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
   6.311  by (rtac trans 2);
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Fri Jun 20 12:10:45 2003 +0200
     7.3 @@ -0,0 +1,796 @@
     7.4 +(*Title: ZF/UNITY/AllocImpl
     7.5 +    ID:    $Id$
     7.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     7.7 +    Copyright   2002  University of Cambridge
     7.8 +
     7.9 +Single-client allocator implementation
    7.10 +Charpentier and Chandy, section 7 (page 17).
    7.11 +*)
    7.12 +
    7.13 +(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
    7.14 +
    7.15 +theory AllocImpl = ClientImpl:
    7.16 +
    7.17 +(*????MOVE UP*)
    7.18 +method_setup constrains = {*
    7.19 +    Method.ctxt_args (fn ctxt =>
    7.20 +        Method.METHOD (fn facts =>
    7.21 +            gen_constrains_tac (Classical.get_local_claset ctxt,
    7.22 +                               Simplifier.get_local_simpset ctxt) 1)) *}
    7.23 +    "for proving safety properties"
    7.24 +
    7.25 +consts
    7.26 +
    7.27 +  NbR :: i            (*number of consumed messages*)
    7.28 +  available_tok :: i  (*number of free tokens (T in paper)*)
    7.29 +
    7.30 +translations
    7.31 +  "NbR" == "Var([succ(2)])"
    7.32 +  "available_tok" == "Var([succ(succ(2))])"
    7.33 +
    7.34 +axioms
    7.35 +  alloc_type_assumes:
    7.36 +  "type_of(NbR) = nat & type_of(available_tok)=nat"
    7.37 +
    7.38 +  alloc_default_val_assumes:
    7.39 +  "default_val(NbR)  = 0 & default_val(available_tok)=0"
    7.40 +
    7.41 +constdefs
    7.42 +  alloc_giv_act :: i
    7.43 +  "alloc_giv_act ==
    7.44 +       {<s, t> : state*state.
    7.45 +	\<exists>k. k = length(s`giv) &
    7.46 +            t = s(giv := s`giv @ [nth(k, s`ask)],
    7.47 +		  available_tok := s`available_tok #- nth(k, s`ask)) &
    7.48 +	    k < length(s`ask) & nth(k, s`ask) le s`available_tok}"
    7.49 +
    7.50 +  alloc_rel_act :: i
    7.51 +  "alloc_rel_act ==
    7.52 +       {<s, t> : state*state.
    7.53 +        t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
    7.54 +	      NbR := succ(s`NbR)) &
    7.55 +  	s`NbR < length(s`rel)}"
    7.56 +
    7.57 +  (*The initial condition s`giv=[] is missing from the
    7.58 +    original definition -- S. O. Ehmety *)
    7.59 +  alloc_prog :: i
    7.60 +  "alloc_prog ==
    7.61 +       mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
    7.62 +		  {alloc_giv_act, alloc_rel_act},
    7.63 +		  \<Union>G \<in> preserves(lift(available_tok)) \<inter>
    7.64 +		        preserves(lift(NbR)) \<inter>
    7.65 +		        preserves(lift(giv)). Acts(G))"
    7.66 +
    7.67 +
    7.68 +
    7.69 +
    7.70 +(*????FIXME: sort out this mess
    7.71 +FoldSet.cons_Int_right_lemma1:
    7.72 +  ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
    7.73 +FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
    7.74 +Multiset.cons_Int_right_cases:
    7.75 +  cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
    7.76 +UNITYMisc.Int_cons_right:
    7.77 +  ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
    7.78 +UNITYMisc.Int_succ_right:
    7.79 +  ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
    7.80 +*)
    7.81 +
    7.82 +
    7.83 +declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
    7.84 +
    7.85 +lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
    7.86 +apply (unfold state_def)
    7.87 +apply (drule_tac a = "available_tok" in apply_type)
    7.88 +apply auto
    7.89 +done
    7.90 +
    7.91 +lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
    7.92 +apply (unfold state_def)
    7.93 +apply (drule_tac a = "NbR" in apply_type)
    7.94 +apply auto
    7.95 +done
    7.96 +
    7.97 +(** The Alloc Program **)
    7.98 +
    7.99 +lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
   7.100 +apply (simp add: alloc_prog_def)
   7.101 +done
   7.102 +
   7.103 +declare alloc_prog_def [THEN def_prg_Init, simp]
   7.104 +declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
   7.105 +ML
   7.106 +{*
   7.107 +program_defs_ref := [thm"alloc_prog_def"]
   7.108 +*}
   7.109 +
   7.110 +declare  alloc_giv_act_def [THEN def_act_simp, simp]
   7.111 +declare  alloc_rel_act_def [THEN def_act_simp, simp]
   7.112 +
   7.113 +
   7.114 +lemma alloc_prog_ok_iff:
   7.115 +"\<forall>G \<in> program. (alloc_prog ok G) <->
   7.116 +     (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) &
   7.117 +       G \<in> preserves(lift(NbR)) &  alloc_prog \<in> Allowed(G))"
   7.118 +by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed])
   7.119 +
   7.120 +
   7.121 +lemma alloc_prog_preserves:
   7.122 +    "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
   7.123 +apply (rule Inter_var_DiffI)
   7.124 +apply (force );
   7.125 +apply (rule ballI)
   7.126 +apply (rule preservesI)
   7.127 +apply (constrains)
   7.128 +done
   7.129 +
   7.130 +(* As a special case of the rule above *)
   7.131 +
   7.132 +lemma alloc_prog_preserves_rel_ask_tok:
   7.133 +    "alloc_prog \<in>
   7.134 +       preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
   7.135 +apply auto
   7.136 +apply (insert alloc_prog_preserves)
   7.137 +apply (drule_tac [3] x = "tok" in Inter_var_DiffD)
   7.138 +apply (drule_tac [2] x = "ask" in Inter_var_DiffD)
   7.139 +apply (drule_tac x = "rel" in Inter_var_DiffD)
   7.140 +apply auto
   7.141 +done
   7.142 +
   7.143 +lemma alloc_prog_Allowed:
   7.144 +"Allowed(alloc_prog) =
   7.145 +  preserves(lift(giv)) \<inter> preserves(lift(available_tok)) \<inter> preserves(lift(NbR))"
   7.146 +apply (cut_tac v="lift(giv)" in preserves_type)
   7.147 +apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
   7.148 +                      cons_Int_distrib safety_prop_Acts_iff)
   7.149 +done
   7.150 +
   7.151 +(* In particular we have *)
   7.152 +lemma alloc_prog_ok_client_prog: "alloc_prog ok client_prog"
   7.153 +apply (auto simp add: ok_iff_Allowed)
   7.154 +apply (cut_tac alloc_prog_preserves)
   7.155 +apply (cut_tac [2] client_prog_preserves)
   7.156 +apply (auto simp add: alloc_prog_Allowed client_prog_Allowed)
   7.157 +apply (drule_tac [6] B = "preserves (lift (NbR))" in InterD)
   7.158 +apply (drule_tac [5] B = "preserves (lift (available_tok))" in InterD)
   7.159 +apply (drule_tac [4] B = "preserves (lift (giv))" in InterD)
   7.160 +apply (drule_tac [3] B = "preserves (lift (tok))" in InterD)
   7.161 +apply (drule_tac [2] B = "preserves (lift (ask))" in InterD)
   7.162 +apply (drule_tac B = "preserves (lift (rel))" in InterD)
   7.163 +apply auto
   7.164 +done
   7.165 +
   7.166 +(** Safety property: (28) **)
   7.167 +lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
   7.168 +apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed)
   7.169 +apply constrains+
   7.170 +apply (auto dest: ActsD)
   7.171 +apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
   7.172 +apply auto
   7.173 +done
   7.174 +
   7.175 +lemma giv_Bounded_lamma1:
   7.176 +"alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
   7.177 +                     {s\<in>state. s`available_tok #+ tokens(s`giv) =
   7.178 +                                 NbT #+ tokens(take(s`NbR, s`rel))})"
   7.179 +apply (constrains)
   7.180 +apply auto
   7.181 +apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
   7.182 +apply (simp (no_asm_simp) add: take_succ)
   7.183 +done
   7.184 +
   7.185 +lemma giv_Bounded_lemma2:
   7.186 +"[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
   7.187 +  ==> alloc_prog Join G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
   7.188 +   {s\<in>state. s`available_tok #+ tokens(s`giv) =
   7.189 +    NbT #+ tokens(take(s`NbR, s`rel))})"
   7.190 +apply (cut_tac giv_Bounded_lamma1)
   7.191 +apply (cut_tac alloc_prog_preserves_rel_ask_tok)
   7.192 +apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
   7.193 +apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
   7.194 +apply (rotate_tac -1)
   7.195 +apply (cut_tac A = "nat * nat * list(nat)"
   7.196 +             and P = "%<m,n,l> y. n \<le> length(y) & 
   7.197 +                                  m #+ tokens(l) = NbT #+ tokens(take(n,y))"
   7.198 +             and g = "lift(rel)" and F = "alloc_prog"
   7.199 +       in stable_Join_Stable)
   7.200 +prefer 3 apply assumption;
   7.201 +apply (auto simp add: Collect_conj_eq)
   7.202 +apply (frule_tac g = "length" in imp_Increasing_comp)
   7.203 +apply (blast intro: mono_length)
   7.204 +apply (auto simp add: refl_prefix)
   7.205 +apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
   7.206 +apply assumption
   7.207 +apply (auto simp add: Le_def length_type)
   7.208 +apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def)
   7.209 +apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
   7.210 +apply assumption+
   7.211 +apply (force dest: ActsD)
   7.212 +apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) Un Acts (G). ?P(x)" in thin_rl)
   7.213 +apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
   7.214 +apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
   7.215 +apply (auto simp add: Stable_def Constrains_def constrains_def)
   7.216 +apply (drule bspec)
   7.217 +apply force
   7.218 +apply (drule subsetD)
   7.219 +apply (rule imageI)
   7.220 +apply assumption
   7.221 +apply (auto simp add: prefix_take_iff)
   7.222 +apply (rotate_tac -1)
   7.223 +apply (erule ssubst)
   7.224 +apply (auto simp add: take_take min_def)
   7.225 +done
   7.226 +
   7.227 +(*Property (29), page 18:
   7.228 +  the number of tokens in circulation never exceeds NbT*)
   7.229 +lemma alloc_prog_giv_Bounded: "alloc_prog \<in> Incr(lift(rel))
   7.230 +      guarantees Always({s\<in>state. tokens(s`giv) \<le> NbT #+ tokens(s`rel)})"
   7.231 +apply (cut_tac NbT_pos)
   7.232 +apply (auto simp add: guar_def)
   7.233 +apply (rule Always_weaken)
   7.234 +apply (rule AlwaysI)
   7.235 +apply (rule_tac [2] giv_Bounded_lemma2)
   7.236 +apply auto
   7.237 +apply (rule_tac j = "NbT #+ tokens (take (x` NbR, x`rel))" in le_trans)
   7.238 +apply (erule subst)
   7.239 +apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
   7.240 +done
   7.241 +
   7.242 +(*Property (30), page 18: the number of tokens given never exceeds the number
   7.243 +  asked for*)
   7.244 +lemma alloc_prog_ask_prefix_giv:
   7.245 +     "alloc_prog \<in> Incr(lift(ask)) guarantees
   7.246 +                   Always({s\<in>state. <s`giv, s`ask>:prefix(tokbag)})"
   7.247 +apply (auto intro!: AlwaysI simp add: guar_def)
   7.248 +apply (subgoal_tac "G \<in> preserves (lift (giv))")
   7.249 + prefer 2 apply (simp add: alloc_prog_ok_iff)
   7.250 +apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)" 
   7.251 +       in stable_Join_Stable)
   7.252 +apply (constrains)
   7.253 + prefer 2 apply (simp add: lift_def); 
   7.254 + apply (clarify ); 
   7.255 +apply (drule_tac a = "k" in Increasing_imp_Stable)
   7.256 +apply auto
   7.257 +done
   7.258 +
   7.259 +(**** Towards proving the liveness property, (31) ****)
   7.260 +
   7.261 +(*** First, we lead up to a proof of Lemma 49, page 28. ***)
   7.262 +
   7.263 +lemma alloc_prog_transient_lemma:
   7.264 +"G \<in> program ==> \<forall>k\<in>nat. alloc_prog Join G \<in>
   7.265 +                   transient({s\<in>state. k \<le> length(s`rel)}
   7.266 +                   \<inter> {s\<in>state. succ(s`NbR) = k})"
   7.267 +apply auto
   7.268 +apply (erule_tac V = "G\<notin>?u" in thin_rl)
   7.269 +apply (rule_tac act = "alloc_rel_act" in transientI)
   7.270 +apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
   7.271 +apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
   7.272 +apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   7.273 +apply (rule ReplaceI)
   7.274 +apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
   7.275 +                        NbR:=succ (x`NbR))" 
   7.276 +       in exI)
   7.277 +apply (auto intro!: state_update_type)
   7.278 +done
   7.279 +
   7.280 +lemma alloc_prog_rel_Stable_NbR_lemma:
   7.281 +"[| G \<in> program; alloc_prog ok G; k\<in>nat |] ==>
   7.282 +    alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
   7.283 +apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
   7.284 +apply constrains
   7.285 +apply auto
   7.286 +apply (blast intro: le_trans leI)
   7.287 +apply (drule_tac f = "lift (NbR)" and A = "nat" in preserves_imp_increasing)
   7.288 +apply (drule_tac [2] g = "succ" in imp_increasing_comp)
   7.289 +apply (rule_tac [2] mono_succ)
   7.290 +apply (drule_tac [4] x = "k" in increasing_imp_stable)
   7.291 +    prefer 5 apply (simp add: Le_def comp_def) 
   7.292 +apply auto
   7.293 +done
   7.294 +
   7.295 +lemma alloc_prog_NbR_LeadsTo_lemma [rule_format (no_asm)]:
   7.296 +"[| G \<in> program; alloc_prog ok G;
   7.297 +    alloc_prog Join G \<in> Incr(lift(rel)) |] ==>
   7.298 +     \<forall>k\<in>nat. alloc_prog Join G \<in>
   7.299 +       {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   7.300 +       LeadsTo {s\<in>state. k \<le> s`NbR}"
   7.301 +apply clarify
   7.302 +apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   7.303 +apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   7.304 +apply (rule_tac [2] mono_length)
   7.305 +    prefer 3 apply (simp add: ); 
   7.306 +apply (simp_all add: refl_prefix Le_def comp_def length_type)
   7.307 +apply (rule LeadsTo_weaken)
   7.308 +apply (rule PSP_Stable)
   7.309 +prefer 2 apply (assumption)
   7.310 +apply (rule PSP_Stable)
   7.311 +apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
   7.312 +apply (rule alloc_prog_transient_lemma [THEN bspec, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo])
   7.313 +apply assumption+
   7.314 +apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
   7.315 +done
   7.316 +
   7.317 +lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
   7.318 +    "[| G :program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
   7.319 +      ==> \<forall>k\<in>nat. \<forall>n \<in> nat. n < k -->
   7.320 +       alloc_prog Join G \<in>
   7.321 +       {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   7.322 +	  LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
   7.323 +	    (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   7.324 +apply (unfold greater_than_def)
   7.325 +apply clarify
   7.326 +apply (rule_tac A' = "{x \<in> state. k \<le> length (x`rel) } \<inter> {x \<in> state. n < x`NbR}" in LeadsTo_weaken_R)
   7.327 +apply safe
   7.328 +apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   7.329 +apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   7.330 +apply (rule_tac [2] mono_length)
   7.331 +    prefer 3 apply (simp add: ); 
   7.332 +apply (simp_all add: refl_prefix Le_def comp_def length_type)
   7.333 +apply (subst Int_commute)
   7.334 +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)
   7.335 +apply (rule PSP_Stable)
   7.336 +apply safe
   7.337 +apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
   7.338 +apply (rule_tac [2] LeadsTo_weaken)
   7.339 +apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
   7.340 +apply (simp_all add: ) 
   7.341 +apply (rule subset_imp_LeadsTo)
   7.342 +apply auto
   7.343 +apply (blast intro: lt_trans2)
   7.344 +done
   7.345 +
   7.346 +lemma Collect_vimage_eq: "u\<in>nat ==> {<s, f(s)>. s \<in> state} -`` u = {s\<in>state. f(s) < u}"
   7.347 +apply (force simp add: lt_def)
   7.348 +done
   7.349 +
   7.350 +(* Lemma 49, page 28 *)
   7.351 +
   7.352 +lemma alloc_prog_NbR_LeadsTo_lemma3:
   7.353 +  "[|G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
   7.354 +     k\<in>nat|]
   7.355 +   ==> alloc_prog Join G \<in>
   7.356 +           {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
   7.357 +(* Proof by induction over the difference between k and n *)
   7.358 +apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
   7.359 +apply (simp_all add: lam_def)
   7.360 +apply auto
   7.361 +apply (rule single_LeadsTo_I)
   7.362 +apply auto
   7.363 +apply (simp (no_asm_simp) add: Collect_vimage_eq)
   7.364 +apply (rename_tac "s0")
   7.365 +apply (case_tac "s0`NbR < k")
   7.366 +apply (rule_tac [2] subset_imp_LeadsTo)
   7.367 +apply safe
   7.368 +apply (auto dest!: not_lt_imp_le)
   7.369 +apply (rule LeadsTo_weaken)
   7.370 +apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2)
   7.371 +apply safe
   7.372 +prefer 3 apply (assumption)
   7.373 +apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
   7.374 +apply (blast dest: lt_asym)
   7.375 +apply (force dest: add_lt_elim2)
   7.376 +done
   7.377 +
   7.378 +(** Towards proving lemma 50, page 29 **)
   7.379 +
   7.380 +lemma alloc_prog_giv_Ensures_lemma:
   7.381 +"[| G \<in> program; k\<in>nat; alloc_prog ok G;
   7.382 +  alloc_prog Join G \<in> Incr(lift(ask)) |] ==>
   7.383 +  alloc_prog Join G \<in>
   7.384 +  {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   7.385 +  {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
   7.386 +  Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
   7.387 +apply (rule EnsuresI)
   7.388 +apply auto
   7.389 +apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
   7.390 +apply (rule_tac [2] act = "alloc_giv_act" in transientI)
   7.391 + prefer 2
   7.392 + apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   7.393 + apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
   7.394 +apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   7.395 +apply (erule_tac [2] swap)
   7.396 +apply (rule_tac [2] ReplaceI)
   7.397 +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)
   7.398 +apply (auto intro!: state_update_type simp add: app_type)
   7.399 +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)
   7.400 +apply safe
   7.401 +apply (auto dest: ActsD simp add: Constrains_def constrains_def length_app alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
   7.402 +apply (subgoal_tac "length (xa ` giv @ [nth (length (xa ` giv), xa ` ask) ]) = length (xa ` giv) #+ 1")
   7.403 +apply (rule_tac [2] trans)
   7.404 +apply (rule_tac [2] length_app)
   7.405 +apply auto
   7.406 +apply (rule_tac j = "xa ` available_tok" in le_trans)
   7.407 +apply auto
   7.408 +apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
   7.409 +apply assumption+
   7.410 +apply auto
   7.411 +apply (drule_tac a = "xa ` ask" and r = "prefix(tokbag)" and A = "list(tokbag)"
   7.412 +       in Increasing_imp_Stable)
   7.413 +apply (auto simp add: prefix_iff)
   7.414 +apply (drule StableD)
   7.415 +apply (auto simp add: Constrains_def constrains_def)
   7.416 +apply force
   7.417 +done
   7.418 +
   7.419 +lemma alloc_prog_giv_Stable_lemma:
   7.420 +"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   7.421 +  ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
   7.422 +apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
   7.423 +apply (constrains)
   7.424 +apply (auto intro: leI simp add: length_app)
   7.425 +apply (drule_tac f = "lift (giv)" and g = "length" in imp_preserves_comp)
   7.426 +apply (drule_tac f = "length comp lift (giv)" and A = "nat" and r = "Le" in preserves_imp_increasing)
   7.427 +apply (drule_tac [2] x = "k" in increasing_imp_stable)
   7.428 + prefer 3 apply (simp add: Le_def comp_def)
   7.429 +apply (auto simp add: length_type)
   7.430 +done
   7.431 +
   7.432 +(* Lemma 50, page 29 *)
   7.433 +
   7.434 +lemma alloc_prog_giv_LeadsTo_lemma:
   7.435 +"[| G \<in> program; alloc_prog ok G;
   7.436 +    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |] ==>
   7.437 +  alloc_prog Join G \<in>
   7.438 +    {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   7.439 +    {s\<in>state.  k < length(s`ask)} \<inter>
   7.440 +    {s\<in>state. length(s`giv) = k}
   7.441 +    LeadsTo {s\<in>state. k < length(s`giv)}"
   7.442 +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}")
   7.443 +prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
   7.444 +apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length (s`ask) }) ")
   7.445 +apply (drule PSP_Stable)
   7.446 +apply assumption
   7.447 +apply (rule LeadsTo_weaken)
   7.448 +apply (rule PSP_Stable)
   7.449 +apply (rule_tac [2] k = "k" in alloc_prog_giv_Stable_lemma)
   7.450 +apply (auto simp add: le_iff)
   7.451 +apply (drule_tac a = "succ (k)" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   7.452 +apply (rule mono_length)
   7.453 + prefer 2 apply (simp add: ); 
   7.454 +apply (simp_all add: refl_prefix Le_def comp_def length_type)
   7.455 +done
   7.456 +
   7.457 +(* Lemma 51, page 29.
   7.458 +  This theorem states as invariant that if the number of
   7.459 +  tokens given does not exceed the number returned, then the upper limit
   7.460 +  (NbT) does not exceed the number currently available.*)
   7.461 +lemma alloc_prog_Always_lemma:
   7.462 +"[| G \<in> program; alloc_prog ok G;
   7.463 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.464 +    alloc_prog Join G \<in> Incr(lift(rel)) |]
   7.465 +  ==> alloc_prog Join G \<in>
   7.466 +        Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
   7.467 +                NbT \<le> s`available_tok})"
   7.468 +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))}) ")
   7.469 +apply (rule_tac [2] AlwaysI)
   7.470 +apply (rule_tac [3] giv_Bounded_lemma2)
   7.471 +apply auto
   7.472 +apply (rule Always_weaken)
   7.473 +apply assumption
   7.474 +apply auto
   7.475 +apply (subgoal_tac "0 \<le> tokens (take (x ` NbR, x ` rel)) #- tokens (x`giv) ")
   7.476 +apply (rule_tac [2] nat_diff_split [THEN iffD2])
   7.477 + prefer 2 apply (force ); 
   7.478 +apply (subgoal_tac "x`available_tok =
   7.479 +                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens (x`giv))")
   7.480 +apply (simp (no_asm_simp))
   7.481 +apply (rule nat_diff_split [THEN iffD2])
   7.482 +apply auto
   7.483 +apply (drule_tac j = "tokens (x ` giv)" in lt_trans2)
   7.484 +apply assumption
   7.485 +apply auto
   7.486 +done
   7.487 +
   7.488 +(* Main lemmas towards proving property (31) *)
   7.489 +
   7.490 +lemma LeadsTo_strength_R:
   7.491 +    "[|  F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo  B"
   7.492 +by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) 
   7.493 +
   7.494 +lemma PSP_StableI:
   7.495 +"[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
   7.496 +   F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo  B"
   7.497 +apply (rule_tac A = " (A-C) Un (A \<inter> C)" in LeadsTo_weaken_L)
   7.498 + prefer 2 apply (blast)
   7.499 +apply (rule LeadsTo_Un)
   7.500 +apply assumption
   7.501 +apply (blast intro: LeadsTo_weaken dest: PSP_Stable) 
   7.502 +done
   7.503 +
   7.504 +lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
   7.505 +apply auto
   7.506 +done
   7.507 +
   7.508 +(*needed?*)
   7.509 +lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
   7.510 +apply auto
   7.511 +done
   7.512 +
   7.513 +
   7.514 +(*First step in proof of (31) -- the corrected version from Charpentier.
   7.515 +  This lemma implies that if a client releases some tokens then the Allocator
   7.516 +  will eventually recognize that they've been released.*)
   7.517 +lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma:
   7.518 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.519 +    G \<in> program; alloc_prog ok G; k \<in> tokbag |]
   7.520 +  ==> alloc_prog Join G \<in>
   7.521 +        {s\<in>state. k \<le> tokens(s`rel)}
   7.522 +        LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   7.523 +apply (rule single_LeadsTo_I)
   7.524 +apply safe
   7.525 +apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
   7.526 +apply (rule_tac [4] k1 = "length (s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
   7.527 +apply (rule_tac [8] subset_imp_LeadsTo)
   7.528 +apply auto
   7.529 +apply (rule_tac j = "tokens (take (length (s`rel), x`rel))" in le_trans)
   7.530 +apply (rule_tac j = "tokens (take (length (s`rel), s`rel))" in le_trans)
   7.531 +apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
   7.532 +done
   7.533 +
   7.534 +(*** Rest of proofs done by lcp ***)
   7.535 +
   7.536 +(*Second step in proof of (31): by LHS of the guarantee and transivity of
   7.537 +  LeadsTo *)
   7.538 +lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma2:
   7.539 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.540 +    G \<in> program; alloc_prog ok G; k \<in> tokbag;
   7.541 +    alloc_prog Join G \<in>
   7.542 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.543 +  ==> alloc_prog Join G \<in>
   7.544 +        {s\<in>state. tokens(s`giv) = k}
   7.545 +        LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   7.546 +apply (rule LeadsTo_Trans)
   7.547 +apply (rule_tac [2] alloc_prog_LeadsTo_tokens_take_NbR_lemma)
   7.548 +apply (blast intro: LeadsTo_weaken_L nat_into_Ord)
   7.549 +apply assumption+
   7.550 +done
   7.551 +
   7.552 +(*Third step in proof of (31): by PSP with the fact that giv increases *)
   7.553 +lemma alloc_prog_LeadsTo_length_giv_disj:
   7.554 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.555 +    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
   7.556 +    alloc_prog Join G \<in>
   7.557 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.558 +  ==> alloc_prog Join G \<in>
   7.559 +        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   7.560 +        LeadsTo
   7.561 +          {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
   7.562 +                     k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
   7.563 +apply (rule single_LeadsTo_I)
   7.564 +apply safe
   7.565 +apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
   7.566 +apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
   7.567 +apply (simp_all add: Int_cons_left)
   7.568 +apply (rule LeadsTo_weaken)
   7.569 +apply (rule_tac k = "tokens (s`giv)" in alloc_prog_LeadsTo_tokens_take_NbR_lemma2)
   7.570 +apply simp_all
   7.571 +apply safe
   7.572 +apply (drule prefix_length_le [THEN le_iff [THEN iffD1]]) 
   7.573 +apply (force simp add:)
   7.574 +apply (simp add: not_lt_iff_le)
   7.575 +apply (drule prefix_length_le_equal)
   7.576 +apply assumption
   7.577 +apply (simp add:)
   7.578 +done
   7.579 +
   7.580 +(*Fourth step in proof of (31): we apply lemma (51) *)
   7.581 +lemma alloc_prog_LeadsTo_length_giv_disj2:
   7.582 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.583 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.584 +    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
   7.585 +    alloc_prog Join G \<in>
   7.586 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.587 +  ==> alloc_prog Join G \<in>
   7.588 +        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   7.589 +        LeadsTo
   7.590 +          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   7.591 +                    n < length(s`giv)}"
   7.592 +apply (rule LeadsTo_weaken_R)
   7.593 +apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma alloc_prog_LeadsTo_length_giv_disj])
   7.594 +apply auto
   7.595 +done
   7.596 +
   7.597 +(*For using "disjunction" (union over an index set) to eliminate a variable.
   7.598 +  ????move way up*)
   7.599 +lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
   7.600 +      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
   7.601 +apply blast
   7.602 +done
   7.603 +
   7.604 +
   7.605 +(*Fifth step in proof of (31): from the fourth step, taking the union over all
   7.606 +  k\<in>nat *)
   7.607 +lemma alloc_prog_LeadsTo_length_giv_disj3:
   7.608 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.609 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.610 +    G \<in> program; alloc_prog ok G;  n \<in> nat;
   7.611 +    alloc_prog Join G \<in>
   7.612 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.613 +  ==> alloc_prog Join G \<in>
   7.614 +        {s\<in>state. length(s`giv) = n}
   7.615 +        LeadsTo
   7.616 +          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   7.617 +                    n < length(s`giv)}"
   7.618 +apply (rule LeadsTo_weaken_L)
   7.619 +apply (rule_tac I = "nat" in LeadsTo_UN)
   7.620 +apply (rule_tac k = "i" in alloc_prog_LeadsTo_length_giv_disj2)
   7.621 +apply (simp_all add: UN_conj_eq)
   7.622 +done
   7.623 +
   7.624 +(*Sixth step in proof of (31): from the fifth step, by PSP with the
   7.625 +  assumption that ask increases *)
   7.626 +lemma alloc_prog_LeadsTo_length_ask_giv:
   7.627 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.628 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.629 +    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   7.630 +    alloc_prog Join G \<in>
   7.631 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.632 +  ==> alloc_prog Join G \<in>
   7.633 +        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   7.634 +        LeadsTo
   7.635 +          {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   7.636 +                     length(s`giv) = n) |
   7.637 +                    n < length(s`giv)}"
   7.638 +apply (rule single_LeadsTo_I)
   7.639 +apply safe
   7.640 +apply (rule_tac a1 = "s`ask" and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI])
   7.641 +apply assumption
   7.642 +apply simp_all
   7.643 +apply (rule LeadsTo_weaken)
   7.644 +apply (rule_tac n = "length (s ` giv)" in alloc_prog_LeadsTo_length_giv_disj3)
   7.645 +apply simp_all
   7.646 +apply (blast intro:)
   7.647 +apply clarify
   7.648 +apply (simp add:)
   7.649 +apply (blast dest!: prefix_length_le intro: lt_trans2)
   7.650 +done
   7.651 +
   7.652 +
   7.653 +(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   7.654 +lemma alloc_prog_LeadsTo_length_ask_giv2:
   7.655 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.656 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.657 +    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   7.658 +    alloc_prog Join G \<in>
   7.659 +      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   7.660 +    alloc_prog Join G \<in>
   7.661 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.662 +  ==> alloc_prog Join G \<in>
   7.663 +        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   7.664 +        LeadsTo
   7.665 +          {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   7.666 +                     length(s`giv) < length(s`ask) & length(s`giv) = n) |
   7.667 +                    n < length(s`giv)}"
   7.668 +apply (rule LeadsTo_weaken_R)
   7.669 +apply (erule Always_LeadsToD [OF asm_rl alloc_prog_LeadsTo_length_ask_giv])
   7.670 +apply assumption+
   7.671 +apply clarify
   7.672 +apply (simp add: INT_iff)
   7.673 +apply clarify
   7.674 +apply (drule_tac x = "length (x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
   7.675 +apply (simp add:)
   7.676 +apply (blast intro: le_trans)
   7.677 +done
   7.678 +
   7.679 +(*Eighth step in proof of (31): by (50), we get |giv| > n. *)
   7.680 +lemma alloc_prog_LeadsTo_extend_giv:
   7.681 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.682 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.683 +    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   7.684 +    alloc_prog Join G \<in>
   7.685 +      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   7.686 +    alloc_prog Join G \<in>
   7.687 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.688 +  ==> alloc_prog Join G \<in>
   7.689 +        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   7.690 +        LeadsTo {s\<in>state. n < length(s`giv)}"
   7.691 +apply (rule LeadsTo_Un_duplicate)
   7.692 +apply (rule LeadsTo_cancel1)
   7.693 +apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
   7.694 +apply safe;
   7.695 + prefer 2 apply (simp add: lt_nat_in_nat)
   7.696 +apply (rule LeadsTo_weaken_R)
   7.697 +apply (rule alloc_prog_LeadsTo_length_ask_giv2)
   7.698 +apply auto
   7.699 +done
   7.700 +
   7.701 +(*Ninth and tenth steps in proof of (31): by (50), we get |giv| > n.
   7.702 +  The report has an error: putting |ask|=k for the precondition fails because
   7.703 +  we can't expect |ask| to remain fixed until |giv| increases.*)
   7.704 +lemma alloc_prog_ask_LeadsTo_giv:
   7.705 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.706 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.707 +    G \<in> program; alloc_prog ok G;  k \<in> nat;
   7.708 +    alloc_prog Join G \<in>
   7.709 +      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   7.710 +    alloc_prog Join G \<in>
   7.711 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.712 +  ==> alloc_prog Join G \<in>
   7.713 +        {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
   7.714 +(* Proof by induction over the difference between k and n *)
   7.715 +apply (rule_tac f = "\<lambda>s\<in>state. k #- length (s`giv)" in LessThan_induct)
   7.716 +apply (simp_all add: lam_def)
   7.717 + prefer 2 apply (force)
   7.718 +apply clarify
   7.719 +apply (simp add: Collect_vimage_eq)
   7.720 +apply (rule single_LeadsTo_I)
   7.721 +apply safe
   7.722 +apply simp
   7.723 +apply (rename_tac "s0")
   7.724 +apply (case_tac "length (s0 ` giv) < length (s0 ` ask) ")
   7.725 + apply (rule_tac [2] subset_imp_LeadsTo)
   7.726 +  apply safe
   7.727 + prefer 2 
   7.728 + apply (simp add: not_lt_iff_le)
   7.729 + apply (blast dest: le_imp_not_lt intro: lt_trans2)
   7.730 +apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
   7.731 +       in Increasing_imp_Stable [THEN PSP_StableI])
   7.732 +apply assumption
   7.733 +apply (simp add:)
   7.734 +apply (force simp add:)
   7.735 +apply (rule LeadsTo_weaken)
   7.736 +apply (rule_tac n = "length (s0 ` giv)" and k = "length (s0 ` ask)" 
   7.737 +       in alloc_prog_LeadsTo_extend_giv)
   7.738 +apply simp_all
   7.739 + apply (force simp add:)
   7.740 +apply clarify
   7.741 +apply (simp add:)
   7.742 +apply (erule disjE)
   7.743 + apply (blast dest!: prefix_length_le intro: lt_trans2)
   7.744 +apply (rule not_lt_imp_le)
   7.745 +apply clarify
   7.746 +apply (simp_all add: leI diff_lt_iff_lt)
   7.747 +done
   7.748 +
   7.749 +(*Final lemma: combine previous result with lemma (30)*)
   7.750 +lemma alloc_prog_progress_lemma:
   7.751 +"[| alloc_prog Join G \<in> Incr(lift(rel));
   7.752 +    alloc_prog Join G \<in> Incr(lift(ask));
   7.753 +    G \<in> program; alloc_prog ok G;  h \<in> list(tokbag);
   7.754 +    alloc_prog Join G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   7.755 +    alloc_prog Join G \<in>
   7.756 +       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
   7.757 +                 {s\<in>state. k \<le> tokens(s`rel)}) |]
   7.758 +  ==> alloc_prog Join G \<in>
   7.759 +        {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   7.760 +        {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   7.761 +apply (rule single_LeadsTo_I)
   7.762 + prefer 2 apply (simp)
   7.763 +apply (rename_tac s0)
   7.764 +apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
   7.765 +       in Increasing_imp_Stable [THEN PSP_StableI])
   7.766 +   apply assumption
   7.767 +  prefer 2 apply (force simp add:)
   7.768 +apply (simp_all add: Int_cons_left)
   7.769 +apply (rule LeadsTo_weaken)
   7.770 +apply (rule_tac k1 = "length (s0 ` ask)" 
   7.771 +       in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
   7.772 +                              alloc_prog_ask_LeadsTo_giv])
   7.773 +apply simp_all
   7.774 +apply (force simp add:)
   7.775 +apply (force simp add:)
   7.776 +apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le lt_trans2)
   7.777 +done
   7.778 +
   7.779 +(** alloc_prog liveness property (31), page 18 **)
   7.780 +
   7.781 +(*missing the LeadsTo assumption on the lhs!?!?!*)
   7.782 +lemma alloc_prog_progress:
   7.783 +"alloc_prog \<in>
   7.784 +    Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
   7.785 +    Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
   7.786 +    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
   7.787 +              {s\<in>state. k \<le> tokens(s`rel)})
   7.788 +  guarantees (\<Inter>h \<in> list(tokbag).
   7.789 +              {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   7.790 +              {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
   7.791 +apply (rule guaranteesI)
   7.792 +apply (rule INT_I)
   7.793 +apply (rule alloc_prog_progress_lemma)
   7.794 +apply simp_all
   7.795 +apply (blast intro:)
   7.796 +done
   7.797 +
   7.798 +
   7.799 +end
     8.1 --- a/src/ZF/UNITY/ClientImpl.ML	Thu Jun 19 18:40:39 2003 +0200
     8.2 +++ b/src/ZF/UNITY/ClientImpl.ML	Fri Jun 20 12:10:45 2003 +0200
     8.3 @@ -191,7 +191,7 @@
     8.4  by (auto_tac (claset(), 
     8.5                simpset() addsimps [prefix_def, Ge_def]));
     8.6  by (dtac strict_prefix_length_lt 1);
     8.7 -by (dres_inst_tac [("x", "length(x`rel)")] bspec 1);
     8.8 +by (dres_inst_tac [("x", "length(x`rel)")] spec 1);
     8.9  by Auto_tac;
    8.10  by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
    8.11  by (auto_tac (claset(), simpset() addsimps [id_def, lam_def]));
     9.1 --- a/src/ZF/UNITY/Constrains.ML	Thu Jun 19 18:40:39 2003 +0200
     9.2 +++ b/src/ZF/UNITY/Constrains.ML	Fri Jun 20 12:10:45 2003 +0200
     9.3 @@ -434,7 +434,7 @@
     9.4  
     9.5  (*proves "co" properties when the program is specified*)
     9.6  
     9.7 -fun constrains_tac i = 
     9.8 +fun gen_constrains_tac(cs,ss) i = 
     9.9     SELECT_GOAL
    9.10        (EVERY [REPEAT (Always_Int_tac 1),
    9.11                REPEAT (etac Always_ConstrainsI 1
    9.12 @@ -445,14 +445,16 @@
    9.13                (* Three subgoals *)
    9.14                rewrite_goal_tac [st_set_def] 3,
    9.15                REPEAT (Force_tac 2),
    9.16 -              full_simp_tac (simpset() addsimps !program_defs_ref) 1,
    9.17 -              ALLGOALS Clarify_tac,
    9.18 +              full_simp_tac (ss addsimps !program_defs_ref) 1,
    9.19 +              ALLGOALS (clarify_tac cs),
    9.20                REPEAT (FIRSTGOAL (etac disjE)),
    9.21                ALLGOALS Clarify_tac,
    9.22                REPEAT (FIRSTGOAL (etac disjE)),
    9.23 -              ALLGOALS Clarify_tac,
    9.24 -              ALLGOALS Asm_full_simp_tac,
    9.25 -              ALLGOALS Clarify_tac]) i;
    9.26 +              ALLGOALS (clarify_tac cs),
    9.27 +              ALLGOALS (asm_full_simp_tac ss),
    9.28 +              ALLGOALS (clarify_tac cs)]) i;
    9.29 +
    9.30 +fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
    9.31  
    9.32  (*For proving invariants*)
    9.33  fun always_tac i = 
    10.1 --- a/src/ZF/UNITY/GenPrefix.ML	Thu Jun 19 18:40:39 2003 +0200
    10.2 +++ b/src/ZF/UNITY/GenPrefix.ML	Fri Jun 20 12:10:45 2003 +0200
    10.3 @@ -12,13 +12,13 @@
    10.4  *)
    10.5  
    10.6  Goalw [refl_def]
    10.7 - "[| refl(A, r); x:A |] ==> <x,x>:r";
    10.8 + "[| refl(A, r); x \\<in> A |] ==> <x,x>:r";
    10.9  by Auto_tac;
   10.10  qed "reflD";
   10.11  
   10.12  (*** preliminary lemmas ***)
   10.13  
   10.14 -Goal "xs:list(A) ==> <[], xs>:gen_prefix(A, r)";
   10.15 +Goal "xs \\<in> list(A) ==> <[], xs> \\<in> gen_prefix(A, r)";
   10.16  by (dtac (rotate_prems  1 gen_prefix.append) 1);
   10.17  by (rtac gen_prefix.Nil 1);
   10.18  by Auto_tac;
   10.19 @@ -26,19 +26,19 @@
   10.20  Addsimps [Nil_gen_prefix];
   10.21  
   10.22  
   10.23 -Goal "<xs,ys>:gen_prefix(A, r) ==> length(xs) le length(ys)";
   10.24 +Goal "<xs,ys> \\<in> gen_prefix(A, r) ==> length(xs) \\<le> length(ys)";
   10.25  by (etac gen_prefix.induct 1);
   10.26 -by (subgoal_tac "ys:list(A)" 3);
   10.27 +by (subgoal_tac "ys \\<in> list(A)" 3);
   10.28  by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
   10.29                         addIs [le_trans], 
   10.30                simpset() addsimps [length_app]));
   10.31  qed "gen_prefix_length_le";
   10.32  
   10.33  
   10.34 -Goal "[| <xs', ys'>:gen_prefix(A, r) |] \
   10.35 -\  ==> (ALL x xs. x:A --> xs'= Cons(x,xs) --> \
   10.36 -\      (EX y ys. y:A & ys' = Cons(y,ys) &\
   10.37 -\      <x,y>:r & <xs, ys>:gen_prefix(A, r)))";
   10.38 +Goal "[| <xs', ys'> \\<in> gen_prefix(A, r) |] \
   10.39 +\  ==> (\\<forall>x xs. x \\<in> A --> xs'= Cons(x,xs) --> \
   10.40 +\      (\\<exists>y ys. y \\<in> A & ys' = Cons(y,ys) &\
   10.41 +\      <x,y>:r & <xs, ys> \\<in> gen_prefix(A, r)))";
   10.42  by (etac gen_prefix.induct 1);
   10.43  by (force_tac (claset() addIs [gen_prefix.append],
   10.44                 simpset()) 3);
   10.45 @@ -47,9 +47,9 @@
   10.46  
   10.47  (*As usual converting it to an elimination rule is tiresome*)
   10.48  val major::prems = 
   10.49 -Goal "[| <Cons(x,xs), zs>:gen_prefix(A, r); \
   10.50 -\   !!y ys. [|zs = Cons(y, ys); y:A; x:A; <x,y>:r; \
   10.51 -\     <xs,ys>:gen_prefix(A, r) |] ==> P \
   10.52 +Goal "[| <Cons(x,xs), zs> \\<in> gen_prefix(A, r); \
   10.53 +\   !!y ys. [|zs = Cons(y, ys); y \\<in> A; x \\<in> A; <x,y>:r; \
   10.54 +\     <xs,ys> \\<in> gen_prefix(A, r) |] ==> P \
   10.55  \     |] ==> P";
   10.56  by (cut_facts_tac [major] 1);
   10.57  by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
   10.58 @@ -65,8 +65,8 @@
   10.59  AddSEs [Cons_gen_prefixE];
   10.60  
   10.61  Goal 
   10.62 -"(<Cons(x,xs),Cons(y,ys)>:gen_prefix(A, r)) \
   10.63 -\ <-> (x:A & y:A & <x,y>:r & <xs,ys>:gen_prefix(A, r))";
   10.64 +"(<Cons(x,xs),Cons(y,ys)> \\<in> gen_prefix(A, r)) \
   10.65 +\ <-> (x \\<in> A & y \\<in> A & <x,y>:r & <xs,ys> \\<in> gen_prefix(A, r))";
   10.66  by (auto_tac (claset() addIs [gen_prefix.prepend], simpset()));
   10.67  qed"Cons_gen_prefix_Cons";
   10.68  AddIffs [Cons_gen_prefix_Cons];
   10.69 @@ -88,8 +88,8 @@
   10.70  by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
   10.71  by (Clarify_tac 1);
   10.72  by (etac rev_mp 1);
   10.73 -by (eres_inst_tac [("P", "y:list(A)")] rev_mp 1);
   10.74 -by (eres_inst_tac [("P", "xa:list(A)")] rev_mp 1);
   10.75 +by (eres_inst_tac [("P", "y \\<in> list(A)")] rev_mp 1);
   10.76 +by (eres_inst_tac [("P", "xa \\<in> list(A)")] rev_mp 1);
   10.77  by (etac gen_prefix.induct 1);
   10.78  by (Asm_simp_tac 1);
   10.79  by (Clarify_tac 1);
   10.80 @@ -119,8 +119,8 @@
   10.81  (* Transitivity *)
   10.82  (* A lemma for proving gen_prefix_trans_comp *)
   10.83  
   10.84 -Goal "xs:list(A) ==> \
   10.85 -\  ALL zs. <xs @ ys, zs>:gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
   10.86 +Goal "xs \\<in> list(A) ==> \
   10.87 +\  \\<forall>zs. <xs @ ys, zs> \\<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
   10.88  by (etac list.induct 1);
   10.89  by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
   10.90  qed_spec_mp "append_gen_prefix";
   10.91 @@ -128,10 +128,10 @@
   10.92  (* Lemma proving transitivity and more*)
   10.93  
   10.94  Goal "<x, y>: gen_prefix(A, r) ==> \
   10.95 -\  (ALL z:list(A). <y,z>:gen_prefix(A, s)--><x, z>:gen_prefix(A, s O r))";
   10.96 +\  (\\<forall>z \\<in> list(A). <y,z> \\<in> gen_prefix(A, s)--><x, z> \\<in> gen_prefix(A, s O r))";
   10.97  by (etac gen_prefix.induct 1);
   10.98  by (auto_tac (claset() addEs [ConsE], simpset() addsimps [Nil_gen_prefix]));
   10.99 -by (subgoal_tac "ys:list(A)" 1);
  10.100 +by (subgoal_tac "ys \\<in> list(A)" 1);
  10.101  by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
  10.102  by (dres_inst_tac [("xs", "ys"), ("r", "s")] append_gen_prefix 1);
  10.103  by Auto_tac;
  10.104 @@ -158,9 +158,9 @@
  10.105  qed "trans_on_gen_prefix";
  10.106  
  10.107  Goalw [prefix_def]
  10.108 -"[| <x,y>:prefix(A); <y, z>:gen_prefix(A, r); r<=A*A |] \
  10.109 -\ ==>  <x, z>:gen_prefix(A, r)";
  10.110 -by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")]
  10.111 +"[| <x,y> \\<in> prefix(A); <y, z> \\<in> gen_prefix(A, r); r<=A*A |] \
  10.112 +\ ==>  <x, z> \\<in> gen_prefix(A, r)";
  10.113 +by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")]
  10.114               (right_comp_id RS subst) 1);
  10.115  by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp, 
  10.116                    gen_prefix.dom_subset RS subsetD]) 1));
  10.117 @@ -168,16 +168,16 @@
  10.118  
  10.119  
  10.120  Goalw [prefix_def]
  10.121 -"[| <x,y>:gen_prefix(A,r); <y, z>:prefix(A); r<=A*A |] \
  10.122 -\ ==>  <x, z>:gen_prefix(A, r)";
  10.123 -by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")] (left_comp_id RS subst) 1);
  10.124 +"[| <x,y> \\<in> gen_prefix(A,r); <y, z> \\<in> prefix(A); r<=A*A |] \
  10.125 +\ ==>  <x, z> \\<in> gen_prefix(A, r)";
  10.126 +by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")] (left_comp_id RS subst) 1);
  10.127  by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp, 
  10.128                                        gen_prefix.dom_subset RS subsetD]) 1));
  10.129  qed_spec_mp "gen_prefix_prefix_trans";
  10.130  
  10.131  (** Antisymmetry **)
  10.132  
  10.133 -Goal "n:nat ==> ALL b:nat. n #+ b le n --> b = 0";
  10.134 +Goal "n \\<in> nat ==> \\<forall>b \\<in> nat. n #+ b \\<le> n --> b = 0";
  10.135  by (induct_tac "n" 1);
  10.136  by Auto_tac;
  10.137  qed_spec_mp "nat_le_lemma";
  10.138 @@ -192,11 +192,11 @@
  10.139  (*append case is hardest*)
  10.140  by (Clarify_tac 1);
  10.141  by (subgoal_tac "length(zs) = 0" 1);
  10.142 -by (subgoal_tac "ys:list(A)" 1);
  10.143 +by (subgoal_tac "ys \\<in> list(A)" 1);
  10.144  by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
  10.145 -by (dres_inst_tac [("psi", "<ys @ zs, xs>:gen_prefix(A,r)")] asm_rl 1);
  10.146 +by (dres_inst_tac [("psi", "<ys @ zs, xs> \\<in> gen_prefix(A,r)")] asm_rl 1);
  10.147  by (Asm_full_simp_tac 1);
  10.148 -by (subgoal_tac "length(ys @ zs)  = length(ys) #+ length(zs) &ys:list(A)&xs:list(A)" 1);
  10.149 +by (subgoal_tac "length(ys @ zs)  = length(ys) #+ length(zs) &ys \\<in> list(A)&xs \\<in> list(A)" 1);
  10.150  by (blast_tac (claset() addIs [length_app] 
  10.151                          addDs [gen_prefix.dom_subset RS subsetD]) 2);
  10.152  by (REPEAT (dtac gen_prefix_length_le 1));
  10.153 @@ -209,41 +209,41 @@
  10.154  
  10.155  (*** recursion equations ***)
  10.156  
  10.157 -Goal "xs:list(A) ==> <xs, []>:gen_prefix(A,r) <-> (xs = [])";
  10.158 +Goal "xs \\<in> list(A) ==> <xs, []> \\<in> gen_prefix(A,r) <-> (xs = [])";
  10.159  by (induct_tac "xs" 1);
  10.160  by Auto_tac;
  10.161  qed "gen_prefix_Nil";
  10.162  Addsimps [gen_prefix_Nil];
  10.163  
  10.164  Goalw [refl_def]
  10.165 - "[| refl(A, r);  xs:list(A) |] ==> \
  10.166 -\   <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs>:gen_prefix(A, r)";
  10.167 + "[| refl(A, r);  xs \\<in> list(A) |] ==> \
  10.168 +\   <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \\<in> gen_prefix(A, r)";
  10.169  by (induct_tac "xs" 1);
  10.170  by (ALLGOALS Asm_simp_tac);
  10.171  qed "same_gen_prefix_gen_prefix";
  10.172  Addsimps [same_gen_prefix_gen_prefix];
  10.173  
  10.174 -Goal "[| xs:list(A); ys:list(A); y:A |] ==> \
  10.175 +Goal "[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
  10.176  \   <xs, Cons(y,ys)> : gen_prefix(A,r)  <-> \
  10.177 -\     (xs=[] | (EX z zs. xs=Cons(z,zs) & z:A & <z,y>:r & <zs,ys>:gen_prefix(A,r)))";
  10.178 +\     (xs=[] | (\\<exists>z zs. xs=Cons(z,zs) & z \\<in> A & <z,y>:r & <zs,ys> \\<in> gen_prefix(A,r)))";
  10.179  by (induct_tac "xs" 1);
  10.180  by Auto_tac;
  10.181  qed "gen_prefix_Cons";
  10.182  
  10.183 -Goal "[| refl(A,r);  <xs,ys>:gen_prefix(A, r); zs:list(A) |] \
  10.184 +Goal "[| refl(A,r);  <xs,ys> \\<in> gen_prefix(A, r); zs \\<in> list(A) |] \
  10.185  \     ==>  <xs@zs, take(length(xs), ys) @ zs> : gen_prefix(A, r)";
  10.186  by (etac gen_prefix.induct 1);
  10.187  by (Asm_simp_tac 1);
  10.188  by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD]));
  10.189  by Auto_tac;
  10.190  by (ftac gen_prefix_length_le 1);
  10.191 -by (subgoal_tac "take(length(xs), ys):list(A)" 1);
  10.192 +by (subgoal_tac "take(length(xs), ys) \\<in> list(A)" 1);
  10.193  by (ALLGOALS (asm_simp_tac (simpset() addsimps 
  10.194           [diff_is_0_iff RS iffD2, take_type ])));
  10.195  qed "gen_prefix_take_append";
  10.196  
  10.197 -Goal "[| refl(A, r);  <xs,ys>:gen_prefix(A,r);   \
  10.198 -\        length(xs) = length(ys); zs:list(A) |] \
  10.199 +Goal "[| refl(A, r);  <xs,ys> \\<in> gen_prefix(A,r);   \
  10.200 +\        length(xs) = length(ys); zs \\<in> list(A) |] \
  10.201  \     ==>  <xs@zs, ys @ zs> : gen_prefix(A, r)";
  10.202  by (dres_inst_tac [("zs", "zs")]  gen_prefix_take_append 1);
  10.203  by (REPEAT(assume_tac 1));
  10.204 @@ -254,13 +254,13 @@
  10.205  qed "gen_prefix_append_both";
  10.206  
  10.207  (*NOT suitable for rewriting since [y] has the form y#ys*)
  10.208 -Goal "xs:list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
  10.209 +Goal "xs \\<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
  10.210  by (auto_tac (claset(), simpset() addsimps [app_assoc]));
  10.211  qed "append_cons_conv";
  10.212  
  10.213 -Goal "[| <xs,ys>:gen_prefix(A, r);  refl(A, r) |] \
  10.214 +Goal "[| <xs,ys> \\<in> gen_prefix(A, r);  refl(A, r) |] \
  10.215  \     ==> length(xs) < length(ys) --> \
  10.216 -\         <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
  10.217 +\         <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
  10.218  by (etac gen_prefix.induct 1);
  10.219  by (Blast_tac 1);
  10.220  by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
  10.221 @@ -290,51 +290,52 @@
  10.222  val append_one_gen_prefix_lemma = result() RS mp;
  10.223  
  10.224  Goal "[| <xs,ys>: gen_prefix(A, r);  length(xs) < length(ys);  refl(A, r) |] \
  10.225 -\     ==> <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
  10.226 +\     ==> <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
  10.227  by (blast_tac (claset() addIs [append_one_gen_prefix_lemma]) 1);
  10.228  qed "append_one_gen_prefix";
  10.229  
  10.230  
  10.231  (** Proving the equivalence with Charpentier's definition **)
  10.232  
  10.233 -Goal "xs:list(A) ==>  \
  10.234 -\ ALL ys:list(A). ALL i:nat. i < length(xs) \
  10.235 +Goal "xs \\<in> list(A) ==>  \
  10.236 +\ \\<forall>ys \\<in> list(A). \\<forall>i \\<in> nat. i < length(xs) \
  10.237  \         --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r";
  10.238  by (induct_tac "xs" 1);
  10.239  by (ALLGOALS(Clarify_tac));
  10.240  by (ALLGOALS(Asm_full_simp_tac));
  10.241  by (etac natE 1);
  10.242  by (ALLGOALS(Asm_full_simp_tac));
  10.243 -qed_spec_mp "gen_prefix_imp_nth";
  10.244 +qed_spec_mp "gen_prefix_imp_nth_lemma";
  10.245  
  10.246 -Goal "xs:list(A) ==> \
  10.247 -\ ALL ys:list(A). length(xs) le length(ys)  \
  10.248 -\     --> (ALL i:nat. i < length(xs)--> <nth(i, xs), nth(i,ys)>:r)  \
  10.249 -\     --> <xs, ys> : gen_prefix(A, r)";
  10.250 +Goal "[| <xs,ys> \\<in> gen_prefix(A,r); i < length(xs)|] \
  10.251 +\     ==> <nth(i, xs), nth(i, ys)>:r";
  10.252 +by (cut_inst_tac [("A","A")] gen_prefix.dom_subset 1); 
  10.253 +by (rtac gen_prefix_imp_nth_lemma 1);
  10.254 +by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat]));  
  10.255 +qed "gen_prefix_imp_nth";
  10.256 +
  10.257 +Goal "xs \\<in> list(A) ==> \
  10.258 +\ \\<forall>ys \\<in> list(A). length(xs) \\<le> length(ys)  \
  10.259 +\     --> (\\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)  \
  10.260 +\     --> <xs, ys> \\<in> gen_prefix(A, r)";
  10.261  by (induct_tac "xs" 1);
  10.262 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj]))); 
  10.263 +by (ALLGOALS Asm_simp_tac); 
  10.264  by (Clarify_tac 1);
  10.265 -by (eres_inst_tac [("a","ys")] list.elim 1); 
  10.266 -by (ALLGOALS Asm_full_simp_tac);
  10.267 -by (Clarify_tac 1);
  10.268 -by (rename_tac "zs" 1);
  10.269 -by (dres_inst_tac [("x", "zs")] bspec 1);
  10.270 -by (ALLGOALS(Clarify_tac));
  10.271 -(*Faster than Auto_tac*)
  10.272 -by (rtac conjI 1); 
  10.273 -by (REPEAT (Force_tac 1));
  10.274 +by (eres_inst_tac [("a","ys")] list.elim 1);
  10.275 +by (asm_full_simp_tac (simpset() addsimps []) 1);  
  10.276 +by (force_tac (claset() addSIs [nat_0_le], simpset() addsimps [lt_nat_in_nat]) 1); 
  10.277  qed_spec_mp "nth_imp_gen_prefix";
  10.278  
  10.279 -Goal "(<xs,ys>: gen_prefix(A,r)) <-> \
  10.280 -\ (xs:list(A) & ys:list(A) & length(xs) le length(ys) & \
  10.281 -\ (ALL i:nat. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
  10.282 +Goal "(<xs,ys> : gen_prefix(A,r)) <-> \
  10.283 +\     (xs \\<in> list(A) & ys \\<in> list(A) & length(xs) \\<le> length(ys) & \
  10.284 +\     (\\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
  10.285  by (rtac iffI 1);
  10.286  by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
  10.287  by (ftac gen_prefix_length_le 1);
  10.288  by (ALLGOALS(Clarify_tac));
  10.289  by (rtac nth_imp_gen_prefix 2);
  10.290 -by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1);
  10.291 -by Auto_tac;
  10.292 +by (dtac gen_prefix_imp_nth 1);
  10.293 +by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat])); 
  10.294  qed "gen_prefix_iff_nth";
  10.295  
  10.296  (** prefix is a partial order: **)
  10.297 @@ -363,44 +364,44 @@
  10.298  (* Monotonicity of "set" operator WRT prefix *)
  10.299  
  10.300  Goalw [prefix_def] 
  10.301 -"<xs,ys>:prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
  10.302 +"<xs,ys> \\<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
  10.303  by (etac gen_prefix.induct 1);
  10.304 -by (subgoal_tac "xs:list(A)&ys:list(A)" 3);
  10.305 +by (subgoal_tac "xs \\<in> list(A)&ys \\<in> list(A)" 3);
  10.306  by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 4);
  10.307  by (auto_tac (claset(), simpset() addsimps [set_of_list_append]));
  10.308  qed "set_of_list_prefix_mono";  
  10.309  
  10.310  (** recursion equations **)
  10.311  
  10.312 -Goalw [prefix_def] "xs:list(A) ==> <[],xs>:prefix(A)";
  10.313 +Goalw [prefix_def] "xs \\<in> list(A) ==> <[],xs> \\<in> prefix(A)";
  10.314  by (asm_simp_tac (simpset() addsimps [Nil_gen_prefix]) 1);
  10.315  qed "Nil_prefix";
  10.316  Addsimps[Nil_prefix];
  10.317  
  10.318  
  10.319 -Goalw [prefix_def] "<xs, []>:prefix(A) <-> (xs = [])";
  10.320 +Goalw [prefix_def] "<xs, []> \\<in> prefix(A) <-> (xs = [])";
  10.321  by Auto_tac;
  10.322  by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
  10.323 -by (dres_inst_tac [("psi", "<xs, []>:gen_prefix(A, id(A))")] asm_rl 1);
  10.324 +by (dres_inst_tac [("psi", "<xs, []> \\<in> gen_prefix(A, id(A))")] asm_rl 1);
  10.325  by (asm_full_simp_tac (simpset() addsimps [gen_prefix_Nil]) 1);
  10.326  qed "prefix_Nil";
  10.327  AddIffs [prefix_Nil];
  10.328  
  10.329  Goalw [prefix_def] 
  10.330 -"<Cons(x,xs), Cons(y,ys)>:prefix(A) <-> (x=y & <xs,ys>:prefix(A) & y:A)";
  10.331 +"<Cons(x,xs), Cons(y,ys)> \\<in> prefix(A) <-> (x=y & <xs,ys> \\<in> prefix(A) & y \\<in> A)";
  10.332  by Auto_tac;
  10.333  qed"Cons_prefix_Cons";
  10.334  AddIffs [Cons_prefix_Cons];
  10.335  
  10.336  Goalw [prefix_def] 
  10.337 -"xs:list(A)==> <xs@ys,xs@zs>:prefix(A) <-> (<ys,zs>:prefix(A))";
  10.338 +"xs \\<in> list(A)==> <xs@ys,xs@zs> \\<in> prefix(A) <-> (<ys,zs> \\<in> prefix(A))";
  10.339  by (subgoal_tac "refl(A,id(A))" 1);
  10.340  by (Asm_simp_tac 1);
  10.341  by (auto_tac (claset(), simpset() addsimps[refl_def]));
  10.342  qed "same_prefix_prefix";
  10.343  Addsimps [same_prefix_prefix];
  10.344  
  10.345 -Goal "xs:list(A) ==> <xs@ys,xs>:prefix(A) <-> (<ys,[]>:prefix(A))";
  10.346 +Goal "xs \\<in> list(A) ==> <xs@ys,xs> \\<in> prefix(A) <-> (<ys,[]> \\<in> prefix(A))";
  10.347  by (res_inst_tac [("P", "%x. <?u, x>:?v <-> ?w(x)")] (app_right_Nil RS subst) 1);
  10.348  by (rtac same_prefix_prefix 2);
  10.349  by Auto_tac;
  10.350 @@ -408,37 +409,37 @@
  10.351  Addsimps [same_prefix_prefix_Nil];
  10.352  
  10.353  Goalw [prefix_def] 
  10.354 -"[| <xs,ys>:prefix(A); zs:list(A) |] ==> <xs,ys@zs>:prefix(A)";
  10.355 +"[| <xs,ys> \\<in> prefix(A); zs \\<in> list(A) |] ==> <xs,ys@zs> \\<in> prefix(A)";
  10.356  by (etac gen_prefix.append 1);
  10.357  by (assume_tac 1);
  10.358  qed "prefix_appendI";
  10.359  Addsimps [prefix_appendI];
  10.360  
  10.361  Goalw [prefix_def] 
  10.362 -"[| xs:list(A); ys:list(A); y:A |] ==> \
  10.363 -\ <xs,Cons(y,ys)>:prefix(A) <-> \
  10.364 -\ (xs=[] | (EX zs. xs=Cons(y,zs) & <zs,ys>:prefix(A)))";
  10.365 +"[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
  10.366 +\ <xs,Cons(y,ys)> \\<in> prefix(A) <-> \
  10.367 +\ (xs=[] | (\\<exists>zs. xs=Cons(y,zs) & <zs,ys> \\<in> prefix(A)))";
  10.368  by (auto_tac (claset(), simpset() addsimps [gen_prefix_Cons]));
  10.369  qed "prefix_Cons";
  10.370  
  10.371  Goalw [prefix_def]
  10.372 -  "[| <xs,ys>:prefix(A); length(xs) < length(ys) |] \
  10.373 -\ ==> <xs @ [nth(length(xs),ys)], ys>:prefix(A)";
  10.374 +  "[| <xs,ys> \\<in> prefix(A); length(xs) < length(ys) |] \
  10.375 +\ ==> <xs @ [nth(length(xs),ys)], ys> \\<in> prefix(A)";
  10.376  by (subgoal_tac "refl(A, id(A))" 1);
  10.377  by (asm_simp_tac (simpset() addsimps [append_one_gen_prefix]) 1);
  10.378  by (auto_tac (claset(), simpset() addsimps [refl_def]));
  10.379  qed "append_one_prefix";
  10.380  
  10.381  Goalw [prefix_def] 
  10.382 -"<xs,ys>:prefix(A) ==> length(xs) le length(ys)";
  10.383 +"<xs,ys> \\<in> prefix(A) ==> length(xs) \\<le> length(ys)";
  10.384  by (blast_tac (claset() addDs [gen_prefix_length_le]) 1);
  10.385  qed "prefix_length_le";
  10.386  
  10.387  Goalw [prefix_def] 
  10.388 -"<xs,ys>:prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
  10.389 +"<xs,ys> \\<in> prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
  10.390  by (etac gen_prefix.induct 1);
  10.391  by (Clarify_tac 1);
  10.392 -by (ALLGOALS(subgoal_tac "ys:list(A)&xs:list(A)"));
  10.393 +by (ALLGOALS(subgoal_tac "ys \\<in> list(A)&xs \\<in> list(A)"));
  10.394  by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], 
  10.395               simpset() addsimps [length_app, length_type]));
  10.396  by (subgoal_tac "length(zs)=0" 1);
  10.397 @@ -465,12 +466,11 @@
  10.398  
  10.399  (*Equivalence to the definition used in Lex/Prefix.thy*)
  10.400  Goalw [prefix_def]
  10.401 -"<xs,zs>:prefix(A) <-> (EX ys:list(A). zs = xs@ys) & xs:list(A)";
  10.402 +    "<xs,zs> \\<in> prefix(A) <-> (\\<exists>ys \\<in> list(A). zs = xs@ys) & xs \\<in> list(A)";
  10.403  by (auto_tac (claset(),
  10.404 -       simpset() addsimps [gen_prefix_iff_nth, 
  10.405 +       simpset() addsimps [gen_prefix_iff_nth, lt_nat_in_nat,
  10.406                             nth_append, nth_type, app_type, length_app]));
  10.407 -by (subgoal_tac "length(xs):nat&length(zs):nat & \
  10.408 -\                drop(length(xs), zs):list(A)" 1);
  10.409 +by (subgoal_tac "drop(length(xs), zs) \\<in> list(A)" 1);
  10.410  by (res_inst_tac [("x", "drop(length(xs), zs)")] bexI 1);
  10.411  by (ALLGOALS(Clarify_tac));
  10.412  by (asm_simp_tac (simpset() addsimps [length_type, drop_type]) 2);
  10.413 @@ -483,17 +483,14 @@
  10.414  by (dres_inst_tac [("i", "length(zs)")] leI 1);
  10.415  by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1);
  10.416  by Safe_tac;
  10.417 -by (Blast_tac 1);
  10.418  by (subgoal_tac "length(xs) #+ (i #- length(xs)) = i" 1);
  10.419  by (stac nth_drop 1);
  10.420 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI])));
  10.421 -by (rtac (nat_diff_split RS iffD2) 1);
  10.422 -by Auto_tac;
  10.423 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI] addsplits [nat_diff_split])));
  10.424  qed "prefix_iff";
  10.425  
  10.426  Goal 
  10.427 -"[|xs:list(A); ys:list(A); y:A |] ==> \
  10.428 -\  <xs, ys@[y]>:prefix(A) <-> (xs = ys@[y] | <xs,ys>:prefix(A))";
  10.429 +"[|xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
  10.430 +\  <xs, ys@[y]> \\<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \\<in> prefix(A))";
  10.431  by (simp_tac (simpset() addsimps [prefix_iff]) 1);
  10.432  by (rtac iffI 1);
  10.433  by (Clarify_tac 1);
  10.434 @@ -504,9 +501,9 @@
  10.435  qed "prefix_snoc";
  10.436  Addsimps [prefix_snoc];
  10.437  
  10.438 -Goal "zs:list(A) ==> ALL xs:list(A). ALL ys:list(A). \
  10.439 -\  (<xs, ys@zs>:prefix(A)) <-> \
  10.440 -\ (<xs,ys>:prefix(A) | (EX us. xs = ys@us & <us,zs>:prefix(A)))";
  10.441 +Goal "zs \\<in> list(A) ==> \\<forall>xs \\<in> list(A). \\<forall>ys \\<in> list(A). \
  10.442 +\  (<xs, ys@zs> \\<in> prefix(A)) <-> \
  10.443 +\ (<xs,ys> \\<in> prefix(A) | (\\<exists>us. xs = ys@us & <us,zs> \\<in> prefix(A)))";
  10.444  by (etac list_append_induct 1);
  10.445  by (Clarify_tac 2);
  10.446  by (rtac iffI 2);
  10.447 @@ -521,9 +518,9 @@
  10.448  
  10.449  (*Although the prefix ordering is not linear, the prefixes of a list
  10.450    are linearly ordered.*)
  10.451 -Goal "[| zs:list(A); xs:list(A); ys:list(A) |] \
  10.452 -\  ==> <xs, zs>:prefix(A) --> <ys,zs>:prefix(A) \
  10.453 -\ --><xs,ys>:prefix(A) | <ys,xs>:prefix(A)";
  10.454 +Goal "[| zs \\<in> list(A); xs \\<in> list(A); ys \\<in> list(A) |] \
  10.455 +\  ==> <xs, zs> \\<in> prefix(A) --> <ys,zs> \\<in> prefix(A) \
  10.456 +\ --><xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
  10.457  by (etac list_append_induct 1);
  10.458  by Auto_tac;
  10.459  qed_spec_mp "common_prefix_linear";
  10.460 @@ -562,7 +559,7 @@
  10.461  qed "part_order_Le";
  10.462  Addsimps [part_order_Le];
  10.463  
  10.464 -Goal "x:list(nat) ==> x pfixLe x";
  10.465 +Goal "x \\<in> list(nat) ==> x pfixLe x";
  10.466  by (blast_tac (claset() addIs [refl_gen_prefix RS reflD, refl_Le]) 1);
  10.467  qed "pfixLe_refl";
  10.468  Addsimps[pfixLe_refl];
  10.469 @@ -597,7 +594,7 @@
  10.470  qed "trans_Ge";
  10.471  AddIffs [trans_Ge];
  10.472  
  10.473 -Goal "x:list(nat) ==> x pfixGe x";
  10.474 +Goal "x \\<in> list(nat) ==> x pfixGe x";
  10.475  by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1);
  10.476  qed "pfixGe_refl";
  10.477  Addsimps[pfixGe_refl];
  10.478 @@ -618,7 +615,7 @@
  10.479  (* Added by Sidi: prefix and take *)
  10.480  
  10.481  Goalw [prefix_def]
  10.482 -"<xs, ys>:prefix(A) ==> xs=take(length(xs), ys)";
  10.483 +"<xs, ys> \\<in> prefix(A) ==> xs = take(length(xs), ys)";
  10.484  by (etac gen_prefix.induct 1);
  10.485  by (subgoal_tac "length(xs):nat" 3);
  10.486  by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
  10.487 @@ -630,8 +627,20 @@
  10.488  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_is_0_iff])));
  10.489  qed "prefix_imp_take";
  10.490  
  10.491 -Goalw [prefix_def]
  10.492 -"xs:list(A) ==> ALL n:nat. <take(n, xs), xs>:prefix(A)";
  10.493 +Goal "[|<xs,ys> \\<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys";
  10.494 +by (cut_inst_tac [("A","A")] prefix_type 1);
  10.495 +by (dtac subsetD 1);
  10.496 +by Auto_tac;  
  10.497 +by (dtac prefix_imp_take 1); 
  10.498 +by (etac trans 1); 
  10.499 +by (Asm_full_simp_tac 1); 
  10.500 +qed "prefix_length_equal";
  10.501 +
  10.502 +Goal "[|<xs,ys> \\<in> prefix(A); length(ys) \\<le> length(xs)|] ==> xs = ys";
  10.503 +by (blast_tac (claset() addIs [prefix_length_equal, le_anti_sym, prefix_length_le]) 1); 
  10.504 +qed "prefix_length_le_equal";
  10.505 +
  10.506 +Goalw [prefix_def] "xs \\<in> list(A) ==> \\<forall>n \\<in> nat. <take(n, xs), xs> \\<in> prefix(A)";
  10.507  by (etac list.induct 1);
  10.508  by (Asm_full_simp_tac 1);
  10.509  by (Clarify_tac 1); 
  10.510 @@ -639,7 +648,7 @@
  10.511  by Auto_tac;
  10.512  qed_spec_mp "take_prefix";
  10.513  
  10.514 -Goal "<xs, ys>:prefix(A) <-> (xs=take(length(xs), ys) & xs:list(A) & ys:list(A))";
  10.515 +Goal "<xs,ys> \\<in> prefix(A) <-> (xs=take(length(xs), ys) & xs \\<in> list(A) & ys \\<in> list(A))";
  10.516  by (rtac iffI 1);
  10.517  by (forward_tac [prefix_type RS subsetD] 1);
  10.518  by (blast_tac (claset() addIs [prefix_imp_take]) 1);
  10.519 @@ -647,3 +656,29 @@
  10.520  by (etac ssubst 1);
  10.521  by (blast_tac (claset() addIs [take_prefix, length_type]) 1);
  10.522  qed "prefix_take_iff";
  10.523 +
  10.524 +Goal "[| <xs,ys> \\<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)";
  10.525 +by (auto_tac (claset() addSDs [gen_prefix_imp_nth],
  10.526 +              simpset() addsimps [prefix_def])); 
  10.527 +qed "prefix_imp_nth";
  10.528 +
  10.529 +val prems = Goal "[|xs \\<in> list(A); ys \\<in> list(A); length(xs) \\<le> length(ys);  \
  10.530 +\       !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]  \
  10.531 +\     ==> <xs,ys> \\<in> prefix(A)";
  10.532 +by (auto_tac (claset(), simpset() addsimps prems@[prefix_def, nth_imp_gen_prefix]));
  10.533 +by (auto_tac (claset() addSIs [nth_imp_gen_prefix], simpset() addsimps prems@[prefix_def]));
  10.534 +by (blast_tac (claset() addIs prems@[nth_type, lt_trans2]) 1); 
  10.535 +qed "nth_imp_prefix";
  10.536 +
  10.537 +
  10.538 +Goal "[|length(xs) \\<le> length(ys); \
  10.539 +\       <xs,zs> \\<in> prefix(A); <ys,zs> \\<in> prefix(A)|] ==> <xs,ys> \\<in> prefix(A)";
  10.540 +by (cut_inst_tac [("A","A")] prefix_type 1); 
  10.541 +by (rtac nth_imp_prefix 1); 
  10.542 +   by (blast_tac (claset() addIs []) 1); 
  10.543 +  by (blast_tac (claset() addIs []) 1); 
  10.544 + by (assume_tac 1); 
  10.545 +by (res_inst_tac [("b","nth(i,zs)")] trans 1); 
  10.546 + by (blast_tac (claset() addIs [prefix_imp_nth]) 1); 
  10.547 +by (blast_tac (claset() addIs [sym, prefix_imp_nth, prefix_length_le, lt_trans2]) 1); 
  10.548 +qed "length_le_prefix_imp_prefix";
  10.549 \ No newline at end of file
    11.1 --- a/src/ZF/UNITY/ROOT.ML	Thu Jun 19 18:40:39 2003 +0200
    11.2 +++ b/src/ZF/UNITY/ROOT.ML	Fri Jun 20 12:10:45 2003 +0200
    11.3 @@ -20,3 +20,4 @@
    11.4  time_use_thy "Distributor";
    11.5  time_use_thy "Merge";
    11.6  time_use_thy "ClientImpl";
    11.7 +time_use_thy "AllocImpl";
    12.1 --- a/src/ZF/UNITY/UNITY.ML	Thu Jun 19 18:40:39 2003 +0200
    12.2 +++ b/src/ZF/UNITY/UNITY.ML	Fri Jun 20 12:10:45 2003 +0200
    12.3 @@ -511,9 +511,9 @@
    12.4  
    12.5  Goalw [constrains_def, st_set_def] 
    12.6    "[| F:A co A' |] ==> A <= A'";
    12.7 -by Auto_tac;
    12.8 -by (Blast_tac 1);
    12.9 +by (Force_tac 1); 
   12.10  qed "constrains_imp_subset";
   12.11 +
   12.12  (*The reasoning is by subsets since "co" refers to single actions
   12.13    only.  So this rule isn't that useful.*)
   12.14  
    13.1 --- a/src/ZF/UNITY/UNITYMisc.ML	Thu Jun 19 18:40:39 2003 +0200
    13.2 +++ b/src/ZF/UNITY/UNITYMisc.ML	Fri Jun 20 12:10:45 2003 +0200
    13.3 @@ -51,6 +51,8 @@
    13.4  AddIffs [Collect_Int2, Collect_Int3];
    13.5  
    13.6  
    13.7 +(*for main ZF????*)
    13.8 +
    13.9  Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
   13.10  by Auto_tac;
   13.11  qed "Collect_disj_eq";
   13.12 @@ -70,3 +72,8 @@
   13.13  Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
   13.14  by Auto_tac;
   13.15  qed "Int_succ_right";
   13.16 +
   13.17 +Goal "cons(a,B) Int A = (if a : A then cons(a, A Int B) else A Int B)";
   13.18 +by Auto_tac;
   13.19 +qed "Int_cons_left";
   13.20 +
    14.1 --- a/src/ZF/UNITY/WFair.ML	Thu Jun 19 18:40:39 2003 +0200
    14.2 +++ b/src/ZF/UNITY/WFair.ML	Fri Jun 20 12:10:45 2003 +0200
    14.3 @@ -19,14 +19,12 @@
    14.4  by Auto_tac;
    14.5  qed "transientD2";
    14.6  
    14.7 -Goalw [stable_def, constrains_def, transient_def]
    14.8 -    "[| F : stable(A); F : transient(A) |] ==> A = 0";
    14.9 -by (Asm_full_simp_tac 1);
   14.10 -by (Blast.depth_tac (claset()) 10 1);
   14.11 +Goal "[| F : stable(A); F : transient(A) |] ==> A = 0";
   14.12 +by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1); 
   14.13 +by (Fast_tac 1); 
   14.14  qed "stable_transient_empty";
   14.15  
   14.16 -Goalw [transient_def, st_set_def] 
   14.17 -"[|F:transient(A); B<=A|] ==> F:transient(B)";
   14.18 +Goalw [transient_def, st_set_def] "[|F:transient(A); B<=A|] ==> F:transient(B)";
   14.19  by Safe_tac;
   14.20  by (res_inst_tac [("x", "act")] bexI 1);
   14.21  by (ALLGOALS(Asm_full_simp_tac));
   14.22 @@ -609,7 +607,6 @@
   14.23  \      F : (A1 - B) co (A1 Un B); \
   14.24  \      F : (A2 - C) co (A2 Un C) |] \
   14.25  \   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
   14.26 -by (Clarify_tac 1);
   14.27  by (Blast_tac 1);
   14.28  qed "leadsTo_123_aux";
   14.29