--- a/src/ZF/UNITY/ClientImpl.ML Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.ML Thu Jun 12 16:40:59 2003 +0200
@@ -8,14 +8,14 @@
Addsimps [type_assumes, default_val_assumes];
(* This part should be automated *)
-Goalw [state_def] "s:state ==> s`ask:list(nat)";
+Goalw [state_def] "s \\<in> state ==> s`ask \\<in> list(nat)";
by (dres_inst_tac [("a", "ask")] apply_type 1);
by Auto_tac;
qed "ask_value_type";
AddTCs [ask_value_type];
Addsimps [ask_value_type];
-Goalw [state_def] "s:state ==> s`giv:list(nat)";
+Goalw [state_def] "s \\<in> state ==> s`giv \\<in> list(nat)";
by (dres_inst_tac [("a", "giv")] apply_type 1);
by Auto_tac;
qed "giv_value_type";
@@ -23,14 +23,14 @@
Addsimps [giv_value_type];
Goalw [state_def]
-"s:state ==> s`rel:list(nat)";
+"s \\<in> state ==> s`rel \\<in> list(nat)";
by (dres_inst_tac [("a", "rel")] apply_type 1);
by Auto_tac;
qed "rel_value_type";
AddTCs [rel_value_type];
Addsimps [rel_value_type];
-Goalw [state_def] "s:state ==> s`tok:nat";
+Goalw [state_def] "s \\<in> state ==> s`tok \\<in> nat";
by (dres_inst_tac [("a", "tok")] apply_type 1);
by Auto_tac;
qed "tok_value_type";
@@ -39,7 +39,7 @@
(** The Client Program **)
-Goalw [client_prog_def] "client_prog:program";
+Goalw [client_prog_def] "client_prog \\<in> program";
by (Simp_tac 1);
qed "client_type";
Addsimps [client_type];
@@ -52,14 +52,14 @@
Addsimps (map simp_of_act [client_rel_act_def,
client_tok_act_def, client_ask_act_def]);
-Goal "ALL G:program. (client_prog ok G) <-> \
-\ (G:preserves(lift(rel)) & G:preserves(lift(ask)) & \
-\ G:preserves(lift(tok)) & client_prog:Allowed(G))";
+Goal "\\<forall>G \\<in> program. (client_prog ok G) <-> \
+\ (G \\<in> preserves(lift(rel)) & G \\<in> preserves(lift(ask)) & \
+\ G \\<in> preserves(lift(tok)) & client_prog \\<in> Allowed(G))";
by (auto_tac (claset(),
simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed]));
qed "client_prog_ok_iff";
-Goal "client_prog:(INT x:var-{ask, rel, tok}. preserves(lift(x)))";
+Goal "client_prog:(\\<Inter>x \\<in> var-{ask, rel, tok}. preserves(lift(x)))";
by (rtac Inter_var_DiffI 1);
by (rtac ballI 2);
by (rtac preservesI 2);
@@ -98,10 +98,10 @@
With no Substitution Axiom, we must prove the two invariants simultaneously. *)
Goal
-"[| client_prog ok G; G:program |]\
+"[| client_prog ok G; G \\<in> program |]\
\ ==> client_prog Join G : \
-\ Always({s:state. s`tok le NbT} Int \
-\ {s:state. ALL elt:set_of_list(s`ask). elt le NbT})";
+\ Always({s \\<in> state. s`tok le NbT} Int \
+\ {s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})";
by (rotate_tac ~1 1);
by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
by (rtac (invariantI RS stable_Join_Always2) 1);
@@ -122,8 +122,8 @@
(* Export version, with no mention of tok in the postcondition, but
unfortunately tok must be declared local.*)
Goal
-"client_prog: program guarantees \
-\ Always({s:state. ALL elt: set_of_list(s`ask). elt le NbT})";
+"client_prog \\<in> program guarantees \
+\ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})";
by (rtac guaranteesI 1);
by (etac (ask_Bounded_lemma RS Always_weaken) 1);
by Auto_tac;
@@ -132,25 +132,25 @@
(*** Towards proving the liveness property ***)
Goal
-"client_prog: stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+"client_prog \\<in> stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
by (constrains_tac 1);
by Auto_tac;
qed "client_prog_stable_rel_le_giv";
Goal
-"[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
-\ ==> client_prog Join G: Stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+"[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
+\ ==> client_prog Join G \\<in> Stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1);
by (auto_tac (claset(), simpset() addsimps [lift_def]));
qed "client_prog_Join_Stable_rel_le_giv";
-Goal "[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
-\ ==> client_prog Join G : Always({s:state. <s`rel, s`giv>:prefix(nat)})";
+Goal "[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
+\ ==> client_prog Join G \\<in> Always({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv],
simpset()) 1);
qed "client_prog_Join_Always_rel_le_giv";
-Goal "xs:list(A) ==> xs@[a]=xs --> False";
+Goal "xs \\<in> list(A) ==> xs@[a]=xs --> False";
by (etac list.induct 1);
by Auto_tac;
qed "list_app_lemma";
@@ -164,8 +164,8 @@
qed "act_subset";
Goal
-"client_prog: \
-\ transient({s:state. s`rel = k & <k, h>:strict_prefix(nat) \
+"client_prog \\<in> \
+\ transient({s \\<in> state. s`rel = k & <k, h>:strict_prefix(nat) \
\ & <h, s`giv>:prefix(nat) & h pfixGe s`ask})";
by (res_inst_tac [("act", "client_rel_act")] transientI 1);
by (simp_tac (simpset() addsimps
@@ -186,7 +186,7 @@
by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
strict_prefix_length_lt]) 1);
by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
-by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(subgoal_tac "h \\<in> list(nat)"));
by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
by (auto_tac (claset(),
simpset() addsimps [prefix_def, Ge_def]));
@@ -203,11 +203,11 @@
qed "strict_prefix_is_prefix";
Goal
-"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] \
-\ ==> client_prog Join G: \
-\ {s:state. s`rel = k & <k,h>:strict_prefix(nat) \
+"[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
+\ ==> client_prog Join G \\<in> \
+\ {s \\<in> state. s`rel = k & <k,h>:strict_prefix(nat) \
\ & <h , s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s:state. <k, s`rel>:strict_prefix(nat) \
+\ LeadsTo {s \\<in> state. <k, s`rel>:strict_prefix(nat) \
\ & <s`rel, s`giv>:prefix(nat) & \
\ <h, s`giv>:prefix(nat) & \
\ h pfixGe s`ask}";
@@ -237,12 +237,12 @@
qed "induct_lemma";
Goal
-"[| client_prog Join G : Incr(lift(giv)); client_prog ok G; G:program |] \
-\ ==> client_prog Join G : \
-\ {s:state. <s`rel, h>:strict_prefix(nat) \
+"[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
+\ ==> client_prog Join G \\<in> \
+\ {s \\<in> state. <s`rel, h>:strict_prefix(nat) \
\ & <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
-by (res_inst_tac [("f", "lam x:state. length(h) #- length(x`rel)")]
+\ LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}";
+by (res_inst_tac [("f", "\\<lambda>x \\<in> state. length(h) #- length(x`rel)")]
LessThan_induct 1);
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
by (rtac single_LeadsTo_I 1);
@@ -258,7 +258,7 @@
by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2);
by (REPEAT (dtac strict_prefix_length_lt 2));
by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2);
-by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(subgoal_tac "h \\<in> list(nat)"));
by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
by (dtac less_imp_succ_add 2);
by (dtac less_imp_succ_add 3);
@@ -272,10 +272,10 @@
qed "rel_progress_lemma";
Goal
-"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] ==> \
-\ client_prog Join G : \
-\ {s:state. <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+"[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] ==> \
+\ client_prog Join G \\<in> \
+\ {s \\<in> state. <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
+\ LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}";
by (rtac (client_prog_Join_Always_rel_le_giv RS Always_LeadsToI) 1);
by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS
LeadsTo_Un RS LeadsTo_weaken_L) 3);
@@ -289,9 +289,9 @@
(*Progress property: all tokens that are given will be released*)
Goal
-"client_prog: Incr(lift(giv)) guarantees \
-\ (INT h:list(nat). {s:state. <h, s`giv>:prefix(nat) &\
-\ h pfixGe s`ask} LeadsTo {s:state. <h, s`rel>:prefix(nat)})";
+"client_prog \\<in> Incr(lift(giv)) guarantees \
+\ (\\<Inter>h \\<in> list(nat). {s \\<in> state. <h, s`giv>:prefix(nat) &\
+\ h pfixGe s`ask} LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (blast_tac (claset() addIs [progress_lemma]) 1);
--- a/src/ZF/UNITY/ClientImpl.thy Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Thu Jun 12 16:40:59 2003 +0200
@@ -36,28 +36,29 @@
client_rel_act ::i
"client_rel_act ==
- {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
- & t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
- nrel < length(s`giv) &
- nth(nrel, s`ask) le nth(nrel, s`giv)}"
+ {<s,t> \\<in> state*state.
+ \\<exists>nrel \\<in> nat. nrel = length(s`rel) &
+ t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
+ nrel < length(s`giv) &
+ nth(nrel, s`ask) le nth(nrel, s`giv)}"
(** Choose a new token requirement **)
- (** Including s'=s suppresses fairness, allowing the non-trivial part
+ (** Including t=s suppresses fairness, allowing the non-trivial part
of the action to be ignored **)
client_tok_act :: i
- "client_tok_act == {<s,t>:state*state. t=s |
- (t = s(tok:=succ(s`tok mod NbT)))}"
+ "client_tok_act == {<s,t> \\<in> state*state. t=s |
+ t = s(tok:=succ(s`tok mod NbT))}"
client_ask_act :: i
- "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+ "client_ask_act == {<s,t> \\<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
client_prog :: i
"client_prog ==
- mk_program({s:state. s`tok le NbT & s`giv = Nil &
+ mk_program({s \\<in> state. s`tok le NbT & s`giv = Nil &
s`ask = Nil & s`rel = Nil},
{client_rel_act, client_tok_act, client_ask_act},
- UN G: preserves(lift(rel)) Int
+ \\<Union>G \\<in> preserves(lift(rel)) Int
preserves(lift(ask)) Int
preserves(lift(tok)). Acts(G))"
end
\ No newline at end of file
--- a/src/ZF/UNITY/Distributor.ML Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Distributor.ML Thu Jun 12 16:40:59 2003 +0200
@@ -16,7 +16,7 @@
Addsimps [var_assumes, default_val_assumes, type_assumes];
Goalw [state_def]
-"s:state ==> s`In:list(A)";
+"s \\<in> state ==> s`In \\<in> list(A)";
by (dres_inst_tac [("a", "In")] apply_type 1);
by Auto_tac;
qed "In_value_type";
@@ -24,7 +24,7 @@
Addsimps [In_value_type];
Goalw [state_def]
-"s:state ==> s`iIn:list(nat)";
+"s \\<in> state ==> s`iIn \\<in> list(nat)";
by (dres_inst_tac [("a", "iIn")] apply_type 1);
by Auto_tac;
qed "iIn_value_type";
@@ -32,7 +32,7 @@
Addsimps [iIn_value_type];
Goalw [state_def]
-"s:state ==> s`Out(n):list(A)";
+"s \\<in> state ==> s`Out(n):list(A)";
by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
by Auto_tac;
qed "Out_value_type";
@@ -41,7 +41,7 @@
val distrib = thm "distr_spec";
-Goal "D:program";
+Goal "D \\<in> program";
by (cut_facts_tac [distrib] 1);
by (auto_tac (claset(), simpset() addsimps
[distr_spec_def, distr_allowed_acts_def]));
@@ -49,9 +49,9 @@
Addsimps [D_in_program];
AddTCs [D_in_program];
-Goal "G:program ==> \
+Goal "G \\<in> program ==> \
\ D ok G <-> \
-\ ((ALL n:nat. G:preserves(lift(Out(n)))) & D:Allowed(G))";
+\ ((\\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n)))) & D \\<in> Allowed(G))";
by (cut_facts_tac [distrib] 1);
by (auto_tac (claset(),
simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def,
@@ -66,9 +66,9 @@
Goal
"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
\ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
-\ Always({s:state. ALL elt:set_of_list(s`iIn). elt<Nclients})) \
+\ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt<Nclients})) \
\ guarantees \
-\ (INT n: Nclients. lift(Out(n)) IncreasingWrt \
+\ (\\<Inter>n \\<in> Nclients. lift(Out(n)) IncreasingWrt \
\ prefix(A)/list(A))";
by (cut_facts_tac [D_in_program, distrib] 1);
by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
@@ -80,17 +80,17 @@
val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
Goal
-"[| ALL n:nat. G:preserves(lift(Out(n))); \
-\ D Join G:Always({s:state. \
-\ ALL elt:set_of_list(s`iIn). elt < Nclients}) |] \
+"[| \\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n))); \
+\ D Join G \\<in> Always({s \\<in> state. \
+\ \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |] \
\ ==> D Join G : Always \
-\ ({s:state. msetsum(%n. bag_of (sublist(s`In, \
-\ {k:nat. k < length(s`iIn) &\
+\ ({s \\<in> state. msetsum(%n. bag_of (sublist(s`In, \
+\ {k \\<in> nat. k < length(s`iIn) &\
\ nth(k, s`iIn)= n})), \
\ Nclients, A) = \
\ bag_of(sublist(s`In, length(s`iIn)))})";
by (cut_facts_tac [D_in_program] 1);
-by (subgoal_tac "G:program" 1);
+by (subgoal_tac "G \\<in> program" 1);
by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
by Auto_tac;
@@ -100,7 +100,7 @@
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1);
by (subgoal_tac
- "(UN i: Nclients. {k:nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
+ "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
\ length(x`iIn)" 1);
by (Asm_simp_tac 1);
by (resolve_tac [equalityI] 1);
@@ -119,9 +119,9 @@
Goal
"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
\ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
-\ Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})) \
+\ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})) \
\ guarantees \
-\ (INT n: Nclients. \
+\ (\\<Inter>n \\<in> Nclients. \
\ (%s. msetsum(%i. bag_of(s`Out(i)), Nclients, A)) \
\ Fols \
\ (%s. bag_of(sublist(s`In, length(s`iIn)))) \
--- a/src/ZF/UNITY/Distributor.thy Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Distributor.thy Thu Jun 12 16:40:59 2003 +0200
@@ -14,19 +14,18 @@
"distr_follows(A, In, iIn, Out) ==
(lift(In) IncreasingWrt prefix(A)/list(A)) Int
(lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
- Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})
+ Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})
guarantees
- (INT n: Nclients.
+ (\\<Inter>n \\<in> Nclients.
lift(Out(n))
Fols
- (%s. sublist(s`In,
- {k:nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
+ (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
Wrt prefix(A)/list(A))"
distr_allowed_acts :: [i=>i]=>i
"distr_allowed_acts(Out) ==
{D:program. AllowedActs(D) =
- cons(id(state), UN G:(INT n:nat. preserves(lift(Out(n)))). Acts(G))}"
+ cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
distr_spec :: [i, i, i, i =>i]=>i
"distr_spec(A, In, iIn, Out) ==
@@ -39,12 +38,12 @@
A :: i (*the type of items being distributed *)
D :: i
assumes
- var_assumes "In:var & iIn:var & (ALL n. Out(n):var)"
- all_distinct_vars "ALL n. all_distinct([In, iIn, iOut(n)])"
+ var_assumes "In:var & iIn:var & (\\<forall>n. Out(n):var)"
+ all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])"
type_assumes "type_of(In)=list(A) & type_of(iIn)=list(nat) &
- (ALL n. type_of(Out(n))=list(A))"
+ (\\<forall>n. type_of(Out(n))=list(A))"
default_val_assumes "default_val(In)=Nil &
default_val(iIn)=Nil &
- (ALL n. default_val(Out(n))=Nil)"
+ (\\<forall>n. default_val(Out(n))=Nil)"
distr_spec "D:distr_spec(A, In, iIn, Out)"
end
--- a/src/ZF/UNITY/Merge.ML Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Merge.ML Thu Jun 12 16:40:59 2003 +0200
@@ -15,7 +15,7 @@
Addsimps [var_assumes, default_val_assumes, type_assumes];
Goalw [state_def]
-"s:state ==> s`In(n):list(A)";
+"s \\<in> state ==> s`In(n):list(A)";
by (dres_inst_tac [("a", "In(n)")] apply_type 1);
by Auto_tac;
qed "In_value_type";
@@ -23,7 +23,7 @@
Addsimps [In_value_type];
Goalw [state_def]
-"s:state ==> s`Out:list(A)";
+"s \\<in> state ==> s`Out \\<in> list(A)";
by (dres_inst_tac [("a", "Out")] apply_type 1);
by Auto_tac;
qed "Out_value_type";
@@ -31,7 +31,7 @@
Addsimps [Out_value_type];
Goalw [state_def]
-"s:state ==> s`iOut:list(nat)";
+"s \\<in> state ==> s`iOut \\<in> list(nat)";
by (dres_inst_tac [("a", "iOut")] apply_type 1);
by Auto_tac;
qed "Out_value_type";
@@ -41,7 +41,7 @@
val merge = thm "merge_spec";
-Goal "M:program";
+Goal "M \\<in> program";
by (cut_facts_tac [merge] 1);
by (auto_tac (claset() addDs [guarantees_type RS subsetD],
simpset() addsimps [merge_spec_def, merge_increasing_def]));
@@ -58,20 +58,20 @@
qed "merge_Allowed";
Goal
-"G:program ==> \
-\ M ok G <-> (G:preserves(lift(Out)) & \
-\ G:preserves(lift(iOut)) & M:Allowed(G))";
+"G \\<in> program ==> \
+\ M ok G <-> (G \\<in> preserves(lift(Out)) & \
+\ G \\<in> preserves(lift(iOut)) & M \\<in> Allowed(G))";
by (cut_facts_tac [merge] 1);
by (auto_tac (claset(), simpset()
addsimps [merge_Allowed, ok_iff_Allowed]));
qed "M_ok_iff";
Goal
-"[| G:preserves(lift(Out)); G:preserves(lift(iOut)); \
-\ M:Allowed(G) |] ==> \
-\ M Join G:Always({s:state. length(s`Out)=length(s`iOut)})";
+"[| G \\<in> preserves(lift(Out)); G \\<in> preserves(lift(iOut)); \
+\ M \\<in> Allowed(G) |] ==> \
+\ M Join G \\<in> Always({s \\<in> state. length(s`Out)=length(s`iOut)})";
by (ftac (preserves_type RS subsetD) 1);
-by (subgoal_tac "G:program" 1);
+by (subgoal_tac "G \\<in> program" 1);
by (assume_tac 2);
by (ftac M_ok_iff 1);
by (cut_facts_tac [merge] 1);
@@ -80,9 +80,9 @@
qed "merge_Always_Out_eq_iOut";
Goal
-"[| G:preserves(lift(iOut)); G:preserves(lift(Out)); \
-\ M:Allowed(G) |] ==> \
-\ M Join G: Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})";
+"[| G \\<in> preserves(lift(iOut)); G \\<in> preserves(lift(Out)); \
+\ M \\<in> Allowed(G) |] ==> \
+\ M Join G: Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})";
by (ftac (preserves_type RS subsetD) 1);
by (ftac M_ok_iff 1);
by (cut_facts_tac [merge] 1);
@@ -91,11 +91,11 @@
qed "merge_Bounded";
Goal
-"[| G:preserves(lift(iOut)); \
-\ G: preserves(lift(Out)); M:Allowed(G) |] \
+"[| G \\<in> preserves(lift(iOut)); \
+\ G: preserves(lift(Out)); M \\<in> Allowed(G) |] \
\ ==> M Join G : Always \
-\ ({s:state. msetsum(%i. bag_of(sublist(s`Out, \
-\ {k:nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
+\ ({s \\<in> state. msetsum(%i. bag_of(sublist(s`Out, \
+\ {k \\<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
\ Nclients, A) = bag_of(s`Out)})";
by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
@@ -105,7 +105,7 @@
by (auto_tac (claset(), simpset()
addsimps [nat_into_Finite, set_of_list_conv_nth]));
by (subgoal_tac
- "(UN i:Nclients. {k:nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
+ "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
by Auto_tac;
by (resolve_tac [equalityI] 1);
by (blast_tac (claset() addDs [ltD]) 1);
@@ -121,7 +121,7 @@
qed "merge_bag_Follows_lemma";
Goal
-"M : (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
+"M : (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
\ guarantees \
\ (%s. bag_of(s`Out)) Fols \
\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
--- a/src/ZF/UNITY/Merge.thy Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy Thu Jun 12 16:40:59 2003 +0200
@@ -20,40 +20,40 @@
(*spec (11)*)
merge_eq_Out :: [i, i] =>i
"merge_eq_Out(Out, iOut) == program guarantees
- Always({s:state. length(s`Out) = length(s`iOut)})"
+ Always({s \\<in> state. length(s`Out) = length(s`iOut)})"
(*spec (12)*)
merge_bounded :: i=>i
"merge_bounded(iOut) == program guarantees
- Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})"
+ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})"
(*spec (13)*)
(* Parameter A represents the type of tokens *)
merge_follows :: [i, i=>i, i, i] =>i
"merge_follows(A, In, Out, iOut) ==
- (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+ (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
guarantees
- (INT n:Nclients.
- (%s. sublist(s`Out, {k:nat. k < length(s`iOut) &
+ (\\<Inter>n \\<in> Nclients.
+ (%s. sublist(s`Out, {k \\<in> nat. k < length(s`iOut) &
nth(k, s`iOut) = n})) Fols lift(In(n))
Wrt prefix(A)/list(A))"
(*spec: preserves part*)
merge_preserves :: [i=>i] =>i
- "merge_preserves(In) == INT n:nat. preserves(lift(In(n)))"
+ "merge_preserves(In) == \\<Inter>n \\<in> nat. preserves(lift(In(n)))"
(* environmental constraints*)
merge_allowed_acts :: [i, i] =>i
"merge_allowed_acts(Out, iOut) ==
- {F:program. AllowedActs(F) =
- cons(id(state), (UN G:preserves(lift(Out)) Int
- preserves(lift(iOut)). Acts(G)))}"
+ {F \\<in> program. AllowedActs(F) =
+ cons(id(state), (\\<Union>G \\<in> preserves(lift(Out)) \\<inter>
+ preserves(lift(iOut)). Acts(G)))}"
merge_spec :: [i, i =>i, i, i]=>i
"merge_spec(A, In, Out, iOut) ==
- merge_increasing(A, Out, iOut) Int merge_eq_Out(Out, iOut) Int
- merge_bounded(iOut) Int merge_follows(A, In, Out, iOut)
- Int merge_allowed_acts(Out, iOut) Int merge_preserves(In)"
+ merge_increasing(A, Out, iOut) \\<inter> merge_eq_Out(Out, iOut) \\<inter>
+ merge_bounded(iOut) \\<inter> merge_follows(A, In, Out, iOut)
+ \\<inter> merge_allowed_acts(Out, iOut) \\<inter> merge_preserves(In)"
(** State definitions. OUTPUT variables are locals **)
locale Merge =
@@ -63,16 +63,16 @@
A :: i (*the type of items being merged *)
M :: i
assumes
- var_assumes "(ALL n. In(n):var) & Out:var & iOut:var"
- all_distinct_vars "ALL n. all_distinct([In(n), Out, iOut])"
- type_assumes "(ALL n. type_of(In(n))=list(A))&
+ var_assumes "(\\<forall>n. In(n):var) & Out \\<in> var & iOut \\<in> var"
+ all_distinct_vars "\\<forall>n. all_distinct([In(n), Out, iOut])"
+ type_assumes "(\\<forall>n. type_of(In(n))=list(A))&
type_of(Out)=list(A) &
type_of(iOut)=list(nat)"
- default_val_assumes "(ALL n. default_val(In(n))=Nil) &
+ default_val_assumes "(\\<forall>n. default_val(In(n))=Nil) &
default_val(Out)=Nil &
default_val(iOut)=Nil"
- merge_spec "M:merge_spec(A, In, Out, iOut)"
+ merge_spec "M \\<in> merge_spec(A, In, Out, iOut)"
end
\ No newline at end of file