--- a/src/ZF/Bool.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Bool.thy Sun Oct 07 15:49:25 2007 +0200
@@ -9,13 +9,13 @@
theory Bool imports pair begin
-syntax
- "1" :: i ("1")
- "2" :: i ("2")
+abbreviation
+ one ("1") where
+ "1 == succ(0)"
-translations
- "1" == "succ(0)"
- "2" == "succ(1)"
+abbreviation
+ two ("2") where
+ "2 == succ(1)"
text{*2 is equal to bool, but is used as a number rather than a type.*}
@@ -60,7 +60,7 @@
lemma boolE:
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"
-by (simp add: bool_defs, blast)
+by (simp add: bool_defs, blast)
(** cond **)
@@ -134,7 +134,7 @@
lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)"
by (elim boolE, auto)
-lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
+lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
(a or b) and c = (a and c) or (b and c)"
by (elim boolE, auto)
@@ -149,7 +149,7 @@
lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)"
by (elim boolE, auto)
-lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
+lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
(a and b) or c = (a or c) and (b or c)"
by (elim boolE, auto)
@@ -158,19 +158,19 @@
"bool_of_o(P) == (if P then 1 else 0)"
lemma [simp]: "bool_of_o(True) = 1"
-by (simp add: bool_of_o_def)
+by (simp add: bool_of_o_def)
lemma [simp]: "bool_of_o(False) = 0"
-by (simp add: bool_of_o_def)
+by (simp add: bool_of_o_def)
lemma [simp,TC]: "bool_of_o(P) \<in> bool"
-by (simp add: bool_of_o_def)
+by (simp add: bool_of_o_def)
lemma [simp]: "(bool_of_o(P) = 1) <-> P"
-by (simp add: bool_of_o_def)
+by (simp add: bool_of_o_def)
lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
-by (simp add: bool_of_o_def)
+by (simp add: bool_of_o_def)
ML
{*
--- a/src/ZF/EquivClass.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/EquivClass.thy Sun Oct 07 15:49:25 2007 +0200
@@ -21,14 +21,15 @@
"congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
<y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
-syntax
- RESPECTS ::"[i=>i, i] => o" (infixr "respects" 80)
- RESPECTS2 ::"[i=>i, i] => o" (infixr "respects2 " 80)
+abbreviation
+ RESPECTS ::"[i=>i, i] => o" (infixr "respects" 80) where
+ "f respects r == congruent(r,f)"
+
+abbreviation
+ RESPECTS2 ::"[i=>i=>i, i] => o" (infixr "respects2 " 80) where
+ "f respects2 r == congruent2(r,r,f)"
--{*Abbreviation for the common case where the relations are identical*}
-translations
- "f respects r" == "congruent(r,f)"
- "f respects2 r" => "congruent2(r,r,f)"
subsection{*Suppes, Theorem 70:
@{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
--- a/src/ZF/Induct/Multiset.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Induct/Multiset.thy Sun Oct 07 15:49:25 2007 +0200
@@ -12,11 +12,10 @@
imports FoldSet Acc
begin
-consts
- (* Short cut for multiset space *)
- Mult :: "i=>i"
-translations
- "Mult(A)" => "A -||> nat-{0}"
+abbreviation (input)
+ -- {* Short cut for multiset space *}
+ Mult :: "i=>i" where
+ "Mult(A) == A -||> nat-{0}"
constdefs
@@ -64,15 +63,15 @@
msize :: "i => i"
"msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
+abbreviation
+ melem :: "[i,i] => o" ("(_/ :# _)" [50, 51] 50) where
+ "a :# M == a \<in> mset_of(M)"
+
syntax
- melem :: "[i,i] => o" ("(_/ :# _)" [50, 51] 50)
"@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
-
syntax (xsymbols)
"@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
-
translations
- "a :# M" == "a \<in> mset_of(M)"
"{#x \<in> M. P#}" == "MCollect(M, %x. P)"
(* multiset orderings *)
--- a/src/ZF/Induct/Primrec.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Induct/Primrec.thy Sun Oct 07 15:49:25 2007 +0200
@@ -42,10 +42,9 @@
"ACK(0) = SC"
"ACK(succ(i)) = PREC (CONSTANT (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
-syntax
- ack :: "[i,i]=>i"
-translations
- "ack(x,y)" == "ACK(x) ` [y]"
+abbreviation
+ ack :: "[i,i]=>i" where
+ "ack(x,y) == ACK(x) ` [y]"
text {*
--- a/src/ZF/Resid/Reduction.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Resid/Reduction.thy Sun Oct 07 15:49:25 2007 +0200
@@ -12,10 +12,10 @@
consts
lambda :: "i"
unmark :: "i=>i"
- Apl :: "[i,i]=>i"
-translations
- "Apl(n,m)" == "App(0,n,m)"
+abbreviation
+ Apl :: "[i,i]=>i" where
+ "Apl(n,m) == App(0,n,m)"
inductive
domains "lambda" <= redexes
--- a/src/ZF/Resid/Substitution.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Resid/Substitution.thy Sun Oct 07 15:49:25 2007 +0200
@@ -7,27 +7,11 @@
theory Substitution imports Redex begin
-consts
- lift_aux :: "i=>i"
- lift :: "i=>i"
- subst_aux :: "i=>i"
- subst :: "[i,i]=>i" (infixl "'/" 70)
-
-constdefs
- lift_rec :: "[i,i]=> i"
- "lift_rec(r,k) == lift_aux(r)`k"
-
- subst_rec :: "[i,i,i]=> i" (**NOTE THE ARGUMENT ORDER BELOW**)
- "subst_rec(u,r,k) == subst_aux(r)`u`k"
-
-translations
- "lift(r)" == "lift_rec(r,0)"
- "u/v" == "subst_rec(u,v,0)"
-
-
(** The clumsy _aux functions are required because other arguments vary
in the recursive calls ***)
+consts
+ lift_aux :: "i=>i"
primrec
"lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
@@ -35,18 +19,36 @@
"lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+constdefs
+ lift_rec :: "[i,i]=> i"
+ "lift_rec(r,k) == lift_aux(r)`k"
-
+abbreviation
+ lift :: "i=>i" where
+ "lift(r) == lift_rec(r,0)"
+
+
+consts
+ subst_aux :: "i=>i"
primrec
"subst_aux(Var(i)) =
- (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
+ (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
else if k=i then r else Var(i))"
"subst_aux(Fun(t)) =
(\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
- "subst_aux(App(b,f,a)) =
+ "subst_aux(App(b,f,a)) =
(\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+constdefs
+ subst_rec :: "[i,i,i]=> i" (**NOTE THE ARGUMENT ORDER BELOW**)
+ "subst_rec(u,r,k) == subst_aux(r)`u`k"
+
+abbreviation
+ subst :: "[i,i]=>i" (infixl "'/" 70) where
+ "u/v == subst_rec(u,v,0)"
+
+
(* ------------------------------------------------------------------------- *)
(* Arithmetic extensions *)
@@ -100,8 +102,8 @@
(* ------------------------------------------------------------------------- *)
lemma subst_Var:
- "[|k \<in> nat; u \<in> redexes|]
- ==> subst_rec(u,Var(i),k) =
+ "[|k \<in> nat; u \<in> redexes|]
+ ==> subst_rec(u,Var(i),k) =
(if k<i then Var(i #- 1) else if k=i then u else Var(i))"
by (simp add: subst_rec_def gt_not_eq leI)
@@ -148,8 +150,8 @@
(*The i\<in>nat is redundant*)
lemma lift_lift_rec [rule_format]:
- "u \<in> redexes
- ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
+ "u \<in> redexes
+ ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
(lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
apply (erule redexes.induct, auto)
apply (case_tac "n < i")
@@ -158,7 +160,7 @@
done
lemma lift_lift:
- "[|u \<in> redexes; n \<in> nat|]
+ "[|u \<in> redexes; n \<in> nat|]
==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
by (simp add: lift_lift_rec)
@@ -166,13 +168,13 @@
by (erule natE, auto)
lemma lift_rec_subst_rec [rule_format]:
- "v \<in> redexes ==>
- \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
- lift_rec(subst_rec(u,v,n),m) =
+ "v \<in> redexes ==>
+ \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
+ lift_rec(subst_rec(u,v,n),m) =
subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
apply safe
-apply (rename_tac n n' m u)
+apply (rename_tac n n' m u)
apply (case_tac "n < n'")
apply (frule_tac j = n' in lt_trans2, assumption)
apply (simp add: leI, simp)
@@ -182,19 +184,19 @@
lemma lift_subst:
- "[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
+ "[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
by (simp add: lift_rec_subst_rec)
lemma lift_rec_subst_rec_lt [rule_format]:
- "v \<in> redexes ==>
- \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
- lift_rec(subst_rec(u,v,n),m) =
+ "v \<in> redexes ==>
+ \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
+ lift_rec(subst_rec(u,v,n),m) =
subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
apply safe
-apply (rename_tac n n' m u)
+apply (rename_tac n n' m u)
apply (case_tac "n < n'")
apply (case_tac "n < m")
apply (simp_all add: leI)
@@ -205,20 +207,20 @@
lemma subst_rec_lift_rec [rule_format]:
- "u \<in> redexes ==>
+ "u \<in> redexes ==>
\<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
apply (erule redexes.induct, auto)
apply (case_tac "n < na", auto)
done
lemma subst_rec_subst_rec [rule_format]:
- "v \<in> redexes ==>
- \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
- subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
+ "v \<in> redexes ==>
+ \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
+ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
subst_rec(w,subst_rec(u,v,m),n)"
apply (erule redexes.induct)
apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe)
-apply (rename_tac n' u w)
+apply (rename_tac n' u w)
apply (case_tac "n \<le> succ(n') ")
apply (erule_tac i = n in leE)
apply (simp_all add: succ_pred subst_rec_lift_rec leI)
@@ -231,7 +233,7 @@
apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption)
apply (erule leE)
apply (frule succ_leI [THEN lt_trans], assumption)
- apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans],
+ apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans],
assumption)
apply (simp_all add: succ_pred lt_pred)
done
@@ -254,9 +256,9 @@
by (erule Scomp.induct, simp_all add: comp_refl)
lemma subst_rec_preserve_comp [rule_format, simp]:
- "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
+ "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
-by (erule Scomp.induct,
+by (erule Scomp.induct,
simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
lemma lift_rec_preserve_reg [simp]:
@@ -264,7 +266,7 @@
by (erule Sreg.induct, simp_all add: lift_rec_Var)
lemma subst_rec_preserve_reg [simp]:
- "regular(v) ==>
+ "regular(v) ==>
\<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
--- a/src/ZF/UNITY/AllocBase.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/AllocBase.thy Sun Oct 07 15:49:25 2007 +0200
@@ -10,11 +10,13 @@
theory AllocBase imports Follows MultisetSum Guar begin
consts
- tokbag :: i (* tokbags could be multisets...or any ordered type?*)
NbT :: i (* Number of tokens in system *)
Nclients :: i (* Number of clients *)
-translations "tokbag" => "nat"
+abbreviation (input)
+ tokbag :: i (* tokbags could be multisets...or any ordered type?*)
+where
+ "tokbag == nat"
axioms
NbT_pos: "NbT \<in> nat-{0}"
--- a/src/ZF/UNITY/AllocImpl.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Sun Oct 07 15:49:25 2007 +0200
@@ -9,14 +9,13 @@
theory AllocImpl imports ClientImpl begin
-consts
+abbreviation
+ NbR :: i (*number of consumed messages*) where
+ "NbR == Var([succ(2)])"
- NbR :: i (*number of consumed messages*)
- available_tok :: i (*number of free tokens (T in paper)*)
-
-translations
- "NbR" == "Var([succ(2)])"
- "available_tok" == "Var([succ(succ(2))])"
+abbreviation
+ available_tok :: i (*number of free tokens (T in paper)*) where
+ "available_tok == Var([succ(succ(2))])"
axioms
alloc_type_assumes [simp]:
--- a/src/ZF/UNITY/ClientImpl.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Sun Oct 07 15:49:25 2007 +0200
@@ -6,20 +6,12 @@
Distributed Resource Management System: Client Implementation
*)
-
theory ClientImpl imports AllocBase Guar begin
-consts
- ask :: i (* input history: tokens requested *)
- giv :: i (* output history: tokens granted *)
- rel :: i (* input history: tokens released *)
- tok :: i (* the number of available tokens *)
-
-translations
- "ask" == "Var(Nil)"
- "giv" == "Var([0])"
- "rel" == "Var([1])"
- "tok" == "Var([2])"
+abbreviation "ask == Var(Nil)" (* input history: tokens requested *)
+abbreviation "giv == Var([0])" (* output history: tokens granted *)
+abbreviation "rel == Var([1])" (* input history: tokens released *)
+abbreviation "tok == Var([2])" (* the number of available tokens *)
axioms
type_assumes:
--- a/src/ZF/UNITY/Follows.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Follows.thy Sun Oct 07 15:49:25 2007 +0200
@@ -12,60 +12,64 @@
constdefs
Follows :: "[i, i, i=>i, i=>i] => i"
- "Follows(A, r, f, g) ==
+ "Follows(A, r, f, g) ==
Increasing(A, r, g) Int
Increasing(A, r,f) Int
Always({s \<in> state. <f(s), g(s)>:r}) Int
(\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})"
-consts
- Incr :: "[i=>i]=>i"
- n_Incr :: "[i=>i]=>i"
- m_Incr :: "[i=>i]=>i"
- s_Incr :: "[i=>i]=>i"
- n_Fols :: "[i=>i, i=>i]=>i" (infixl "n'_Fols" 65)
+
+abbreviation
+ Incr :: "[i=>i]=>i" where
+ "Incr(f) == Increasing(list(nat), prefix(nat), f)"
-syntax
- Follows' :: "[i=>i, i=>i, i, i] => i"
- ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)
+abbreviation
+ n_Incr :: "[i=>i]=>i" where
+ "n_Incr(f) == Increasing(nat, Le, f)"
+
+abbreviation
+ s_Incr :: "[i=>i]=>i" where
+ "s_Incr(f) == Increasing(Pow(nat), SetLe(nat), f)"
-
-translations
- "Incr(f)" == "Increasing(list(nat), prefix(nat), f)"
- "n_Incr(f)" == "Increasing(nat, Le, f)"
- "s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"
- "m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"
-
- "f n_Fols g" == "Follows(nat, Le, f, g)"
+abbreviation
+ m_Incr :: "[i=>i]=>i" where
+ "m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)"
- "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
+abbreviation
+ n_Fols :: "[i=>i, i=>i]=>i" (infixl "n'_Fols" 65) where
+ "f n_Fols g == Follows(nat, Le, f, g)"
+
+abbreviation
+ Follows' :: "[i=>i, i=>i, i, i] => i"
+ ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60) where
+ "f Fols g Wrt r/A == Follows(A,r,f,g)"
(*Does this hold for "invariant"?*)
-lemma Follows_cong:
+lemma Follows_cong:
"[|A=A'; r=r'; !!x. x \<in> state ==> f(x)=f'(x); !!x. x \<in> state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')"
by (simp add: Increasing_def Follows_def)
-lemma subset_Always_comp:
-"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
+lemma subset_Always_comp:
+"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
apply (unfold mono1_def metacomp_def)
apply (auto simp add: Always_eq_includes_reachable)
done
-lemma imp_Always_comp:
-"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});
- mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
+lemma imp_Always_comp:
+"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});
+ mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
by (blast intro: subset_Always_comp [THEN subsetD])
-lemma imp_Always_comp2:
-"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});
- F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});
- mono2(A, r, B, s, C, t, h);
- \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]
+lemma imp_Always_comp2:
+"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});
+ F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});
+ mono2(A, r, B, s, C, t, h);
+ \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]
==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})"
apply (auto simp add: Always_eq_includes_reachable mono2_def)
apply (auto dest!: subsetD)
@@ -73,10 +77,10 @@
(* comp LeadsTo *)
-lemma subset_LeadsTo_comp:
-"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s);
- \<forall>x \<in> state. f(x):A & g(x):A |] ==>
- (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <=
+lemma subset_LeadsTo_comp:
+"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s);
+ \<forall>x \<in> state. f(x):A & g(x):A |] ==>
+ (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <=
(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
apply (unfold mono1_def metacomp_def, clarify)
@@ -93,19 +97,19 @@
apply auto
done
-lemma imp_LeadsTo_comp:
-"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r});
- mono1(A, r, B, s, h); refl(A,r); trans[B](s);
- \<forall>x \<in> state. f(x):A & g(x):A |] ==>
+lemma imp_LeadsTo_comp:
+"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r});
+ mono1(A, r, B, s, h); refl(A,r); trans[B](s);
+ \<forall>x \<in> state. f(x):A & g(x):A |] ==>
F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
apply (rule subset_LeadsTo_comp [THEN subsetD], auto)
done
-lemma imp_LeadsTo_comp_right:
-"[| F \<in> Increasing(B, s, g);
- \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
- mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
- \<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C |] ==>
+lemma imp_LeadsTo_comp_right:
+"[| F \<in> Increasing(B, s, g);
+ \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
+ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
+ \<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C |] ==>
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
@@ -124,11 +128,11 @@
apply (auto simp add: part_order_def)
done
-lemma imp_LeadsTo_comp_left:
-"[| F \<in> Increasing(A, r, f);
- \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
- mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
- \<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C |] ==>
+lemma imp_LeadsTo_comp_left:
+"[| F \<in> Increasing(A, r, f);
+ \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
+ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
+ \<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C |] ==>
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
@@ -148,12 +152,12 @@
done
(** This general result is used to prove Follows Un, munion, etc. **)
-lemma imp_LeadsTo_comp2:
-"[| F \<in> Increasing(A, r, f1) Int Increasing(B, s, g);
- \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
- \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
- mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
- \<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C |]
+lemma imp_LeadsTo_comp2:
+"[| F \<in> Increasing(A, r, f1) Int Increasing(B, s, g);
+ \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
+ \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
+ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
+ \<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C |]
==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}"
apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans)
apply (blast intro: imp_LeadsTo_comp_right)
@@ -169,21 +173,21 @@
lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program"
by (blast dest: Follows_type [THEN subsetD])
-lemma FollowsD:
-"F \<in> Follows(A, r, f, g)==>
+lemma FollowsD:
+"F \<in> Follows(A, r, f, g)==>
F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)"
apply (unfold Follows_def)
apply (blast dest: IncreasingD)
done
-lemma Follows_constantI:
+lemma Follows_constantI:
"[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)"
apply (unfold Follows_def, auto)
apply (auto simp add: refl_def)
done
-lemma subset_Follows_comp:
-"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
+lemma subset_Follows_comp:
+"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
==> Follows(A, r, f, g) <= Follows(B, s, h comp f, h comp g)"
apply (unfold Follows_def, clarify)
apply (frule_tac f = g in IncreasingD)
@@ -194,19 +198,19 @@
apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps)
done
-lemma imp_Follows_comp:
-"[| F \<in> Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
+lemma imp_Follows_comp:
+"[| F \<in> Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
==> F \<in> Follows(B, s, h comp f, h comp g)"
apply (blast intro: subset_Follows_comp [THEN subsetD])
done
(* 2-place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *)
-(* 2-place monotone operation \<in> this general result is
+(* 2-place monotone operation \<in> this general result is
used to prove Follows_Un, Follows_munion *)
-lemma imp_Follows_comp2:
-"[| F \<in> Follows(A, r, f1, f); F \<in> Follows(B, s, g1, g);
- mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]
+lemma imp_Follows_comp2:
+"[| F \<in> Follows(A, r, f1, f); F \<in> Follows(B, s, g1, g);
+ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]
==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"
apply (unfold Follows_def, clarify)
apply (frule_tac f = g in IncreasingD)
@@ -223,13 +227,13 @@
apply (rule_tac h = h in imp_LeadsTo_comp2)
prefer 4 apply assumption
apply auto
- prefer 3 apply (simp add: mono2_def)
+ prefer 3 apply (simp add: mono2_def)
apply (blast dest: IncreasingD)+
done
lemma Follows_trans:
- "[| F \<in> Follows(A, r, f, g); F \<in> Follows(A,r, g, h);
+ "[| F \<in> Follows(A, r, f, g); F \<in> Follows(A,r, g, h);
trans[A](r) |] ==> F \<in> Follows(A, r, f, h)"
apply (frule_tac f = f in FollowsD)
apply (frule_tac f = g in FollowsD)
@@ -242,64 +246,64 @@
(** Destruction rules for Follows **)
-lemma Follows_imp_Increasing_left:
+lemma Follows_imp_Increasing_left:
"F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)"
by (unfold Follows_def, blast)
-lemma Follows_imp_Increasing_right:
+lemma Follows_imp_Increasing_right:
"F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)"
by (unfold Follows_def, blast)
-lemma Follows_imp_Always:
+lemma Follows_imp_Always:
"F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})"
by (unfold Follows_def, blast)
-lemma Follows_imp_LeadsTo:
- "[| F \<in> Follows(A, r, f, g); k \<in> A |] ==>
+lemma Follows_imp_LeadsTo:
+ "[| F \<in> Follows(A, r, f, g); k \<in> A |] ==>
F: {s \<in> state. <k,g(s)> \<in> r } LeadsTo {s \<in> state. <k,f(s)> \<in> r}"
by (unfold Follows_def, blast)
lemma Follows_LeadsTo_pfixLe:
- "[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |]
+ "[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |]
==> F \<in> {s \<in> state. k pfixLe g(s)} LeadsTo {s \<in> state. k pfixLe f(s)}"
by (blast intro: Follows_imp_LeadsTo)
lemma Follows_LeadsTo_pfixGe:
- "[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |]
+ "[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |]
==> F \<in> {s \<in> state. k pfixGe g(s)} LeadsTo {s \<in> state. k pfixGe f(s)}"
by (blast intro: Follows_imp_LeadsTo)
-lemma Always_Follows1:
-"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
+lemma Always_Follows1:
+"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
\<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)"
apply (unfold Follows_def Increasing_def Stable_def)
apply (simp add: INT_iff, auto)
-apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
- and A = "{s \<in> state. <k, h (s)> \<in> r}"
+apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
+ and A = "{s \<in> state. <k, h (s)> \<in> r}"
and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken)
-apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}"
+apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}"
and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken)
apply auto
apply (drule Always_Int_I, assumption)
-apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}"
+apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}"
in Always_weaken)
apply auto
done
-lemma Always_Follows2:
-"[| F \<in> Always({s \<in> state. g(s) = h(s)});
+lemma Always_Follows2:
+"[| F \<in> Always({s \<in> state. g(s) = h(s)});
F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A |] ==> F \<in> Follows(A, r, f, h)"
apply (unfold Follows_def Increasing_def Stable_def)
apply (simp add: INT_iff, auto)
-apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
- and A = "{s \<in> state. <k, g (s) > \<in> r}"
+apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
+ and A = "{s \<in> state. <k, g (s) > \<in> r}"
and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken)
-apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}"
+apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}"
and A' = "{s \<in> state. <k, g(s)> \<in> r}" in Always_Constrains_weaken)
apply auto
apply (drule Always_Int_I, assumption)
-apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}"
+apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}"
in Always_weaken)
apply auto
done
@@ -319,26 +323,26 @@
by (unfold part_order_def, auto)
lemma increasing_Un:
- "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);
- F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]
+ "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);
+ F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]
==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
by (rule_tac h = "op Un" in imp_increasing_comp2, auto)
lemma Increasing_Un:
- "[| F \<in> Increasing(Pow(A), SetLe(A), f);
- F \<in> Increasing(Pow(A), SetLe(A), g) |]
+ "[| F \<in> Increasing(Pow(A), SetLe(A), f);
+ F \<in> Increasing(Pow(A), SetLe(A), g) |]
==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
by (rule_tac h = "op Un" in imp_Increasing_comp2, auto)
lemma Always_Un:
- "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});
- F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]
+ "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});
+ F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]
==> F \<in> Always({s \<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})"
by (simp add: Always_eq_includes_reachable, blast)
-lemma Follows_Un:
-"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);
- F \<in> Follows(Pow(A), SetLe(A), g1, g) |]
+lemma Follows_Un:
+"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);
+ F \<in> Follows(Pow(A), SetLe(A), g1, g) |]
==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"
by (rule_tac h = "op Un" in imp_Follows_comp2, auto)
@@ -347,7 +351,7 @@
lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))"
by (unfold MultLe_def refl_def, auto)
-lemma MultLe_refl1 [simp]:
+lemma MultLe_refl1 [simp]:
"[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)"
apply (unfold MultLe_def id_def lam_def)
apply (auto simp add: Mult_iff_multiset)
@@ -374,7 +378,7 @@
apply (auto dest: MultLe_type [THEN subsetD])
done
-lemma part_order_imp_part_ord:
+lemma part_order_imp_part_ord:
"part_order(A, r) ==> part_ord(A, r-id(A))"
apply (unfold part_order_def part_ord_def)
apply (simp add: refl_def id_def lam_def irrefl_def, auto)
@@ -385,7 +389,7 @@
apply auto
done
-lemma antisym_MultLe [simp]:
+lemma antisym_MultLe [simp]:
"part_order(A, r) ==> antisym(MultLe(A,r))"
apply (unfold MultLe_def antisym_def)
apply (drule part_order_imp_part_ord, auto)
@@ -401,7 +405,7 @@
apply (auto simp add: part_order_def)
done
-lemma empty_le_MultLe [simp]:
+lemma empty_le_MultLe [simp]:
"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)"
apply (unfold MultLe_def)
apply (case_tac "M=0")
@@ -414,8 +418,8 @@
lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)"
by (simp add: Mult_iff_multiset)
-lemma munion_mono:
-"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==>
+lemma munion_mono:
+"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==>
<M +# K, N +# L> \<in> MultLe(A, r)"
apply (unfold MultLe_def)
apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
@@ -423,41 +427,41 @@
done
lemma increasing_munion:
- "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);
- F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]
+ "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);
+ F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]
==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
by (rule_tac h = munion in imp_increasing_comp2, auto)
lemma Increasing_munion:
- "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);
- F \<in> Increasing(Mult(A), MultLe(A,r), g)|]
+ "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);
+ F \<in> Increasing(Mult(A), MultLe(A,r), g)|]
==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
by (rule_tac h = munion in imp_Increasing_comp2, auto)
-lemma Always_munion:
-"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});
- F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)});
- \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]
+lemma Always_munion:
+"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});
+ F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)});
+ \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]
==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})"
apply (rule_tac h = munion in imp_Always_comp2, simp_all)
apply (blast intro: munion_mono, simp_all)
done
-lemma Follows_munion:
-"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);
- F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]
+lemma Follows_munion:
+"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);
+ F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]
==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"
by (rule_tac h = munion in imp_Follows_comp2, auto)
(** Used in ClientImp **)
-lemma Follows_msetsum_UN:
-"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));
- \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &
- multiset(f(i, s)) & mset_of(f(i, s))<=A ;
- Finite(I); F \<in> program |]
- ==> F \<in> Follows(Mult(A),
- MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),
+lemma Follows_msetsum_UN:
+"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));
+ \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &
+ multiset(f(i, s)) & mset_of(f(i, s))<=A ;
+ Finite(I); F \<in> program |]
+ ==> F \<in> Follows(Mult(A),
+ MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),
%x. msetsum(%i. f(i, x), I, A))"
apply (erule rev_mp)
apply (drule Finite_into_Fin)
--- a/src/ZF/UNITY/GenPrefix.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy Sun Oct 07 15:49:25 2007 +0200
@@ -12,8 +12,7 @@
header{*Charpentier's Generalized Prefix Relation*}
theory GenPrefix
-imports Main
-
+imports Main
begin
constdefs (*really belongs in ZF/Trancl*)
@@ -22,12 +21,12 @@
consts
gen_prefix :: "[i, i] => i"
-
+
inductive
(* Parameter A is the domain of zs's elements *)
-
+
domains "gen_prefix(A, r)" <= "list(A)*list(A)"
-
+
intros
Nil: "<[],[]>:gen_prefix(A, r)"
@@ -45,17 +44,19 @@
strict_prefix :: "i=>i"
"strict_prefix(A) == prefix(A) - id(list(A))"
-syntax
- (* less or equal and greater or equal over prefixes *)
- pfixLe :: "[i, i] => o" (infixl "pfixLe" 50)
- pfixGe :: "[i, i] => o" (infixl "pfixGe" 50)
+
+(* less or equal and greater or equal over prefixes *)
+
+abbreviation
+ pfixLe :: "[i, i] => o" (infixl "pfixLe" 50) where
+ "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
-translations
- "xs pfixLe ys" == "<xs, ys>:gen_prefix(nat, Le)"
- "xs pfixGe ys" == "<xs, ys>:gen_prefix(nat, Ge)"
-
+abbreviation
+ pfixGe :: "[i, i] => o" (infixl "pfixGe" 50) where
+ "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
-lemma reflD:
+
+lemma reflD:
"[| refl(A, r); x \<in> A |] ==> <x,x>:r"
apply (unfold refl_def, auto)
done
@@ -76,25 +77,25 @@
lemma Cons_gen_prefix_aux:
- "[| <xs', ys'> \<in> gen_prefix(A, r) |]
- ==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->
- (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
+ "[| <xs', ys'> \<in> gen_prefix(A, r) |]
+ ==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->
+ (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
<x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))"
apply (erule gen_prefix.induct)
-prefer 3 apply (force intro: gen_prefix.append, auto)
+prefer 3 apply (force intro: gen_prefix.append, auto)
done
lemma Cons_gen_prefixE:
- "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
- !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
+ "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
+ !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
<xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P"
-apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
-apply (blast dest: Cons_gen_prefix_aux)
+apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
+apply (blast dest: Cons_gen_prefix_aux)
done
declare Cons_gen_prefixE [elim!]
-lemma Cons_gen_prefix_Cons:
-"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))
+lemma Cons_gen_prefix_Cons:
+"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))
<-> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))"
apply (auto intro: gen_prefix.prepend)
done
@@ -142,7 +143,7 @@
(* Transitivity *)
(* A lemma for proving gen_prefix_trans_comp *)
-lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
+lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
\<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)"
apply (erule list.induct)
apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
@@ -151,7 +152,7 @@
(* Lemma proving transitivity and more*)
lemma gen_prefix_trans_comp [rule_format (no_asm)]:
- "<x, y>: gen_prefix(A, r) ==>
+ "<x, y>: gen_prefix(A, r) ==>
(\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)--><x, z> \<in> gen_prefix(A, s O r))"
apply (erule gen_prefix.induct)
apply (auto elim: ConsE simp add: Nil_gen_prefix)
@@ -171,14 +172,14 @@
apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
done
-lemma trans_on_gen_prefix:
+lemma trans_on_gen_prefix:
"trans(r) ==> trans[list(A)](gen_prefix(A, r))"
apply (drule_tac A = A in trans_gen_prefix)
apply (unfold trans_def trans_on_def, blast)
done
lemma prefix_gen_prefix_trans:
- "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
+ "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
==> <x, z> \<in> gen_prefix(A, r)"
apply (unfold prefix_def)
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
@@ -186,8 +187,8 @@
done
-lemma gen_prefix_prefix_trans:
-"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
+lemma gen_prefix_prefix_trans:
+"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
==> <x, z> \<in> gen_prefix(A, r)"
apply (unfold prefix_def)
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
@@ -202,7 +203,7 @@
lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))"
apply (simp (no_asm) add: antisym_def)
apply (rule impI [THEN allI, THEN allI])
-apply (erule gen_prefix.induct, blast)
+apply (erule gen_prefix.induct, blast)
apply (simp add: antisym_def, blast)
txt{*append case is hardest*}
apply clarify
@@ -227,8 +228,8 @@
by (induct_tac "xs", auto)
declare gen_prefix_Nil [simp]
-lemma same_gen_prefix_gen_prefix:
- "[| refl(A, r); xs \<in> list(A) |] ==>
+lemma same_gen_prefix_gen_prefix:
+ "[| refl(A, r); xs \<in> list(A) |] ==>
<xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \<in> gen_prefix(A, r)"
apply (unfold refl_def)
apply (induct_tac "xs")
@@ -236,13 +237,13 @@
done
declare same_gen_prefix_gen_prefix [simp]
-lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
- <xs, Cons(y,ys)> \<in> gen_prefix(A,r) <->
+lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+ <xs, Cons(y,ys)> \<in> gen_prefix(A,r) <->
(xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))"
apply (induct_tac "xs", auto)
done
-lemma gen_prefix_take_append: "[| refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
+lemma gen_prefix_take_append: "[| refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
==> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
apply (erule gen_prefix.induct)
apply (simp (no_asm_simp))
@@ -252,8 +253,8 @@
apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type)
done
-lemma gen_prefix_append_both: "[| refl(A, r); <xs,ys> \<in> gen_prefix(A,r);
- length(xs) = length(ys); zs \<in> list(A) |]
+lemma gen_prefix_append_both: "[| refl(A, r); <xs,ys> \<in> gen_prefix(A,r);
+ length(xs) = length(ys); zs \<in> list(A) |]
==> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
apply (drule_tac zs = zs in gen_prefix_take_append, assumption+)
apply (subgoal_tac "take (length (xs), ys) =ys")
@@ -265,8 +266,8 @@
by (auto simp add: app_assoc)
lemma append_one_gen_prefix_lemma [rule_format]:
- "[| <xs,ys> \<in> gen_prefix(A, r); refl(A, r) |]
- ==> length(xs) < length(ys) -->
+ "[| <xs,ys> \<in> gen_prefix(A, r); refl(A, r) |]
+ ==> length(xs) < length(ys) -->
<xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
apply (erule gen_prefix.induct, blast)
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
@@ -286,9 +287,9 @@
apply (simplesubst append_cons_conv)
apply (rule_tac [2] gen_prefix.append)
apply (auto elim: ConsE simp add: gen_prefix_append_both)
-done
+done
-lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |]
+lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |]
==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
apply (blast intro: append_one_gen_prefix_lemma)
done
@@ -296,24 +297,24 @@
(** Proving the equivalence with Charpentier's definition **)
-lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
- \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
+lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
+ \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
--> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r"
-apply (induct_tac "xs", simp, clarify)
-apply simp
-apply (erule natE, auto)
+apply (induct_tac "xs", simp, clarify)
+apply simp
+apply (erule natE, auto)
done
-lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
+lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
==> <nth(i, xs), nth(i, ys)>:r"
apply (cut_tac A = A in gen_prefix.dom_subset)
apply (rule gen_prefix_imp_nth_lemma)
apply (auto simp add: lt_nat_in_nat)
done
-lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
- \<forall>ys \<in> list(A). length(xs) \<le> length(ys)
- --> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)
+lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
+ \<forall>ys \<in> list(A). length(xs) \<le> length(ys)
+ --> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)
--> <xs, ys> \<in> gen_prefix(A, r)"
apply (induct_tac "xs")
apply (simp_all (no_asm_simp))
@@ -322,12 +323,12 @@
apply (force intro!: nat_0_le simp add: lt_nat_in_nat)
done
-lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->
- (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
+lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->
+ (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
(\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))"
apply (rule iffI)
apply (frule gen_prefix.dom_subset [THEN subsetD])
-apply (frule gen_prefix_length_le, auto)
+apply (frule gen_prefix_length_le, auto)
apply (rule_tac [2] nth_imp_gen_prefix)
apply (drule gen_prefix_imp_nth)
apply (auto simp add: lt_nat_in_nat)
@@ -360,7 +361,7 @@
(* Monotonicity of "set" operator WRT prefix *)
-lemma set_of_list_prefix_mono:
+lemma set_of_list_prefix_mono:
"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)"
apply (unfold prefix_def)
@@ -389,13 +390,13 @@
done
declare prefix_Nil [iff]
-lemma Cons_prefix_Cons:
+lemma Cons_prefix_Cons:
"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) <-> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)"
apply (unfold prefix_def, auto)
done
declare Cons_prefix_Cons [iff]
-lemma same_prefix_prefix:
+lemma same_prefix_prefix:
"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) <-> (<ys,zs> \<in> prefix(A))"
apply (unfold prefix_def)
apply (subgoal_tac "refl (A,id (A))")
@@ -410,23 +411,23 @@
done
declare same_prefix_prefix_Nil [simp]
-lemma prefix_appendI:
+lemma prefix_appendI:
"[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)"
apply (unfold prefix_def)
apply (erule gen_prefix.append, assumption)
done
declare prefix_appendI [simp]
-lemma prefix_Cons:
-"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
- <xs,Cons(y,ys)> \<in> prefix(A) <->
+lemma prefix_Cons:
+"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+ <xs,Cons(y,ys)> \<in> prefix(A) <->
(xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))"
apply (unfold prefix_def)
apply (auto simp add: gen_prefix_Cons)
done
-lemma append_one_prefix:
- "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
+lemma append_one_prefix:
+ "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
apply (unfold prefix_def)
apply (subgoal_tac "refl (A, id (A))")
@@ -434,7 +435,7 @@
apply (auto simp add: refl_def)
done
-lemma prefix_length_le:
+lemma prefix_length_le:
"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)"
apply (unfold prefix_def)
apply (blast dest: gen_prefix_length_le)
@@ -445,13 +446,13 @@
apply (blast intro!: gen_prefix.dom_subset)
done
-lemma strict_prefix_type:
+lemma strict_prefix_type:
"strict_prefix(A) <= list(A)*list(A)"
apply (unfold strict_prefix_def)
apply (blast intro!: prefix_type [THEN subsetD])
done
-lemma strict_prefix_length_lt_aux:
+lemma strict_prefix_length_lt_aux:
"<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys --> length(xs) < length(ys)"
apply (unfold prefix_def)
apply (erule gen_prefix.induct, clarify)
@@ -464,7 +465,7 @@
apply auto
done
-lemma strict_prefix_length_lt:
+lemma strict_prefix_length_lt:
"<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"
apply (unfold strict_prefix_def)
apply (rule strict_prefix_length_lt_aux [THEN mp])
@@ -472,7 +473,7 @@
done
(*Equivalence to the definition used in Lex/Prefix.thy*)
-lemma prefix_iff:
+lemma prefix_iff:
"<xs,zs> \<in> prefix(A) <-> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)"
apply (unfold prefix_def)
apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
@@ -490,8 +491,8 @@
apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
done
-lemma prefix_snoc:
-"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+lemma prefix_snoc:
+"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
<xs, ys@[y]> \<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
apply (simp (no_asm) add: prefix_iff)
apply (rule iffI, clarify)
@@ -501,28 +502,28 @@
done
declare prefix_snoc [simp]
-lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
- (<xs, ys@zs> \<in> prefix(A)) <->
+lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
+ (<xs, ys@zs> \<in> prefix(A)) <->
(<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))"
-apply (erule list_append_induct, force, clarify)
-apply (rule iffI)
+apply (erule list_append_induct, force, clarify)
+apply (rule iffI)
apply (simp add: add: app_assoc [symmetric])
-apply (erule disjE)
-apply (rule disjI2)
-apply (rule_tac x = "y @ [x]" in exI)
+apply (erule disjE)
+apply (rule disjI2)
+apply (rule_tac x = "y @ [x]" in exI)
apply (simp add: add: app_assoc [symmetric], force+)
done
(*Although the prefix ordering is not linear, the prefixes of a list
are linearly ordered.*)
-lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
- ==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)
+lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
+ ==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)
--><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
apply (erule list_append_induct, auto)
done
-lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
+lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
apply (cut_tac prefix_type)
apply (blast del: disjCI intro: common_prefix_linear_lemma)
@@ -574,7 +575,7 @@
by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le)
-lemma prefix_imp_pfixLe:
+lemma prefix_imp_pfixLe:
"<xs,ys>:prefix(nat)==> xs pfixLe ys"
apply (unfold prefix_def)
@@ -607,14 +608,14 @@
lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
by (blast intro: antisym_gen_prefix [THEN antisymE])
-lemma prefix_imp_pfixGe:
+lemma prefix_imp_pfixGe:
"<xs,ys>:prefix(nat) ==> xs pfixGe ys"
apply (unfold prefix_def Ge_def)
apply (rule gen_prefix_mono [THEN subsetD], auto)
done
(* Added by Sidi \<in> prefix and take *)
-lemma prefix_imp_take:
+lemma prefix_imp_take:
"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)"
apply (unfold prefix_def)
@@ -655,9 +656,9 @@
lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)"
by (auto dest!: gen_prefix_imp_nth simp add: prefix_def)
-lemma nth_imp_prefix:
- "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
- !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
+lemma nth_imp_prefix:
+ "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
+ !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
==> <xs,ys> \<in> prefix(A)"
apply (auto simp add: prefix_def nth_imp_gen_prefix)
apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def)
@@ -665,7 +666,7 @@
done
-lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
+lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
<xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)"
apply (cut_tac A = A in prefix_type)
apply (rule nth_imp_prefix, blast, blast)
--- a/src/ZF/UNITY/Increasing.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Increasing.thy Sun Oct 07 15:49:25 2007 +0200
@@ -23,11 +23,9 @@
{F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
(\<forall>x \<in> state. f(x):A)}"
-syntax
- IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
-
-translations
- "IncWrt(f,r,A)" => "Increasing[A](r,f)"
+abbreviation (input)
+ IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) where
+ "f IncreasingWrt r/A == Increasing[A](r,f)"
(** increasing **)
--- a/src/ZF/UNITY/Mutex.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Mutex.thy Sun Oct 07 15:49:25 2007 +0200
@@ -15,27 +15,19 @@
the usual ZF typechecking: an ill-tyed expressions reduce to the empty set.
*}
-consts
- p :: i
- m :: i
- n :: i
- u :: i
- v :: i
-
-translations
- "p" == "Var([0])"
- "m" == "Var([1])"
- "n" == "Var([0,0])"
- "u" == "Var([0,1])"
- "v" == "Var([1,0])"
-
+abbreviation "p == Var([0])"
+abbreviation "m == Var([1])"
+abbreviation "n == Var([0,0])"
+abbreviation "u == Var([0,1])"
+abbreviation "v == Var([1,0])"
+
axioms --{** Type declarations **}
p_type: "type_of(p)=bool & default_val(p)=0"
m_type: "type_of(m)=int & default_val(m)=#0"
n_type: "type_of(n)=int & default_val(n)=#0"
u_type: "type_of(u)=bool & default_val(u)=0"
v_type: "type_of(v)=bool & default_val(v)=0"
-
+
constdefs
(** The program for process U **)
U0 :: i
@@ -53,9 +45,9 @@
U4 :: i
"U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
-
+
(** The program for process V **)
-
+
V0 :: i
"V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
@@ -180,18 +172,18 @@
declare bad_IU_def [THEN def_set_simp, simp]
lemma IU: "Mutex \<in> Always(IU)"
-apply (rule AlwaysI, force)
-apply (unfold Mutex_def, safety, auto)
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, safety, auto)
done
lemma IV: "Mutex \<in> Always(IV)"
-apply (rule AlwaysI, force)
-apply (unfold Mutex_def, safety)
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, safety)
done
(*The safety property: mutual exclusion*)
lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
-apply (rule Always_weaken)
+apply (rule Always_weaken)
apply (rule Always_Int_I [OF IU IV], auto)
done
@@ -203,13 +195,13 @@
done
lemma "Mutex \<in> Always(bad_IU)"
-apply (rule AlwaysI, force)
+apply (rule AlwaysI, force)
apply (unfold Mutex_def, safety, auto)
apply (subgoal_tac "#1 $<= #3")
apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
apply auto
-(*Resulting state: n=1, p=false, m=4, u=false.
+(*Resulting state: n=1, p=false, m=4, u=false.
Execution of V1 (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
oops
@@ -291,7 +283,7 @@
lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
Int_lower2 [THEN subset_imp_LeadsTo]])
-apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
+apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
apply (auto dest!: p_value_type simp add: bool_def)
done
--- a/src/ZF/Univ.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Univ.thy Sun Oct 07 15:49:25 2007 +0200
@@ -17,9 +17,9 @@
Vfrom :: "[i,i]=>i"
"Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
-syntax Vset :: "i=>i"
-translations
- "Vset(x)" == "Vfrom(0,x)"
+abbreviation
+ Vset :: "i=>i" where
+ "Vset(x) == Vfrom(0,x)"
constdefs