--- a/src/ZF/Coind/BCR.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/BCR.thy Mon May 21 14:46:30 2001 +0200
@@ -21,7 +21,7 @@
defs
isofenv_def "isofenv(ve,te) ==
ve_dom(ve) = te_dom(te) &
- ( ALL x:ve_dom(ve).
- EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+ ( \\<forall>x \\<in> ve_dom(ve).
+ \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
end
--- a/src/ZF/Coind/Dynamic.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Dynamic.thy Mon May 21 14:46:30 2001 +0200
@@ -12,25 +12,25 @@
domains "EvalRel" <= "ValEnv * Exp * Val"
intrs
eval_constI
- " [| ve:ValEnv; c:Const |] ==>
+ " [| ve \\<in> ValEnv; c \\<in> Const |] ==>
<ve,e_const(c),v_const(c)>:EvalRel"
eval_varI
- " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>
+ " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>
<ve,e_var(x),ve_app(ve,x)>:EvalRel"
eval_fnI
- " [| ve:ValEnv; x:ExVar; e:Exp |] ==>
+ " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>
<ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
eval_fixI
- " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;
+ " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;
v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>
<ve,e_fix(f,x,e),cl>:EvalRel "
eval_appI1
- " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;
+ " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;
<ve,e1,v_const(c1)>:EvalRel;
<ve,e2,v_const(c2)>:EvalRel |] ==>
<ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
eval_appI2
- " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;
+ " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;
<ve,e1,v_clos(xm,em,vem)>:EvalRel;
<ve,e2,v2>:EvalRel;
<ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>
--- a/src/ZF/Coind/ECR.ML Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/ECR.ML Mon May 21 14:46:30 2001 +0200
@@ -6,9 +6,9 @@
(* Specialised co-induction rule *)
-Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
+Goal "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; \
\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
-\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
+\ {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}: \
\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] \
\ ==> <v_clos(x, e, ve),t>:HasTyRel";
by (rtac (singletonI RS HasTyRel.coinduct) 1);
@@ -40,7 +40,7 @@
HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
Goalw [hastyenv_def]
- "[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
+ "[| ve \\<in> ValEnv; te \\<in> TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
by (asm_full_simp_tac
(simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
@@ -48,7 +48,7 @@
qed "hastyenv_owr";
Goalw [isofenv_def,hastyenv_def]
- "[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
+ "[| ve \\<in> ValEnv; te \\<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
by Safe_tac;
by (dtac bspec 1);
by (assume_tac 1);
--- a/src/ZF/Coind/ECR.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/ECR.thy Mon May 21 14:46:30 2001 +0200
@@ -14,12 +14,12 @@
domains "HasTyRel" <= "Val * Ty"
intrs
htr_constI
- "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
+ "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
htr_closI
- "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
+ "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv;
<te,e_fn(x,e),t>:ElabRel;
ve_dom(ve) = te_dom(te);
- {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
+ {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)
|] ==>
<v_clos(x,e,ve),t>:HasTyRel"
monos Pow_mono
@@ -33,6 +33,6 @@
hastyenv_def
" hastyenv(ve,te) ==
ve_dom(ve) = te_dom(te) &
- (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+ (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
end
--- a/src/ZF/Coind/Language.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Language.thy Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
c_app :: [i,i] => i (*Abstract constructor for fun application*)
rules
- constNEE "c:Const ==> c ~= 0"
- c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+ constNEE "c \\<in> Const ==> c \\<noteq> 0"
+ c_appI "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
consts
@@ -20,10 +20,10 @@
ExVar :: i (* Abstract type of variables *)
datatype
- "Exp" = e_const ("c:Const")
- | e_var ("x:ExVar")
- | e_fn ("x:ExVar","e:Exp")
- | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
- | e_app ("e1:Exp","e2:Exp")
+ "Exp" = e_const ("c \\<in> Const")
+ | e_var ("x \\<in> ExVar")
+ | e_fn ("x \\<in> ExVar","e \\<in> Exp")
+ | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
+ | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
end
--- a/src/ZF/Coind/MT.ML Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/MT.ML Mon May 21 14:46:30 2001 +0200
@@ -8,23 +8,23 @@
(* The Consistency theorem *)
(* ############################################################ *)
-Goal "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
-\ <v_const(c), t> : HasTyRel";
+Goal "[| c \\<in> Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
+\ <v_const(c), t> \\<in> HasTyRel";
by (Fast_tac 1);
qed "consistency_const";
Goalw [hastyenv_def]
- "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
+ "[| x \\<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
\ <ve_app(ve,x),t>:HasTyRel";
by (Fast_tac 1);
qed "consistency_var";
Goalw [hastyenv_def]
- "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \
+ "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; hastyenv(ve,te); \
\ <te,e_fn(x,e),t>:ElabRel \
-\ |] ==> <v_clos(x, e, ve), t> : HasTyRel";
+\ |] ==> <v_clos(x, e, ve), t> \\<in> HasTyRel";
by (Blast_tac 1);
qed "consistency_fn";
@@ -40,7 +40,7 @@
(ematch_tac [te_owrE] i));
Goalw [hastyenv_def]
- "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \
+ "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val; \
\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \
\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \
\ <cl,t>:HasTyRel";
@@ -75,12 +75,12 @@
qed "consistency_fix";
-Goal "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
+Goal "[| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const; \
\ <ve,e1,v_const(c1)>:EvalRel; \
-\ ALL t te. \
+\ \\<forall>t te. \
\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
-\ <ve, e2, v_const(c2)> : EvalRel; \
-\ ALL t te. \
+\ <ve, e2, v_const(c2)> \\<in> EvalRel; \
+\ \\<forall>t te. \
\ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
\ hastyenv(ve, te); \
\ <te,e_app(e1,e2),t>:ElabRel |] ==> \
@@ -89,19 +89,19 @@
by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
qed "consistency_app1";
-Goal "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
+Goal "[| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val; \
\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
-\ ALL t te. \
+\ \\<forall>t te. \
\ hastyenv(ve,te) --> \
\ <te,e1,t>:ElabRel --> \
\ <v_clos(xm,em,vem),t>:HasTyRel; \
\ <ve,e2,v2>:EvalRel; \
-\ ALL t te. \
+\ \\<forall>t te. \
\ hastyenv(ve,te) --> \
\ <te,e2,t>:ElabRel --> \
\ <v2,t>:HasTyRel; \
\ <ve_owr(vem,xm,v2),em,v>:EvalRel; \
-\ ALL t te. \
+\ \\<forall>t te. \
\ hastyenv(ve_owr(vem,xm,v2),te) --> \
\ <te,em,t>:ElabRel --> \
\ <v,t>:HasTyRel; \
@@ -130,14 +130,14 @@
qed "consistency_app2";
Goal "<ve,e,v>:EvalRel ==> \
-\ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
+\ (\\<forall>t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
by (etac EvalRel.induct 1);
by (blast_tac (claset() addIs [consistency_app2]) 6);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
qed "consistency";
-Goal "[| ve:ValEnv; te:TyEnv; \
+Goal "[| ve \\<in> ValEnv; te \\<in> TyEnv; \
\ isofenv(ve,te); \
\ <ve,e,v_const(c)>:EvalRel; \
\ <te,e,t>:ElabRel \
--- a/src/ZF/Coind/Map.ML Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Map.ML Mon May 21 14:46:30 2001 +0200
@@ -6,21 +6,21 @@
(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
-Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})";
+Goalw [TMap_def] "{0,1} \\<subseteq> {1} Un TMap(I, {0,1})";
by (Blast_tac 1);
result();
-Goalw [TMap_def] "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))";
+Goalw [TMap_def] "{0} Un TMap(I,1) \\<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))";
by (Blast_tac 1);
result();
-Goalw [TMap_def] "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))";
+Goalw [TMap_def] "{0,1} Un TMap(I,2) \\<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))";
by (Blast_tac 1);
result();
(*
Goalw [TMap_def]
- "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
+ "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \\<subseteq> \
\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
by (Blast_tac 1);
result();
@@ -31,19 +31,19 @@
(* Lemmas *)
(* ############################################################ *)
-Goal "Sigma(A,B)``{a} = (if a:A then B(a) else 0)";
+Goal "Sigma(A,B)``{a} = (if a \\<in> A then B(a) else 0)";
by Auto_tac;
qed "qbeta_if";
-Goal "a:A ==> Sigma(A,B)``{a} = B(a)";
+Goal "a \\<in> A ==> Sigma(A,B)``{a} = B(a)";
by (Fast_tac 1);
qed "qbeta";
-Goal "a~:A ==> Sigma(A,B)``{a} = 0";
+Goal "a\\<notin>A ==> Sigma(A,B)``{a} = 0";
by (Fast_tac 1);
qed "qbeta_emp";
-Goal "a ~: A ==> Sigma(A,B)``{a}=0";
+Goal "a \\<notin> A ==> Sigma(A,B)``{a}=0";
by (Fast_tac 1);
qed "image_Sigma1";
@@ -55,7 +55,7 @@
(* Lemmas *)
Goalw [quniv_def]
- "A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
+ "A \\<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \\<subseteq> quniv(X)";
by (rtac Pow_mono 1);
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
by (etac subset_trans 1);
@@ -66,7 +66,7 @@
(* Theorems *)
val prems = goalw Map.thy [PMap_def,TMap_def]
- "[| m:PMap(A,quniv(B)); !!x. x:A ==> x:univ(B) |] ==> m:quniv(B)";
+ "[| m \\<in> PMap(A,quniv(B)); !!x. x \\<in> A ==> x \\<in> univ(B) |] ==> m \\<in> quniv(B)";
by (cut_facts_tac prems 1);
by (rtac (MapQU_lemma RS subsetD) 1);
by (rtac subsetI 1);
@@ -78,7 +78,7 @@
(* Monotonicity *)
(* ############################################################ *)
-Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
+Goalw [PMap_def,TMap_def] "B \\<subseteq> C ==> PMap(A,B)<=PMap(A,C)";
by (Blast_tac 1);
qed "map_mono";
@@ -90,7 +90,7 @@
(** map_emp **)
-Goalw [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
+Goalw [map_emp_def,PMap_def,TMap_def] "map_emp \\<in> PMap(A,B)";
by Auto_tac;
qed "pmap_empI";
@@ -98,7 +98,7 @@
Goalw [map_owr_def,PMap_def,TMap_def]
- "[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)";
+ "[| m \\<in> PMap(A,B); a \\<in> A; b \\<in> B |] ==> map_owr(m,a,b):PMap(A,B)";
by Safe_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff])));
by (Fast_tac 1);
@@ -107,10 +107,10 @@
(*Remaining subgoal*)
by (rtac (excluded_middle RS disjE) 1);
by (etac image_Sigma1 1);
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
+by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 1);
by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1);
by Safe_tac;
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
+by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 3);
by (ALLGOALS Asm_full_simp_tac);
by (Fast_tac 1);
qed "pmap_owrI";
@@ -118,7 +118,7 @@
(** map_app **)
Goalw [TMap_def,map_app_def]
- "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
+ "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a) \\<noteq>0";
by (etac domainE 1);
by (dtac imageI 1);
by (Fast_tac 1);
@@ -126,12 +126,12 @@
qed "tmap_app_notempty";
Goalw [TMap_def,map_app_def,domain_def]
- "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+ "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
by (Fast_tac 1);
qed "tmap_appI";
Goalw [PMap_def]
- "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+ "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
by (ftac tmap_app_notempty 1);
by (assume_tac 1);
by (dtac tmap_appI 1);
@@ -142,12 +142,12 @@
(** domain **)
Goalw [TMap_def]
- "[| m:TMap(A,B); a:domain(m) |] ==> a:A";
+ "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
by (Fast_tac 1);
qed "tmap_domainD";
Goalw [PMap_def,TMap_def]
- "[| m:PMap(A,B); a:domain(m) |] ==> a:A";
+ "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
by (Fast_tac 1);
qed "pmap_domainD";
@@ -159,11 +159,11 @@
(* Lemmas *)
-Goal "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))";
+Goal "domain(\\<Union>x \\<in> A. B(x)) = (\\<Union>x \\<in> A. domain(B(x)))";
by (Fast_tac 1);
qed "domain_UN";
-Goal "domain(Sigma(A,B)) = {x:A. EX y. y:B(x)}";
+Goal "domain(Sigma(A,B)) = {x \\<in> A. \\<exists>y. y \\<in> B(x)}";
by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1);
by (Fast_tac 1);
qed "domain_Sigma";
@@ -175,7 +175,7 @@
qed "map_domain_emp";
Goalw [map_owr_def]
- "b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
+ "b \\<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
by (simp_tac (simpset() addsimps [domain_Sigma]) 1);
by (rtac equalityI 1);
by (Fast_tac 1);
@@ -201,6 +201,6 @@
by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "map_app_owr1";
-Goal "c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+Goal "c \\<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "map_app_owr2";
--- a/src/ZF/Coind/Map.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Map.thy Mon May 21 14:46:30 2001 +0200
@@ -6,23 +6,21 @@
Map = QUniv +
-consts
+constdefs
TMap :: [i,i] => i
+ "TMap(A,B) == {m \\<in> Pow(A*Union(B)).\\<forall>a \\<in> A. m``{a} \\<in> B}"
+
PMap :: [i,i] => i
-defs
- TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A. m``{a}:B}"
- PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
+ "PMap(A,B) == TMap(A,cons(0,B))"
-(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
+(* Note: 0 \\<in> B ==> TMap(A,B) = PMap(A,B) *)
-consts
map_emp :: i
+ "map_emp == 0"
+
map_owr :: [i,i,i]=>i
+ "map_owr(m,a,b) == \\<Sigma>x \\<in> {a} Un domain(m). if x=a then b else m``{x}"
map_app :: [i,i]=>i
-defs
- map_emp_def "map_emp == 0"
- map_owr_def "map_owr(m,a,b) ==
- SUM x:{a} Un domain(m). if x=a then b else m``{x}"
- map_app_def "map_app(m,a) == m``{a}"
+ "map_app(m,a) == m``{a}"
end
--- a/src/ZF/Coind/Static.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Static.thy Mon May 21 14:46:30 2001 +0200
@@ -12,21 +12,21 @@
domains "ElabRel" <= "TyEnv * Exp * Ty"
intrs
constI
- " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>
+ " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==>
<te,e_const(c),t>:ElabRel "
varI
- " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>
+ " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==>
<te,e_var(x),te_app(te,x)>:ElabRel "
fnI
- " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;
+ " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
<te_owr(te,x,t1),e,t2>:ElabRel |] ==>
<te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
fixI
- " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;
+ " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty;
<te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>
<te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
appI
- " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;
+ " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
<te,e1,t_fun(t1,t2)>:ElabRel;
<te,e2,t1>:ElabRel |] ==>
<te,e_app(e1,e2),t2>:ElabRel "
--- a/src/ZF/Coind/Types.ML Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Types.ML Mon May 21 14:46:30 2001 +0200
@@ -10,12 +10,12 @@
by (Simp_tac 1);
qed "te_app_owr1";
-Goal "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
+Goal "x \\<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
by Auto_tac;
qed "te_app_owr2";
-Goal "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
-by (res_inst_tac [("P","x:te_dom(te)")] impE 1);
+Goal "[| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> te_app(te,x):Ty";
+by (res_inst_tac [("P","x \\<in> te_dom(te)")] impE 1);
by (assume_tac 2);
by (assume_tac 2);
by (etac TyEnv.induct 1);
--- a/src/ZF/Coind/Types.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Types.thy Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
TyConst :: i (* Abstract type of type constants *)
datatype
- "Ty" = t_const ("tc:TyConst")
- | t_fun ("t1:Ty","t2:Ty")
+ "Ty" = t_const ("tc \\<in> TyConst")
+ | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
(* Definition of type environments and associated operators *)
@@ -22,7 +22,7 @@
datatype
"TyEnv" = te_emp
- | te_owr ("te:TyEnv","x:ExVar","t:Ty")
+ | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty")
consts
te_dom :: i => i
--- a/src/ZF/Coind/Values.ML Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Values.ML Mon May 21 14:46:30 2001 +0200
@@ -9,7 +9,7 @@
(* Elimination rules *)
val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
- "[| ve:ValEnv; !!m.[| ve=ve_mk(m); m:PMap(ExVar,Val) |] ==> Q |] ==> Q";
+ "[| ve \\<in> ValEnv; !!m.[| ve=ve_mk(m); m \\<in> PMap(ExVar,Val) |] ==> Q |] ==> Q";
by (cut_facts_tac prems 1);
by (etac CollectE 1);
by (etac exE 1);
@@ -20,10 +20,10 @@
qed "ValEnvE";
val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
- "[| v:Val; \
-\ !!c. [| v = v_const(c); c:Const |] ==> Q;\
+ "[| v \\<in> Val; \
+\ !!c. [| v = v_const(c); c \\<in> Const |] ==> Q;\
\ !!e ve x. \
-\ [| v = v_clos(x,e,ve); x:ExVar; e:Exp; ve:ValEnv |] ==> Q \
+\ [| v = v_clos(x,e,ve); x \\<in> ExVar; e \\<in> Exp; ve \\<in> ValEnv |] ==> Q \
\ |] ==> \
\ Q";
by (cut_facts_tac prems 1);
@@ -43,7 +43,7 @@
(* Nonempty sets *)
Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
- "v_clos(x,e,ve) ~= 0";
+ "v_clos(x,e,ve) \\<noteq> 0";
by (Blast_tac 1);
qed "v_closNE";
@@ -51,7 +51,7 @@
AddSEs [v_closNE RS notE];
Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
- "c:Const ==> v_const(c) ~= 0";
+ "c \\<in> Const ==> v_const(c) \\<noteq> 0";
by (dtac constNEE 1);
by Auto_tac;
qed "v_constNE";
@@ -60,32 +60,32 @@
(* Proving that the empty set is not a value *)
-Goal "v:Val ==> v ~= 0";
+Goal "v \\<in> Val ==> v \\<noteq> 0";
by (etac ValE 1);
by Auto_tac;
qed "ValNEE";
(* Equalities for value environments *)
-Goal "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
+Goal "[| ve \\<in> ValEnv; v \\<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
by (etac ValEnvE 1);
by (auto_tac (claset(),
simpset() addsimps [map_domain_owr]));
qed "ve_dom_owr";
-Goal "ve:ValEnv \
+Goal "ve \\<in> ValEnv \
\ ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))";
by (etac ValEnvE 1);
by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "ve_app_owr";
-Goal "ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
+Goal "ve \\<in> ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
by (etac ValEnvE 1);
by (Asm_full_simp_tac 1);
by (rtac map_app_owr1 1);
qed "ve_app_owr1";
-Goal "ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+Goal "ve \\<in> ValEnv ==> x \\<noteq> y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
by (etac ValEnvE 1);
by (Asm_full_simp_tac 1);
by (rtac map_app_owr2 1);
@@ -94,7 +94,7 @@
(* Introduction rules for operators on value environments *)
-Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
+Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> ve_app(ve,x):Val";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
@@ -103,7 +103,7 @@
by (assume_tac 1);
qed "ve_appI";
-Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
+Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> x \\<in> ExVar";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
@@ -112,12 +112,12 @@
by (assume_tac 1);
qed "ve_domI";
-Goalw [ve_emp_def] "ve_emp:ValEnv";
+Goalw [ve_emp_def] "ve_emp \\<in> ValEnv";
by (rtac Val_ValEnv.ve_mk_I 1);
by (rtac pmap_empI 1);
qed "ve_empI";
-Goal "[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
+Goal "[|ve \\<in> ValEnv; x \\<in> ExVar; v \\<in> Val |] ==> ve_owr(ve,x,v):ValEnv";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
--- a/src/ZF/Coind/Values.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Values.thy Mon May 21 14:46:30 2001 +0200
@@ -12,10 +12,10 @@
Val, ValEnv, Val_ValEnv :: i
codatatype
- "Val" = v_const ("c:Const")
- | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
+ "Val" = v_const ("c \\<in> Const")
+ | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
and
- "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
+ "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
monos map_mono
type_intrs A_into_univ, mapQU