--- a/src/HOL/Arith.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Arith.ML Fri Mar 24 12:30:35 1995 +0100
@@ -175,7 +175,7 @@
val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
-goalw Nat.thy [less_def] "<m,n> : pred_nat^+ = (m<n)";
+goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
by (rtac refl 1);
qed "less_eq";
--- a/src/HOL/Arith.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Arith.thy Fri Mar 24 12:30:35 1995 +0100
@@ -26,6 +26,6 @@
(*"Difference" is subtraction of natural numbers.
There are no negative numbers; we have
- m - n = 0 iff m<=n and m - n = Suc(k) iff m>n.
+ m - n = 0 iff m<=n and m - n = Suc(k) iff m)n.
Also, nat_rec(m, 0, %z w.z) is pred(m). *)
--- a/src/HOL/IMP/Com.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IMP/Com.thy Fri Mar 24 12:30:35 1995 +0100
@@ -26,9 +26,9 @@
(** Evaluation of arithmetic expressions **)
consts evala :: "(aexp*state*nat)set"
- "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50)
+ "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50)
translations
- "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+ "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
inductive "evala"
intrs
N "<N(n),s> -a-> n"
@@ -51,10 +51,10 @@
(** Evaluation of boolean expressions **)
consts evalb :: "(bexp*state*bool)set"
- "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50)
+ "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50)
translations
- "<be,sig> -b-> b" == "<be,sig,b> : evalb"
+ "<be,sig> -b-> b" == "(be,sig,b) : evalb"
inductive "evalb"
intrs (*avoid clash with ML constructors true, false*)
@@ -79,11 +79,11 @@
(** Execution of commands **)
consts evalc :: "(com*state*state)set"
- "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
- "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95)
+ "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
+ "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95)
translations
- "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+ "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
rules
assign_def "s[m/x] == (%y. if y=x then m else s y)"
--- a/src/HOL/IMP/Equiv.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IMP/Equiv.ML Fri Mar 24 12:30:35 1995 +0100
@@ -25,7 +25,7 @@
val BfstD = read_instantiate_sg (sign_of Equiv.thy)
[("P","%x.B ?b x")] (fst_conv RS subst);
-goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
+goal Equiv.thy "!!c. <c,s> -c-> t ==> (s,t) : C(c)";
(* start with rule induction *)
be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
--- a/src/HOL/IMP/Hoare.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IMP/Hoare.ML Fri Mar 24 12:30:35 1995 +0100
@@ -39,8 +39,8 @@
qed"hoare_if";
val major::prems = goal Hoare.thy
- "[| <a,b> :lfp f; mono f; \
-\ !!a b. <a,b> : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
+ "[| (a,b) :lfp f; mono f; \
+\ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
by(res_inst_tac [("c1","P")] (split RS subst) 1);
br (major RS induct) 1;
brs prems 1;
--- a/src/HOL/IMP/Hoare.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IMP/Hoare.thy Fri Mar 24 12:30:35 1995 +0100
@@ -12,7 +12,7 @@
(* syntax "@spec" :: "[bool,com,bool] => bool" *)
("{{(1_)}}/ (_)/ {{(1_)}}" 10)
defs
- spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
+ spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
end
(* Pretty-printing of assertions.
Not very helpful as long as programs are not pretty-printed.
--- a/src/HOL/IOA/meta_theory/Asig.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/Asig.thy Fri Mar 24 12:30:35 1995 +0100
@@ -39,7 +39,7 @@
mk_ext_asig_def
- "mk_ext_asig(triple) == <inputs(triple), outputs(triple), {}>"
+ "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
end
--- a/src/HOL/IOA/meta_theory/IOA.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/IOA.ML Fri Mar 24 12:30:35 1995 +0100
@@ -13,12 +13,12 @@
val exec_rws = [executions_def,is_execution_fragment_def];
goal IOA.thy
-"asig_of(<x,y,z>) = x & starts_of(<x,y,z>) = y & trans_of(<x,y,z>) = z";
+"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
by (simp_tac (SS addsimps ioa_projections) 1);
qed "ioa_triple_proj";
goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def]
- "!!A. [| IOA(A); <s1,a,s2>:trans_of(A) |] ==> a:actions(asig_of(A))";
+ "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
by (REPEAT(etac conjE 1));
by (EVERY1[etac allE, etac impE, atac]);
by (asm_full_simp_tac SS 1);
@@ -45,18 +45,18 @@
qed "mk_behaviour_thm";
goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
- by (res_inst_tac [("x","<%i.None,%i.s>")] bexI 1);
+ by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1);
by (simp_tac SS 1);
by (asm_simp_tac (SS addsimps exec_rws) 1);
qed "reachable_0";
goalw IOA.thy (reachable_def::exec_rws)
-"!!A. [| reachable A s; <s,a,t> : trans_of(A) |] ==> reachable A t";
+"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
by(asm_full_simp_tac SS 1);
by(safe_tac set_cs);
- by(res_inst_tac [("x","<%i.if i<n then fst ex i \
+ by(res_inst_tac [("x","(%i.if i<n then fst ex i \
\ else (if i=n then Some a else None), \
-\ %i.if i<Suc n then snd ex i else t>")] bexI 1);
+\ %i.if i<Suc n then snd ex i else t)")] bexI 1);
by(res_inst_tac [("x","Suc(n)")] exI 1);
by(simp_tac SS 1);
by(asm_simp_tac (SS delsimps [less_Suc_eq]) 1);
@@ -73,7 +73,7 @@
val [p1,p2] = goalw IOA.thy [invariant_def]
"[| !!s. s:starts_of(A) ==> P(s); \
-\ !!s t a. [|reachable A s; P(s)|] ==> <s,a,t>: trans_of(A) --> P(t) |] \
+\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
\ ==> invariant A P";
by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
by (safe_tac set_cs);
@@ -91,7 +91,7 @@
val [p1,p2] = goal IOA.thy
"[| !!s. s : starts_of(A) ==> P(s); \
-\ !!s t a. reachable A s ==> P(s) --> <s,a,t>:trans_of(A) --> P(t) \
+\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
\ |] ==> invariant A P";
by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
qed "invariantI1";
@@ -121,18 +121,18 @@
goal IOA.thy
-"<s,a,t> : trans_of(A || B || C || D) = \
+"(s,a,t) : trans_of(A || B || C || D) = \
\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \
\ a:actions(asig_of(D))) & \
-\ (if a:actions(asig_of(A)) then <fst(s),a,fst(t)>:trans_of(A) \
+\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \
\ else fst t=fst s) & \
-\ (if a:actions(asig_of(B)) then <fst(snd(s)),a,fst(snd(t))>:trans_of(B) \
+\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \
\ else fst(snd(t))=fst(snd(s))) & \
\ (if a:actions(asig_of(C)) then \
-\ <fst(snd(snd(s))),a,fst(snd(snd(t)))>:trans_of(C) \
+\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \
\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \
\ (if a:actions(asig_of(D)) then \
-\ <snd(snd(snd(s))),a,snd(snd(snd(t)))>:trans_of(D) \
+\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
ioa_projections)
--- a/src/HOL/IOA/meta_theory/IOA.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/IOA.thy Fri Mar 24 12:30:35 1995 +0100
@@ -62,7 +62,7 @@
state_trans_def
"state_trans asig R == \
\ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
- \ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
+ \ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
asig_of_def "asig_of == fst"
@@ -83,7 +83,7 @@
"is_execution_fragment A ex == \
\ let act = fst(ex); state = snd(ex) \
\ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & \
- \ (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
+ \ (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
executions_def
@@ -98,7 +98,7 @@
* ----------------
* reachable(ioa,x)
*
- * reachable(ioa,s) & ? <s,a,s'>:trans_of(ioa)
+ * reachable(ioa,s) & ? (s,a,s'):trans_of(ioa)
* -------------------------------------------
* reachable(ioa,s')
*
@@ -147,35 +147,35 @@
asig_comp_def
"asig_comp a1 a2 == \
- \ (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \
+ \ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \
\ (outputs(a1) Un outputs(a2)), \
- \ (internals(a1) Un internals(a2))>)"
+ \ (internals(a1) Un internals(a2))))"
par_def
"(ioa1 || ioa2) == \
- \ <asig_comp (asig_of ioa1) (asig_of ioa2), \
+ \ (asig_comp (asig_of ioa1) (asig_of ioa2), \
\ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, \
\ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
\ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
\ (if a:actions(asig_of(ioa1)) then \
- \ <fst(s),a,fst(t)>:trans_of(ioa1) \
+ \ (fst(s),a,fst(t)):trans_of(ioa1) \
\ else fst(t) = fst(s)) \
\ & \
\ (if a:actions(asig_of(ioa2)) then \
- \ <snd(s),a,snd(t)>:trans_of(ioa2) \
- \ else snd(t) = snd(s))}>"
+ \ (snd(s),a,snd(t)):trans_of(ioa2) \
+ \ else snd(t) = snd(s))})"
restrict_asig_def
"restrict_asig asig actns == \
-\ <inputs(asig) Int actns, outputs(asig) Int actns, \
-\ internals(asig) Un (externals(asig) - actns)>"
+\ (inputs(asig) Int actns, outputs(asig) Int actns, \
+\ internals(asig) Un (externals(asig) - actns))"
restrict_def
"restrict ioa actns == \
-\ <restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa)>"
+\ (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
ioa_implements_def
--- a/src/HOL/IOA/meta_theory/Solve.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.ML Fri Mar 24 12:30:35 1995 +0100
@@ -18,7 +18,7 @@
by (safe_tac set_cs);
(* give execution of abstract automata *)
- by (res_inst_tac[("x","<mk_behaviour A (fst ex),%i.f(snd ex i)>")] bexI 1);
+ by (res_inst_tac[("x","(mk_behaviour A (fst ex),%i.f(snd ex i))")] bexI 1);
(* Behaviours coincide *)
by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1);
--- a/src/HOL/IOA/meta_theory/Solve.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.thy Fri Mar 24 12:30:35 1995 +0100
@@ -18,9 +18,9 @@
"is_weak_pmap f C A == \
\ (!s:starts_of(C). f(s):starts_of(A)) & \
\ (!s t a. reachable C s & \
-\ <s,a,t>:trans_of(C) \
+\ (s,a,t):trans_of(C) \
\ --> (if a:externals(asig_of(C)) then \
-\ <f(s),a,f(t)>:trans_of(A) \
+\ (f(s),a,f(t)):trans_of(A) \
\ else f(s)=f(t)))"
end
--- a/src/HOL/Integ/Equiv.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Equiv.ML Fri Mar 24 12:30:35 1995 +0100
@@ -19,24 +19,24 @@
by (fast_tac (comp_cs addSEs [converseD]) 1);
qed "sym_trans_comp_subset";
-val [major,minor]=goal Equiv.thy "[|<x,y>:r; z=<x,y>|] ==> z:r";
+val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==> z:r";
by (simp_tac (prod_ss addsimps [minor]) 1);
by (rtac major 1);
qed "BreakPair";
-val [major]=goal Equiv.thy "[|? x y. <x,y>:r & z=<x,y>|] ==> z:r";
+val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==> z:r";
by (resolve_tac [major RS exE] 1);
by (etac exE 1);
by (etac conjE 1);
by (asm_simp_tac (prod_ss addsimps [minor]) 1);
qed "BreakPair1";
-val [major,minor]=goal Equiv.thy "[|z:r; z=<x,y>|] ==> <x,y>:r";
+val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r";
by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
by (rtac major 1);
qed "BuildPair";
-val [major]=goal Equiv.thy "[|? z:r. <x,y>=z|] ==> <x,y>:r";
+val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r";
by (resolve_tac [major RS bexE] 1);
by (asm_simp_tac (prod_ss addsimps []) 1);
qed "BuildPair1";
@@ -65,7 +65,7 @@
goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
"!!A r. [| converse(r) O r = r; Domain(r) = A |] ==> equiv A r";
by (etac equalityE 1);
-by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
+by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
by (safe_tac set_cs);
by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
@@ -84,14 +84,14 @@
(*Lemma for the next result*)
goalw Equiv.thy [equiv_def,trans_def,sym_def]
- "!!A r. [| equiv A r; <a,b>: r |] ==> r^^{a} <= r^^{b}";
+ "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
by (safe_tac rel_cs);
by (rtac ImageI 1);
by (fast_tac rel_cs 2);
by (fast_tac rel_cs 1);
qed "equiv_class_subset";
-goal Equiv.thy "!!A r. [| equiv A r; <a,b>: r |] ==> r^^{a} = r^^{b}";
+goal Equiv.thy "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}";
by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
by (rewrite_goals_tac [equiv_def,sym_def]);
by (fast_tac rel_cs 1);
@@ -105,18 +105,18 @@
(*Lemma for the next result*)
goalw Equiv.thy [equiv_def,refl_def]
- "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> <a,b>: r";
+ "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r";
by (fast_tac rel_cs 1);
qed "subset_equiv_class";
val prems = goal Equiv.thy
- "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> <a,b>: r";
+ "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r";
by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
qed "eq_equiv_class";
(*thus r^^{a} = r^^{b} as well*)
goalw Equiv.thy [equiv_def,trans_def,sym_def]
- "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> <a,b>: r";
+ "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
by (fast_tac rel_cs 1);
qed "equiv_class_nondisjoint";
@@ -126,7 +126,7 @@
qed "equiv_type";
goal Equiv.thy
- "!!A r. equiv A r ==> (<x,y>: r) = (r^^{x} = r^^{y} & x:A & y:A)";
+ "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
by (safe_tac rel_cs);
by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
by ((rtac eq_equiv_class 3) THEN
@@ -138,7 +138,7 @@
qed "equiv_class_eq_iff";
goal Equiv.thy
- "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = (<x,y>: r)";
+ "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
by (safe_tac rel_cs);
by ((rtac eq_equiv_class 1) THEN
(assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
@@ -227,7 +227,7 @@
val _::_::prems = goalw Equiv.thy [quotient_def]
"[| equiv A r; congruent r b; \
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
-\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
+\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \
\ ==> X=Y";
by (cut_facts_tac prems 1);
by (safe_tac rel_cs);
@@ -286,8 +286,8 @@
than the direct proof*)
val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
"[| equiv A r; \
-\ !! y z w. [| w: A; <y,z> : r |] ==> b y w = b z w; \
-\ !! y z w. [| w: A; <y,z> : r |] ==> b w y = b w z \
+\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \
+\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \
\ |] ==> congruent2 r b";
by (cut_facts_tac prems 1);
by (safe_tac rel_cs);
@@ -299,7 +299,7 @@
val [equivA,commute,congt] = goal Equiv.thy
"[| equiv A r; \
\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \
-\ !! y z w. [| w: A; <y,z>: r |] ==> b w y = b w z \
+\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \
\ |] ==> congruent2 r b";
by (resolve_tac [equivA RS congruent2I] 1);
by (rtac (commute RS trans) 1);
--- a/src/HOL/Integ/Equiv.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Equiv.thy Fri Mar 24 12:30:35 1995 +0100
@@ -18,11 +18,11 @@
congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool"
defs
- refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. <x,x> : r)"
- sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
+ refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)"
+ sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r"
equiv_def "equiv A r == refl A r & sym(r) & trans(r)"
quotient_def "A/r == UN x:A. {r^^{x}}"
- congruent_def "congruent r b == ALL y z. <y,z>:r --> b(y)=b(z)"
+ congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)"
congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. \
-\ <y1,z1>:r --> <y2,z2>:r --> b y1 y2 = b z1 z2"
+\ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
end
--- a/src/HOL/Integ/Integ.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Integ.ML Fri Mar 24 12:30:35 1995 +0100
@@ -34,20 +34,20 @@
val prems = goalw Integ.thy [intrel_def]
"[| x1+y2 = x2+y1|] ==> \
-\ <<x1,y1>,<x2,y2>>: intrel";
+\ ((x1,y1),(x2,y2)): intrel";
by (fast_tac (rel_cs addIs prems) 1);
qed "intrelI";
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
goalw Integ.thy [intrel_def]
"p: intrel --> (EX x1 y1 x2 y2. \
-\ p = <<x1,y1>,<x2,y2>> & x1+y2 = x2+y1)";
+\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
by (fast_tac rel_cs 1);
qed "intrelE_lemma";
val [major,minor] = goal Integ.thy
"[| p: intrel; \
-\ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1+y2 = x2+y1|] ==> Q |] \
+\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \
\ ==> Q";
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
@@ -55,11 +55,11 @@
val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
-goal Integ.thy "<<x1,y1>,<x2,y2>>: intrel = (x1+y2 = x2+y1)";
+goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
by (fast_tac intrel_cs 1);
qed "intrel_iff";
-goal Integ.thy "<x,x>: intrel";
+goal Integ.thy "(x,x): intrel";
by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
qed "intrel_refl";
@@ -74,7 +74,7 @@
([CollectI, CollectI] MRS
(equiv_intrel RS eq_equiv_class_iff));
-goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{<x,y>}:Integ";
+goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
by (fast_tac set_cs 1);
qed "intrel_in_integ";
@@ -113,7 +113,7 @@
(**** zminus: unary negation on Integ ****)
goalw Integ.thy [congruent_def]
- "congruent intrel (%p. split (%x y. intrel^^{<y,x>}) p)";
+ "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
by (safe_tac intrel_cs);
by (asm_simp_tac (intrel_ss addsimps add_ac) 1);
qed "zminus_congruent";
@@ -123,7 +123,7 @@
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
goalw Integ.thy [zminus_def]
- "$~ Abs_Integ(intrel^^{<x,y>}) = Abs_Integ(intrel ^^ {<y,x>})";
+ "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
by (simp_tac (set_ss addsimps
[intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
@@ -133,7 +133,7 @@
(*by lcp*)
val [prem] = goal Integ.thy
- "(!!x y. z = Abs_Integ(intrel^^{<x,y>}) ==> P) ==> P";
+ "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
@@ -202,7 +202,7 @@
qed "diff_Suc_add_inverse";
goalw Integ.thy [congruent_def]
- "congruent intrel (split (%x y. intrel^^{<(y-x) + (x-(y::nat)),0>}))";
+ "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
by (safe_tac intrel_cs);
by (asm_simp_tac intrel_ss 1);
by (etac rev_mp 1);
@@ -225,8 +225,8 @@
goalw Integ.thy [zmagnitude_def]
- "zmagnitude (Abs_Integ(intrel^^{<x,y>})) = \
-\ Abs_Integ(intrel^^{<(y - x) + (x - y),0>})";
+ "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
+\ Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1);
qed "zmagnitude";
@@ -246,7 +246,7 @@
goalw Integ.thy [congruent2_def]
"congruent2 intrel (%p1 p2. \
-\ split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)";
+\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
(*Proof via congruent2_commuteI seems longer*)
by (safe_tac intrel_cs);
by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
@@ -260,8 +260,8 @@
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
goalw Integ.thy [zadd_def]
- "Abs_Integ(intrel^^{<x1,y1>}) + Abs_Integ(intrel^^{<x2,y2>}) = \
-\ Abs_Integ(intrel^^{<x1+x2, y1+y2>})";
+ "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
+\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
by (asm_simp_tac
(intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1);
qed "zadd";
@@ -333,7 +333,7 @@
goal Integ.thy
"congruent2 intrel (%p1 p2. \
\ split (%x1 y1. split (%x2 y2. \
-\ intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)";
+\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
by (safe_tac intrel_cs);
by (rewtac split_def);
@@ -352,8 +352,8 @@
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
goalw Integ.thy [zmult_def]
- "Abs_Integ((intrel^^{<x1,y1>})) * Abs_Integ((intrel^^{<x2,y2>})) = \
-\ Abs_Integ(intrel ^^ {<x1*x2 + y1*y2, x1*y2 + y1*x2>})";
+ "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \
+\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1);
qed "zmult";
--- a/src/HOL/Integ/Integ.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Integ.thy Fri Mar 24 12:30:35 1995 +0100
@@ -14,7 +14,7 @@
defs
intrel_def
- "intrel == {p. ? x1 y1 x2 y2. p=<<x1::nat,y1>,<x2,y2>> & x1+y2 = x2+y1}"
+ "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
subtype (Integ)
int = "{x::(nat*nat).True}/intrel" ("quotient_def")
@@ -35,21 +35,21 @@
defs
zNat_def "zNat == {x::nat. True}"
- znat_def "$# m == Abs_Integ(intrel ^^ {<m,0>})"
+ znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})"
zminus_def
- "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{<y,x>}) p)"
+ "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
znegative_def
- "znegative(Z) == EX x y. x<y & <x,y::nat>:Rep_Integ(Z)"
+ "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
zmagnitude_def
- "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{<(y-x) + (x-y),0>}) p)"
+ "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
zadd_def
"Z1 + Z2 == \
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \
-\ split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)"
+\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
@@ -60,19 +60,19 @@
zmult_def
"Z1 * Z2 == \
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \
-\ split (%x2 y2. intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)"
+\ split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
zdiv_def
"Z1 zdiv Z2 == \
\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \
-\ split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \
-\ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)"
+\ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \
+\ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
zmod_def
"Z1 zmod Z2 == \
\ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \
-\ split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)), \
-\ (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)"
+\ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), \
+\ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
zsuc_def "zsuc(Z) == Z + $# Suc(0)"
--- a/src/HOL/Integ/Relation.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Relation.ML Fri Mar 24 12:30:35 1995 +0100
@@ -12,18 +12,18 @@
open Relation;
-goalw Relation.thy [converse_def] "!!a b r. <a,b>:r ==> <b,a>:converse(r)";
+goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
by (simp_tac prod_ss 1);
by (fast_tac set_cs 1);
qed "converseI";
-goalw Relation.thy [converse_def] "!!a b r. <a,b> : converse(r) ==> <b,a> : r";
+goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
by (fast_tac comp_cs 1);
qed "converseD";
qed_goalw "converseE" Relation.thy [converse_def]
"[| yx : converse(r); \
-\ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \
+\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \
\ |] ==> P"
(fn [major,minor]=>
[ (rtac (major RS CollectE) 1),
@@ -35,23 +35,23 @@
addSEs [converseD,converseE];
qed_goalw "Domain_iff" Relation.thy [Domain_def]
- "a: Domain(r) = (EX y. <a,y>: r)"
+ "a: Domain(r) = (EX y. (a,y): r)"
(fn _=> [ (fast_tac comp_cs 1) ]);
-qed_goal "DomainI" Relation.thy "!!a b r. <a,b>: r ==> a: Domain(r)"
+qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
(fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
qed_goal "DomainE" Relation.thy
- "[| a : Domain(r); !!y. <a,y>: r ==> P |] ==> P"
+ "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P"
(fn prems=>
[ (rtac (Domain_iff RS iffD1 RS exE) 1),
(REPEAT (ares_tac prems 1)) ]);
-qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.<a,b>: r ==> b : Range(r)"
+qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
(fn _ => [ (etac (converseI RS DomainI) 1) ]);
qed_goalw "RangeE" Relation.thy [Range_def]
- "[| b : Range(r); !!x. <x,b>: r ==> P |] ==> P"
+ "[| b : Range(r); !!x. (x,b): r ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS DomainE) 1),
(resolve_tac prems 1),
@@ -60,23 +60,23 @@
(*** Image of a set under a function/relation ***)
qed_goalw "Image_iff" Relation.thy [Image_def]
- "b : r^^A = (? x:A. <x,b>:r)"
+ "b : r^^A = (? x:A. (x,b):r)"
(fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
qed_goal "Image_singleton_iff" Relation.thy
- "(b : r^^{a}) = (<a,b>:r)"
+ "(b : r^^{a}) = ((a,b):r)"
(fn _ => [ rtac (Image_iff RS trans) 1,
fast_tac comp_cs 1 ]);
qed_goalw "ImageI" Relation.thy [Image_def]
- "!!a b r. [| <a,b>: r; a:A |] ==> b : r^^A"
+ "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A"
(fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
(resolve_tac [conjI ] 1),
(resolve_tac [RangeI] 1),
(REPEAT (fast_tac set_cs 1))]);
qed_goalw "ImageE" Relation.thy [Image_def]
- "[| b: r^^A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P"
+ "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS CollectE) 1),
(safe_tac set_cs),
--- a/src/HOL/Integ/Relation.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Integ/Relation.thy Fri Mar 24 12:30:35 1995 +0100
@@ -16,9 +16,9 @@
Range :: "('a*'a) set => 'a set"
defs
- converse_def "converse(r) == {z. (? w:r. ? x y. w=<x,y> & z=<y,x>)}"
- Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. <x,y>:r))}"
+ converse_def "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}"
+ Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}"
Range_def "Range(r) == Domain(converse(r))"
- Image_def "r ^^ s == {y. y:Range(r) & (? x:s. <x,y>:r)}"
+ Image_def "r ^^ s == {y. y:Range(r) & (? x:s. (x,y):r)}"
end
--- a/src/HOL/Nat.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Nat.ML Fri Mar 24 12:30:35 1995 +0100
@@ -136,12 +136,12 @@
(** Introduction rules for 'pred_nat' **)
-goalw Nat.thy [pred_nat_def] "<n, Suc(n)> : pred_nat";
+goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
by (fast_tac set_cs 1);
qed "pred_natI";
val major::prems = goalw Nat.thy [pred_nat_def]
- "[| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R \
+ "[| p : pred_nat; !!x n. [| p = (n, Suc(n)) |] ==> R \
\ |] ==> R";
by (rtac (major RS CollectE) 1);
by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
@@ -204,7 +204,7 @@
by (rtac (pred_natI RS r_into_trancl) 1);
qed "lessI";
-(* i<j ==> i<Suc(j) *)
+(* i(j ==> i(Suc(j) *)
val less_SucI = lessI RSN (2, less_trans);
goal Nat.thy "0 < Suc(n)";
@@ -220,7 +220,7 @@
by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
qed "less_not_sym";
-(* [| n<m; m<n |] ==> R *)
+(* [| n(m; m(n |] ==> R *)
bind_thm ("less_asym", (less_not_sym RS notE));
goalw Nat.thy [less_def] "~ n<(n::nat)";
@@ -228,7 +228,7 @@
by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
qed "less_not_refl";
-(* n<n ==> R *)
+(* n(n ==> R *)
bind_thm ("less_anti_refl", (less_not_refl RS notE));
goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
--- a/src/HOL/Nat.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Nat.thy Fri Mar 24 12:30:35 1995 +0100
@@ -59,9 +59,9 @@
(*nat operations and recursion*)
nat_case_def "nat_case a f n == @z. (n=0 --> z=a) \
\ & (!x. n=Suc(x) --> z=f(x))"
- pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
+ pred_nat_def "pred_nat == {p. ? n. p = (n, Suc(n))}"
- less_def "m<n == <m,n>:trancl(pred_nat)"
+ less_def "m<n == (m,n):trancl(pred_nat)"
le_def "m<=(n::nat) == ~(n<m)"
--- a/src/HOL/Prod.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Prod.ML Fri Mar 24 12:30:35 1995 +0100
@@ -25,35 +25,35 @@
qed "inj_onto_Abs_Prod";
val prems = goalw Prod.thy [Pair_def]
- "[| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R";
+ "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R";
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
by (REPEAT (ares_tac (prems@[ProdI]) 1));
qed "Pair_inject";
-goal Prod.thy "(<a,b> = <a',b'>) = (a=a' & b=b')";
+goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
by (fast_tac (set_cs addIs [Pair_inject]) 1);
qed "Pair_eq";
-goalw Prod.thy [fst_def] "fst(<a,b>) = a";
+goalw Prod.thy [fst_def] "fst((a,b)) = a";
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
qed "fst_conv";
-goalw Prod.thy [snd_def] "snd(<a,b>) = b";
+goalw Prod.thy [snd_def] "snd((a,b)) = b";
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
qed "snd_conv";
-goalw Prod.thy [Pair_def] "? x y. p = <x,y>";
+goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]);
qed "PairE_lemma";
-val [prem] = goal Prod.thy "[| !!x y. p = <x,y> ==> Q |] ==> Q";
+val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
by (rtac (PairE_lemma RS exE) 1);
by (REPEAT (eresolve_tac [prem,exE] 1));
qed "PairE";
-goalw Prod.thy [split_def] "split c <a,b> = c a b";
+goalw Prod.thy [split_def] "split c (a,b) = c a b";
by (sstac [fst_conv, snd_conv] 1);
by (rtac refl 1);
qed "split";
@@ -72,18 +72,18 @@
(fn [prem] => [rtac (prem RS arg_cong) 1]);
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
-goal Prod.thy "p = <fst(p),snd(p)>";
+goal Prod.thy "p = (fst(p),snd(p))";
by (res_inst_tac [("p","p")] PairE 1);
by (asm_simp_tac prod_ss 1);
qed "surjective_pairing";
-goal Prod.thy "p = split (%x y.<x,y>) p";
+goal Prod.thy "p = split (%x y.(x,y)) p";
by (res_inst_tac [("p","p")] PairE 1);
by (asm_simp_tac prod_ss 1);
qed "surjective_pairing2";
(*For use with split_tac and the simplifier*)
-goal Prod.thy "R(split c p) = (! x y. p = <x,y> --> R(c x y))";
+goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
by (stac surjective_pairing 1);
by (stac split 1);
by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
@@ -94,31 +94,31 @@
(*These rules are for use with fast_tac.
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
-goal Prod.thy "!!a b c. c a b ==> split c <a,b>";
+goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
by (asm_simp_tac prod_ss 1);
qed "splitI";
val prems = goalw Prod.thy [split_def]
- "[| split c p; !!x y. [| p = <x,y>; c x y |] ==> Q |] ==> Q";
+ "[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "splitE";
-goal Prod.thy "!!R a b. split R <a,b> ==> R a b";
+goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
by (etac (split RS iffD1) 1);
qed "splitD";
-goal Prod.thy "!!a b c. z: c a b ==> z: split c <a,b>";
+goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
by (asm_simp_tac prod_ss 1);
qed "mem_splitI";
val prems = goalw Prod.thy [split_def]
- "[| z: split c p; !!x y. [| p = <x,y>; z: c x y |] ==> Q |] ==> Q";
+ "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "mem_splitE";
(*** prod_fun -- action of the product functor upon functions ***)
-goalw Prod.thy [prod_fun_def] "prod_fun f g <a,b> = <f(a),g(b)>";
+goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
by (rtac split 1);
qed "prod_fun";
@@ -135,14 +135,14 @@
by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1);
qed "prod_fun_ident";
-val prems = goal Prod.thy "<a,b>:r ==> <f(a),g(b)> : (prod_fun f g)``r";
+val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
by (rtac image_eqI 1);
by (rtac (prod_fun RS sym) 1);
by (resolve_tac prems 1);
qed "prod_fun_imageI";
val major::prems = goal Prod.thy
- "[| c: (prod_fun f g)``r; !!x y. [| c=<f(x),g(y)>; <x,y>:r |] ==> P \
+ "[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
\ |] ==> P";
by (rtac (major RS imageE) 1);
by (res_inst_tac [("p","x")] PairE 1);
@@ -154,31 +154,31 @@
(*** Disjoint union of a family of sets - Sigma ***)
qed_goalw "SigmaI" Prod.thy [Sigma_def]
- "[| a:A; b:B(a) |] ==> <a,b> : Sigma A B"
+ "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
(*The general elimination rule*)
qed_goalw "SigmaE" Prod.thy [Sigma_def]
"[| c: Sigma A B; \
-\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
+\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \
\ |] ==> P"
(fn major::prems=>
[ (cut_facts_tac [major] 1),
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
-(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
-qed_goal "SigmaD1" Prod.thy "<a,b> : Sigma A B ==> a : A"
+(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
+qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
(fn [major]=>
[ (rtac (major RS SigmaE) 1),
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
-qed_goal "SigmaD2" Prod.thy "<a,b> : Sigma A B ==> b : B(a)"
+qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
(fn [major]=>
[ (rtac (major RS SigmaE) 1),
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
qed_goal "SigmaE2" Prod.thy
- "[| <a,b> : Sigma A B; \
+ "[| (a,b) : Sigma A B; \
\ [| a:A; b:B(a) |] ==> P \
\ |] ==> P"
(fn [major,minor]=>
@@ -188,7 +188,7 @@
(*** Domain of a relation ***)
-val prems = goalw Prod.thy [image_def] "<a,b> : r ==> a : fst``r";
+val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
by (rtac CollectI 1);
by (rtac bexI 1);
by (rtac (fst_conv RS sym) 1);
@@ -196,7 +196,7 @@
qed "fst_imageI";
val major::prems = goal Prod.thy
- "[| a : fst``r; !!y.[| <a,y> : r |] ==> P |] ==> P";
+ "[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (resolve_tac prems 1);
by (etac ssubst 1);
@@ -206,7 +206,7 @@
(*** Range of a relation ***)
-val prems = goalw Prod.thy [image_def] "<a,b> : r ==> b : snd``r";
+val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
by (rtac CollectI 1);
by (rtac bexI 1);
by (rtac (snd_conv RS sym) 1);
@@ -214,7 +214,7 @@
qed "snd_imageI";
val major::prems = goal Prod.thy
- "[| a : snd``r; !!y.[| <y,a> : r |] ==> P |] ==> P";
+ "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (resolve_tac prems 1);
by (etac ssubst 1);
@@ -225,7 +225,7 @@
(** Exhaustion rule for unit -- a degenerate form of induction **)
goalw Prod.thy [Unity_def]
- "u = Unity";
+ "u = ()";
by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
by (rtac (Rep_Unit_inverse RS sym) 1);
qed "unit_eq";
--- a/src/HOL/Prod.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Prod.thy Fri Mar 24 12:30:35 1995 +0100
@@ -35,20 +35,19 @@
Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set"
syntax
- "@Tuple" :: "args => 'a * 'b" ("(1<_>)")
+ "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
translations
- "<x, y, z>" == "<x, <y, z>>"
- "<x, y>" == "Pair x y"
- "<x>" => "x"
+ "(x, y, z)" == "(x, (y, z))"
+ "(x, y)" == "Pair x y"
defs
Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
- fst_def "fst(p) == @a. ? b. p = <a, b>"
- snd_def "snd(p) == @b. ? a. p = <a, b>"
+ fst_def "fst(p) == @a. ? b. p = (a, b)"
+ snd_def "snd(p) == @b. ? a. p = (a, b)"
split_def "split c p == c (fst p) (snd p)"
- prod_fun_def "prod_fun f g == split(%x y.<f(x), g(y)>)"
- Sigma_def "Sigma A B == UN x:A. UN y:B(x). {<x, y>}"
+ prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))"
+ Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
@@ -58,9 +57,9 @@
unit = "{p. p = True}"
consts
- Unity :: "unit" ("'(')")
+ "()" :: "unit" ("'(')")
defs
- Unity_def "Unity == Abs_Unit(True)"
+ Unity_def "() == Abs_Unit(True)"
end
--- a/src/HOL/Sexp.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Sexp.ML Fri Mar 24 12:30:35 1995 +0100
@@ -63,19 +63,19 @@
by (fast_tac sexp_cs 1);
qed "pred_sexp_subset_Sigma";
-(* <a,b> : pred_sexp^+ ==> a : sexp *)
+(* (a,b) : pred_sexp^+ ==> a : sexp *)
val trancl_pred_sexpD1 =
pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
and trancl_pred_sexpD2 =
pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
val prems = goalw Sexp.thy [pred_sexp_def]
- "[| M: sexp; N: sexp |] ==> <M, M$N> : pred_sexp";
+ "[| M: sexp; N: sexp |] ==> (M, M$N) : pred_sexp";
by (fast_tac (set_cs addIs prems) 1);
qed "pred_sexpI1";
val prems = goalw Sexp.thy [pred_sexp_def]
- "[| M: sexp; N: sexp |] ==> <N, M$N> : pred_sexp";
+ "[| M: sexp; N: sexp |] ==> (N, M$N) : pred_sexp";
by (fast_tac (set_cs addIs prems) 1);
qed "pred_sexpI2";
@@ -86,7 +86,7 @@
val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
-(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
+(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
val pred_sexp_simps =
sexp.intrs @
[pred_sexp_t1, pred_sexp_t2,
@@ -95,8 +95,8 @@
val major::prems = goalw Sexp.thy [pred_sexp_def]
"[| p : pred_sexp; \
-\ !!M N. [| p = <M, M$N>; M: sexp; N: sexp |] ==> R; \
-\ !!M N. [| p = <N, M$N>; M: sexp; N: sexp |] ==> R \
+\ !!M N. [| p = (M, M$N); M: sexp; N: sexp |] ==> R; \
+\ !!M N. [| p = (N, M$N); M: sexp; N: sexp |] ==> R \
\ |] ==> R";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
--- a/src/HOL/Sexp.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Sexp.thy Fri Mar 24 12:30:35 1995 +0100
@@ -32,7 +32,7 @@
\ | (? N1 N2. M = N1 $ N2 & z=e N1 N2)"
pred_sexp_def
- "pred_sexp == UN M: sexp. UN N: sexp. {<M, M$N>, <N, M$N>}"
+ "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
sexp_rec_def
"sexp_rec M c d e == wfrec pred_sexp M \
--- a/src/HOL/Subst/AList.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Subst/AList.ML Fri Mar 24 12:30:35 1995 +0100
@@ -12,13 +12,13 @@
(fn _ => [simp_tac list_ss 1])
in map mk_thm
["alist_rec [] c d = c",
- "alist_rec (<a,b>#al) c d = d a b al (alist_rec al c d)",
+ "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
"assoc v d [] = d",
- "assoc v d (<a,b>#al) = (if v=a then b else assoc v d al)"] end;
+ "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end;
val prems = goal AList.thy
"[| P([]); \
-\ !!x y xs. P(xs) ==> P(<x,y>#xs) |] ==> P(l)";
+\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)";
by (list.induct_tac "l" 1);
by (resolve_tac prems 1);
by (rtac PairE 1);
--- a/src/HOL/Subst/Subst.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Subst/Subst.ML Fri Mar 24 12:30:35 1995 +0100
@@ -19,9 +19,9 @@
["Const(c) <| al = Const(c)",
"Comb t u <| al = Comb (t <| al) (u <| al)",
"[] <> bl = bl",
- "(<a,b>#al) <> bl = <a,b <| bl> # (al <> bl)",
+ "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
"sdom([]) = {}",
- "sdom(<a,b>#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
+ "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
\ else (sdom al) Un {a})"
];
(* This rewrite isn't always desired *)
@@ -42,10 +42,10 @@
by (ALLGOALS (asm_simp_tac subst_ss));
val subst_mono = store_thm("subst_mono", result() RS mp);
-goal Subst.thy "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
+goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s";
by (imp_excluded_middle_tac "t = Var(v)" 1);
by (res_inst_tac [("P",
- "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
+ "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
uterm_induct 2);
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
by (fast_tac HOL_cs 1);
@@ -59,13 +59,13 @@
by (ALLGOALS (fast_tac HOL_cs));
qed "agreement";
-goal Subst.thy "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
+goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
by(simp_tac(subst_ss addsimps [agreement,Var_subst]
setloop (split_tac [expand_if])) 1);
val repl_invariance = store_thm("repl_invariance", result() RS mp);
val asms = goal Subst.thy
- "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
+ "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
by (uterm_ind_tac "t" 1);
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
val Var_in_subst = store_thm("Var_in_subst", result() RS mp);
@@ -113,7 +113,7 @@
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
qed "comp_assoc";
-goal Subst.thy "<w,Var(w) <| s>#s =s= s";
+goal Subst.thy "(w,Var(w) <| s)#s =s= s";
by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
by (uterm_ind_tac "t" 1);
by (REPEAT (etac rev_mp 3));
--- a/src/HOL/Subst/Subst.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Subst/Subst.thy Fri Mar 24 12:30:35 1995 +0100
@@ -26,7 +26,7 @@
\ (%x.Const(x)) \
\ (%u v q r.Comb q r)"
- comp_def "al <> bl == alist_rec al bl (%x y xs g.<x,y <| bl>#g)"
+ comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
sdom_def
"sdom(al) == alist_rec al {} \
--- a/src/HOL/Subst/Unifier.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Subst/Unifier.ML Fri Mar 24 12:30:35 1995 +0100
@@ -25,7 +25,7 @@
goal Unifier.thy
"~v : vars_of(t) --> ~v : vars_of(u) -->Unifier s t u --> \
-\ Unifier (<v,r>#s) t u";
+\ Unifier ((v,r)#s) t u";
by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
val Cons_Unifier = store_thm("Cons_Unifier", result() RS mp RS mp RS mp);
@@ -49,7 +49,7 @@
qed "MGU_iff";
val [prem] = goal Unifier.thy
- "~ Var(v) <: t ==> MGUnifier [<v,t>] (Var v) t";
+ "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t";
by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
by (REPEAT_SOME (step_tac set_cs));
by (etac subst 1);
@@ -85,7 +85,7 @@
by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
qed "Idem_Nil";
-goal Unifier.thy "~ (Var(v) <: t) --> Idem([<v,t>])";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
setloop (split_tac [expand_if])) 1);
by (fast_tac set_cs 1);
@@ -114,8 +114,8 @@
val prems = goal Unifier.thy
"x : sdom(s) --> ~x : srange(s) --> \
-\ ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
-\ vars_of(Var(x) <| <x,Var(x)>#s)";
+\ ~vars_of(Var(x) <| s<> (x,Var(x))#s) = \
+\ vars_of(Var(x) <| (x,Var(x))#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI2] 1));
by(res_inst_tac [("x","x")] exI 1);
@@ -141,8 +141,8 @@
val prems = goal Unifier.thy
"~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\ ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
-\ vars_of(Var(w) <| <x,Var(w)>#s)";
+\ ~vars_of(Var(w) <| s<> (x,Var(w))#s) = \
+\ vars_of(Var(w) <| (x,Var(w))#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI1] 1));
by(res_inst_tac [("x","w")] exI 1);
@@ -167,10 +167,10 @@
(* *)
(* fun unify Const(m) Const(n) = if m=n then Nil else Fail *)
(* | unify Const(m) _ = Fail *)
-(* | unify Var(v) t = if Var(v)<:t then Fail else <v,t>#Nil *)
+(* | unify Var(v) t = if Var(v)<:t then Fail else (v,t)#Nil *)
(* | unify Comb(t,u) Const(n) = Fail *)
(* | unify Comb(t,u) Var(v) = if Var(v) <: Comb(t,u) then Fail *)
-(* else <v,Comb(t,u>#Nil *)
+(* else (v,Comb(t,u)#Nil *)
(* | unify Comb(t,u) Comb(v,w) = let s = unify t v *)
(* in if s=Fail then Fail *)
(* else unify (u<|s) (w<|s); *)
@@ -191,7 +191,7 @@
val Unify2 = store_thm("Unify2", result() RS mp);
val [prem] = goalw Unifier.thy [MGIUnifier_def]
- "~Var(v) <: t ==> MGIUnifier [<v,t>] (Var v) t";
+ "~Var(v) <: t ==> MGIUnifier [(v,t)] (Var v) t";
by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
qed "Unify3";
--- a/src/HOL/Trancl.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Trancl.ML Fri Mar 24 12:30:35 1995 +0100
@@ -11,55 +11,55 @@
(** Natural deduction for trans(r) **)
val prems = goalw Trancl.thy [trans_def]
- "(!! x y z. [| <x,y>:r; <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
+ "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)";
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
qed "transI";
val major::prems = goalw Trancl.thy [trans_def]
- "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
+ "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
by (cut_facts_tac [major] 1);
by (fast_tac (HOL_cs addIs prems) 1);
qed "transD";
(** Identity relation **)
-goalw Trancl.thy [id_def] "<a,a> : id";
+goalw Trancl.thy [id_def] "(a,a) : id";
by (rtac CollectI 1);
by (rtac exI 1);
by (rtac refl 1);
qed "idI";
val major::prems = goalw Trancl.thy [id_def]
- "[| p: id; !!x.[| p = <x,x> |] ==> P \
+ "[| p: id; !!x.[| p = (x,x) |] ==> P \
\ |] ==> P";
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (eresolve_tac prems 1);
qed "idE";
-goalw Trancl.thy [id_def] "<a,b>:id = (a=b)";
+goalw Trancl.thy [id_def] "(a,b):id = (a=b)";
by(fast_tac prod_cs 1);
qed "pair_in_id_conv";
(** Composition of two relations **)
val prems = goalw Trancl.thy [comp_def]
- "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
+ "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
by (fast_tac (set_cs addIs prems) 1);
qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
val prems = goalw Trancl.thy [comp_def]
"[| xz : r O s; \
-\ !!x y z. [| xz = <x,z>; <x,y>:s; <y,z>:r |] ==> P \
+\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \
\ |] ==> P";
by (cut_facts_tac prems 1);
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
qed "compE";
val prems = goal Trancl.thy
- "[| <a,c> : r O s; \
-\ !!y. [| <a,y>:s; <y,c>:r |] ==> P \
+ "[| (a,c) : r O s; \
+\ !!y. [| (a,y):s; (y,c):r |] ==> P \
\ |] ==> P";
by (rtac compE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
@@ -88,20 +88,20 @@
val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
(*Reflexivity of rtrancl*)
-goal Trancl.thy "<a,a> : r^*";
+goal Trancl.thy "(a,a) : r^*";
by (stac rtrancl_unfold 1);
by (fast_tac comp_cs 1);
qed "rtrancl_refl";
(*Closure under composition with r*)
val prems = goal Trancl.thy
- "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
+ "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*";
by (stac rtrancl_unfold 1);
by (fast_tac (comp_cs addIs prems) 1);
qed "rtrancl_into_rtrancl";
(*rtrancl of r contains r*)
-val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
+val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*";
by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
by (rtac prem 1);
qed "r_into_rtrancl";
@@ -114,22 +114,22 @@
(** standard induction rule **)
val major::prems = goal Trancl.thy
- "[| <a,b> : r^*; \
-\ !!x. P(<x,x>); \
-\ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
-\ ==> P(<a,b>)";
+ "[| (a,b) : r^*; \
+\ !!x. P((x,x)); \
+\ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \
+\ ==> P((a,b))";
by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
by (fast_tac (comp_cs addIs prems) 1);
qed "rtrancl_full_induct";
(*nice induction rule*)
val major::prems = goal Trancl.thy
- "[| <a::'a,b> : r^*; \
+ "[| (a::'a,b) : r^*; \
\ P(a); \
-\ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |] \
+\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \
\ ==> P(b)";
(*by induction on this formula*)
-by (subgoal_tac "! y. <a::'a,b> = <a,y> --> P(y)" 1);
+by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
(*now solve first subgoal: this formula is sufficient*)
by (fast_tac HOL_cs 1);
(*now do the induction*)
@@ -147,10 +147,10 @@
(*elimination of rtrancl -- by induction on a special formula*)
val major::prems = goal Trancl.thy
- "[| <a::'a,b> : r^*; (a = b) ==> P; \
-\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P \
+ "[| (a::'a,b) : r^*; (a = b) ==> P; \
+\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \
\ |] ==> P";
-by (subgoal_tac "(a::'a) = b | (? y. <a,y> : r^* & <y,b> : r)" 1);
+by (subgoal_tac "(a::'a) = b | (? y. (a,y) : r^* & (y,b) : r)" 1);
by (rtac (major RS rtrancl_induct) 2);
by (fast_tac (set_cs addIs prems) 2);
by (fast_tac (set_cs addIs prems) 2);
@@ -163,26 +163,26 @@
(** Conversions between trancl and rtrancl **)
val [major] = goalw Trancl.thy [trancl_def]
- "<a,b> : r^+ ==> <a,b> : r^*";
+ "(a,b) : r^+ ==> (a,b) : r^*";
by (resolve_tac [major RS compEpair] 1);
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
qed "trancl_into_rtrancl";
(*r^+ contains r*)
val [prem] = goalw Trancl.thy [trancl_def]
- "[| <a,b> : r |] ==> <a,b> : r^+";
+ "[| (a,b) : r |] ==> (a,b) : r^+";
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
qed "r_into_trancl";
(*intro rule by definition: from rtrancl and r*)
val prems = goalw Trancl.thy [trancl_def]
- "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
+ "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^+";
by (REPEAT (resolve_tac ([compI]@prems) 1));
qed "rtrancl_into_trancl1";
(*intro rule from r and rtrancl*)
val prems = goal Trancl.thy
- "[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+";
+ "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+";
by (resolve_tac (prems RL [rtranclE]) 1);
by (etac subst 1);
by (resolve_tac (prems RL [r_into_trancl]) 1);
@@ -192,11 +192,11 @@
(*elimination of r^+ -- NOT an induction rule*)
val major::prems = goal Trancl.thy
- "[| <a::'a,b> : r^+; \
-\ <a,b> : r ==> P; \
-\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
+ "[| (a::'a,b) : r^+; \
+\ (a,b) : r ==> P; \
+\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \
\ |] ==> P";
-by (subgoal_tac "<a::'a,b> : r | (? y. <a,y> : r^+ & <y,b> : r)" 1);
+by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+ & (y,b) : r)" 1);
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
by (etac rtranclE 1);
@@ -214,7 +214,7 @@
qed "trans_trancl";
val prems = goal Trancl.thy
- "[| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+";
+ "[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
@@ -222,7 +222,7 @@
val major::prems = goal Trancl.thy
- "[| <a,b> : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A";
+ "[| (a,b) : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A";
by (cut_facts_tac prems 1);
by (rtac (major RS rtrancl_induct) 1);
by (rtac (refl RS disjI1) 1);
--- a/src/HOL/Trancl.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Trancl.thy Fri Mar 24 12:30:35 1995 +0100
@@ -16,11 +16,11 @@
trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
defs
-trans_def "trans(r) == (!x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
comp_def (*composition of relations*)
- "r O s == {xz. ? x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+ "r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}"
id_def (*the identity relation*)
- "id == {p. ? x. p = <x,x>}"
+ "id == {p. ? x. p = (x,x)}"
rtrancl_def "r^* == lfp(%s. id Un (r O s))"
trancl_def "r^+ == r O rtrancl(r)"
end
--- a/src/HOL/Univ.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Univ.ML Fri Mar 24 12:30:35 1995 +0100
@@ -51,12 +51,12 @@
(** apfst -- can be used in similar type definitions **)
-goalw Univ.thy [apfst_def] "apfst f <a,b> = <f(a),b>";
+goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
by (rtac split 1);
qed "apfst";
val [major,minor] = goal Univ.thy
- "[| q = apfst f p; !!x y. [| p = <x,y>; q = <f(x),y> |] ==> R \
+ "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \
\ |] ==> R";
by (rtac PairE 1);
by (rtac minor 1);
@@ -109,7 +109,7 @@
(*** Introduction rules for Node ***)
-goalw Univ.thy [Node_def] "<%k. 0,a> : Node";
+goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
by (fast_tac set_cs 1);
qed "Node_K0_I";
@@ -256,7 +256,7 @@
val univ_ss = nat_ss addsimps univ_simps;
-goalw Univ.thy [ndepth_def] "ndepth (Abs_Node(<%k.0, x>)) = 0";
+goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1);
by (rtac Least_equality 1);
by (rtac refl 1);
@@ -496,7 +496,7 @@
(*** Equality : the diagonal relation ***)
-goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> <a,b> : diag(A)";
+goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> (a,b) : diag(A)";
by (fast_tac set_cs 1);
qed "diag_eqI";
@@ -505,7 +505,7 @@
(*The general elimination rule*)
val major::prems = goalw Univ.thy [diag_def]
"[| c : diag(A); \
-\ !!x y. [| x:A; c = <x,x> |] ==> P \
+\ !!x y. [| x:A; c = (x,x) |] ==> P \
\ |] ==> P";
by (rtac (major RS UN_E) 1);
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
@@ -514,14 +514,14 @@
(*** Equality for Cartesian Product ***)
goalw Univ.thy [dprod_def]
- "!!r s. [| <M,M'>:r; <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
+ "!!r s. [| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
by (fast_tac prod_cs 1);
qed "dprodI";
(*The general elimination rule*)
val major::prems = goalw Univ.thy [dprod_def]
"[| c : r<**>s; \
-\ !!x y x' y'. [| <x,x'> : r; <y,y'> : s; c = <x$y,x'$y'> |] ==> P \
+\ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (x$y,x'$y') |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
@@ -531,18 +531,18 @@
(*** Equality for Disjoint Sum ***)
-goalw Univ.thy [dsum_def] "!!r. <M,M'>:r ==> <In0(M), In0(M')> : r<++>s";
+goalw Univ.thy [dsum_def] "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
by (fast_tac prod_cs 1);
qed "dsum_In0I";
-goalw Univ.thy [dsum_def] "!!r. <N,N'>:s ==> <In1(N), In1(N')> : r<++>s";
+goalw Univ.thy [dsum_def] "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
by (fast_tac prod_cs 1);
qed "dsum_In1I";
val major::prems = goalw Univ.thy [dsum_def]
"[| w : r<++>s; \
-\ !!x x'. [| <x,x'> : r; w = <In0(x), In0(x')> |] ==> P; \
-\ !!y y'. [| <y,y'> : s; w = <In1(y), In1(y')> |] ==> P \
+\ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \
+\ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
--- a/src/HOL/Univ.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Univ.thy Fri Mar 24 12:30:35 1995 +0100
@@ -16,7 +16,7 @@
(** lists, trees will be sets of nodes **)
subtype (Node)
- 'a node = "{p. EX f x k. p = <f::nat=>nat, x::'a+nat> & f(k)=0}"
+ 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
types
'a item = "'a node set"
@@ -58,13 +58,13 @@
Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
(*crude "lists" of nats -- needed for the constructions*)
- apfst_def "apfst == (%f. split(%x y. <f(x),y>))"
+ apfst_def "apfst == (%f. split(%x y. (f(x),y)))"
Push_def "Push == (%b h. nat_case (Suc b) h)"
(** operations on S-expressions -- sets of nodes **)
(*S-expression constructors*)
- Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})"
+ Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})"
Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
(*Leaf nodes, with arbitrary or nat labels*)
@@ -92,12 +92,12 @@
(** diagonal sets and equality for the "universe" **)
- diag_def "diag(A) == UN x:A. {<x,x>}"
+ diag_def "diag(A) == UN x:A. {(x,x)}"
dprod_def "r<**>s == UN u:r. split (%x x'. \
-\ UN v:s. split (%y y'. {<x$y,x'$y'>}) v) u"
+\ UN v:s. split (%y y'. {(x$y,x'$y')}) v) u"
- dsum_def "r<++>s == (UN u:r. split (%x x'. {<In0(x),In0(x')>}) u) Un \
-\ (UN v:s. split (%y y'. {<In1(y),In1(y')>}) v)"
+ dsum_def "r<++>s == (UN u:r. split (%x x'. {(In0(x),In0(x'))}) u) Un \
+\ (UN v:s. split (%y y'. {(In1(y),In1(y'))}) v)"
end
--- a/src/HOL/WF.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/WF.ML Fri Mar 24 12:30:35 1995 +0100
@@ -14,7 +14,7 @@
(*Restriction to domain A. If r is well-founded over A then wf(r)*)
val [prem1,prem2] = goalw WF.thy [wf_def]
"[| r <= Sigma A (%u.A); \
-\ !!x P. [| ! x. (! y. <y,x> : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
+\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
\ ==> wf(r)";
by (strip_tac 1);
by (rtac allE 1);
@@ -24,7 +24,7 @@
val major::prems = goalw WF.thy [wf_def]
"[| wf(r); \
-\ !!x.[| ! y. <y,x>: r --> P(y) |] ==> P(x) \
+\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
by (rtac (major RS spec RS mp RS spec) 1);
by (fast_tac (HOL_cs addEs prems) 1);
@@ -36,14 +36,14 @@
rename_last_tac a ["1"] (i+1),
ares_tac prems i];
-val prems = goal WF.thy "[| wf(r); <a,x>:r; <x,a>:r |] ==> P";
-by (subgoal_tac "! x. <a,x>:r --> <x,a>:r --> P" 1);
+val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P";
+by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
by (fast_tac (HOL_cs addIs prems) 1);
by (wf_ind_tac "a" prems 1);
by (fast_tac set_cs 1);
qed "wf_asym";
-val prems = goal WF.thy "[| wf(r); <a,a>: r |] ==> P";
+val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P";
by (rtac wf_asym 1);
by (REPEAT (resolve_tac prems 1));
qed "wf_anti_refl";
@@ -68,12 +68,12 @@
(*This rewrite rule works upon formulae; thus it requires explicit use of
H_cong to expose the equality*)
goalw WF.thy [cut_def]
- "(cut f r x = cut g r x) = (!y. <y,x>:r --> f(y)=g(y))";
+ "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
by(simp_tac (HOL_ss addsimps [expand_fun_eq]
setloop (split_tac [expand_if])) 1);
qed "cut_cut_eq";
-goalw WF.thy [cut_def] "!!x. <x,a>:r ==> (cut f r a)(x) = f(x)";
+goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
by(asm_simp_tac HOL_ss 1);
qed "cut_apply";
@@ -81,12 +81,12 @@
(*** is_recfun ***)
goalw WF.thy [is_recfun_def,cut_def]
- "!!f. [| is_recfun r a H f; ~<b,a>:r |] ==> f(b) = (@z.True)";
+ "!!f. [| is_recfun r a H f; ~(b,a):r |] ==> f(b) = (@z.True)";
by (etac ssubst 1);
by(asm_simp_tac HOL_ss 1);
qed "is_recfun_undef";
-(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
+(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
mp amd allE instantiate induction hypotheses*)
fun indhyp_tac hyps =
ares_tac (TrueI::hyps) ORELSE'
@@ -104,7 +104,7 @@
val prems = goalw WF.thy [is_recfun_def,cut_def]
"[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \
- \ <x,a>:r --> <x,b>:r --> f(x)=g(x)";
+ \ (x,a):r --> (x,b):r --> f(x)=g(x)";
by (cut_facts_tac prems 1);
by (etac wf_induct 1);
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
@@ -115,7 +115,7 @@
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
"[| wf(r); trans(r); \
-\ is_recfun r a H f; is_recfun r b H g; <b,a>:r |] ==> \
+\ is_recfun r a H f; is_recfun r b H g; (b,a):r |] ==> \
\ cut f r b = g";
val gundef = recgb RS is_recfun_undef
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
@@ -150,13 +150,13 @@
(*Beware incompleteness of unification!*)
val prems = goal WF.thy
- "[| wf(r); trans(r); <c,a>:r; <c,b>:r |] \
+ "[| wf(r); trans(r); (c,a):r; (c,b):r |] \
\ ==> the_recfun r a H c = the_recfun r b H c";
by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
qed "the_recfun_equal";
val prems = goal WF.thy
- "[| wf(r); trans(r); <b,a>:r |] \
+ "[| wf(r); trans(r); (b,a):r |] \
\ ==> cut (the_recfun r a H) r b = the_recfun r b H";
by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
qed "the_recfun_cut";
--- a/src/HOL/WF.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/WF.thy Fri Mar 24 12:30:35 1995 +0100
@@ -15,9 +15,9 @@
the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
defs
- wf_def "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
+ wf_def "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
- cut_def "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
+ cut_def "cut f r x == (%y. if (y,x):r then f y else @z.True)"
is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
--- a/src/HOL/ex/Acc.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/Acc.ML Fri Mar 24 12:30:35 1995 +0100
@@ -13,12 +13,12 @@
(*The intended introduction rule*)
val prems = goal Acc.thy
- "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)";
+ "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
by (fast_tac (set_cs addIs (prems @
map (rewrite_rule [pred_def]) acc.intrs)) 1);
qed "accI";
-goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
+goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)";
by (etac acc.elim 1);
by (rewtac pred_def);
by (fast_tac set_cs 1);
@@ -26,7 +26,7 @@
val [major,indhyp] = goal Acc.thy
"[| a : acc(r); \
-\ !!x. [| x: acc(r); ALL y. <y,x>:r --> P(y) |] ==> P(x) \
+\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
by (rtac (major RS acc.induct) 1);
by (rtac indhyp 1);
@@ -44,7 +44,7 @@
by (fast_tac set_cs 1);
qed "acc_wfI";
-val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
+val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
by (rtac (major RS wf_induct) 1);
br (impI RS allI) 1;
br accI 1;
--- a/src/HOL/ex/Acc.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/Acc.thy Fri Mar 24 12:30:35 1995 +0100
@@ -16,7 +16,7 @@
acc :: "('a * 'a)set => 'a set" (*Accessible part*)
defs
- pred_def "pred x r == {y. <y,x>:r}"
+ pred_def "pred x r == {y. (y,x):r}"
inductive "acc(r)"
intrs
--- a/src/HOL/ex/LList.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/LList.ML Fri Mar 24 12:30:35 1995 +0100
@@ -135,7 +135,7 @@
(*Lemma for the proof of llist_corec*)
goal LList.thy
- "LList_corec a (%z.sum_case Inl (split(%v w.Inr(<Leaf(v),w>))) (f z)) : \
+ "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
\ llist(range(Leaf))";
by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
@@ -156,7 +156,7 @@
end;
qed "LListD_unfold";
-goal LList.thy "!M N. <M,N> : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
+goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
by (res_inst_tac [("n", "k")] less_induct 1);
by (safe_tac set_cs);
by (etac LListD.elim 1);
@@ -202,12 +202,12 @@
ba 1;
qed "LListD_coinduct";
-goalw LList.thy [LListD_Fun_def,NIL_def] "<NIL,NIL> : LListD_Fun r s";
+goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
by (fast_tac set_cs 1);
qed "LListD_Fun_NIL_I";
goalw LList.thy [LListD_Fun_def,CONS_def]
- "!!x. [| x:A; <M,N>:s |] ==> <CONS x M, CONS x N> : LListD_Fun (diag A) s";
+ "!!x. [| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
by (fast_tac univ_cs 1);
qed "LListD_Fun_CONS_I";
@@ -237,7 +237,7 @@
qed "LListD_eq_diag";
goal LList.thy
- "!!M N. M: llist(A) ==> <M,M> : LListD_Fun (diag A) (X Un diag(llist(A)))";
+ "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
by (rtac (LListD_eq_diag RS subst) 1);
br LListD_Fun_LListD_I 1;
by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1);
@@ -248,7 +248,7 @@
[also admits true equality]
Replace "A" by some particular set, like {x.True}??? *)
goal LList.thy
- "!!r. [| <M,N> : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
+ "!!r. [| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
\ |] ==> M=N";
by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
by (etac LListD_coinduct 1);
@@ -267,7 +267,7 @@
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
by (res_inst_tac [("A", "{u.True}"),
- ("r", "range(%u. <h1(u),h2(u)>)")] LList_equalityI 1);
+ ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
by (stac prem1 1);
@@ -332,14 +332,14 @@
by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
qed "Lconst_type";
-goal LList.thy "Lconst(M) = LList_corec M (%x.Inr(<x,x>))";
+goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
by (rtac (equals_LList_corec RS fun_cong) 1);
by (simp_tac sum_ss 1);
by (rtac Lconst 1);
qed "Lconst_eq_LList_corec";
(*Thus we could have used gfp in the definition of Lconst*)
-goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr(<x,x>))";
+goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
by (rtac (equals_LList_corec RS fun_cong) 1);
by (simp_tac sum_ss 1);
by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
@@ -420,8 +420,8 @@
"[| M: llist(A); g(NIL): llist(A); \
\ f(NIL)=g(NIL); \
\ !!x l. [| x:A; l: llist(A) |] ==> \
-\ <f(CONS x l),g(CONS x l)> : \
-\ LListD_Fun (diag A) ((%u.<f(u),g(u)>)``llist(A) Un \
+\ (f(CONS x l),g(CONS x l)) : \
+\ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \
\ diag(llist(A))) \
\ |] ==> f(M) = g(M)";
by (rtac LList_equalityI 1);
@@ -637,7 +637,7 @@
qed "prod_fun_lemma";
goal LList.thy
- "prod_fun Rep_llist Rep_llist `` range(%x. <x, x>) = \
+ "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
\ diag(llist(range(Leaf)))";
br equalityI 1;
by (fast_tac (univ_cs addIs [Rep_llist]) 1);
@@ -647,7 +647,7 @@
(** To show two llists are equal, exhibit a bisimulation!
[also admits true equality] **)
val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
- "[| <l1,l2> : r; r <= llistD_Fun(r Un range(%x.<x,x>)) |] ==> l1=l2";
+ "[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
by (rtac (inj_Rep_llist RS injD) 1);
by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
("A", "range(Leaf)")]
@@ -664,19 +664,19 @@
qed "llist_equalityI";
(** Rules to prove the 2nd premise of llist_equalityI **)
-goalw LList.thy [llistD_Fun_def,LNil_def] "<LNil,LNil> : llistD_Fun(r)";
+goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
qed "llistD_Fun_LNil_I";
val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
- "<l1,l2>:r ==> <LCons x l1, LCons x l2> : llistD_Fun(r)";
+ "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
by (rtac (prem RS prod_fun_imageI) 1);
qed "llistD_Fun_LCons_I";
(*Utilise the "strong" part, i.e. gfp(f)*)
goalw LList.thy [llistD_Fun_def]
- "!!l. <l,l> : llistD_Fun(r Un range(%x.<x,x>))";
+ "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
br (Rep_llist_inverse RS subst) 1;
br prod_fun_imageI 1;
by (rtac (image_Un RS ssubst) 1);
@@ -687,10 +687,10 @@
(*A special case of list_equality for functions over lazy lists*)
val [prem1,prem2] = goal LList.thy
"[| f(LNil)=g(LNil); \
-\ !!x l. <f(LCons x l),g(LCons x l)> : \
-\ llistD_Fun(range(%u. <f(u),g(u)>) Un range(%v. <v,v>)) \
+\ !!x l. (f(LCons x l),g(LCons x l)) : \
+\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \
\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
-by (res_inst_tac [("r", "range(%u. <f(u),g(u)>)")] llist_equalityI 1);
+by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
by (rtac rangeI 1);
by (rtac subsetI 1);
by (etac rangeE 1);
@@ -744,7 +744,7 @@
qed "iterates";
goal LList.thy "lmap f (iterates f x) = iterates f (f x)";
-by (res_inst_tac [("r", "range(%u.<lmap f (iterates f u),iterates f (f u)>)")]
+by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")]
llist_equalityI 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
@@ -777,14 +777,14 @@
val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
[("f","Pair")] (standard(refl RS cong RS cong));
-(*The bisimulation consists of {<lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u))>}
+(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
for all u and all n::nat.*)
val [prem] = goal LList.thy
"(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
br ext 1;
by (res_inst_tac [("r",
- "UN u. range(%n. <nat_rec n (h u) (%m y.lmap f y), \
-\ nat_rec n (iterates f u) (%m y.lmap f y)>)")]
+ "UN u. range(%n. (nat_rec n (h u) (%m y.lmap f y), \
+\ nat_rec n (iterates f u) (%m y.lmap f y)))")]
llist_equalityI 1);
by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
by (safe_tac set_cs);
@@ -834,7 +834,7 @@
(*The infinite first argument blocks the second*)
goal LList.thy "lappend (iterates f x) N = iterates f x";
-by (res_inst_tac [("r", "range(%u.<lappend (iterates f u) N,iterates f u>)")]
+by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")]
llist_equalityI 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
@@ -848,7 +848,7 @@
goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
by (res_inst_tac
[("r",
- "UN n. range(%l.<lmap f (lappend l n),lappend (lmap f l) (lmap f n)>)")]
+ "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")]
llist_equalityI 1);
by (rtac UN1_I 1);
by (rtac rangeI 1);
--- a/src/HOL/ex/LList.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/LList.thy Fri Mar 24 12:30:35 1995 +0100
@@ -19,8 +19,8 @@
Previous definition of llistD_Fun was explicit:
llistD_Fun_def
"llistD_Fun(r) == \
-\ {<LNil,LNil>} Un \
-\ (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
+\ {(LNil,LNil)} Un \
+\ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
*)
LList = Gfp + SList +
@@ -69,9 +69,9 @@
coinductive "LListD(r)"
intrs
- NIL_I "<NIL, NIL> : LListD(r)"
- CONS_I "[| <a,b>: r; <M,N> : LListD(r) \
-\ |] ==> <CONS a M, CONS b N> : LListD(r)"
+ NIL_I "(NIL, NIL) : LListD(r)"
+ CONS_I "[| (a,b): r; (M,N) : LListD(r) \
+\ |] ==> (CONS a M, CONS b N) : LListD(r)"
defs
(*Now used exclusively for abbreviating the coinduction rule*)
@@ -79,9 +79,9 @@
\ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
LListD_Fun_def "LListD_Fun r X == \
-\ {z. z = <NIL, NIL> | \
-\ (? M N a b. z = <CONS a M, CONS b N> & \
-\ <a, b> : r & <M, N> : X)}"
+\ {z. z = (NIL, NIL) | \
+\ (? M N a b. z = (CONS a M, CONS b N) & \
+\ (a, b) : r & (M, N) : X)}"
(*defining the abstract constructors*)
LNil_def "LNil == Abs_llist(NIL)"
@@ -102,7 +102,7 @@
llist_corec_def
"llist_corec a f == \
\ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
-\ (split(%v w. Inr(<Leaf(v), w>))) (f z)))"
+\ (split(%v w. Inr((Leaf(v), w)))) (f z)))"
llistD_Fun_def
"llistD_Fun(r) == \
@@ -113,28 +113,28 @@
Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
Lmap_def
- "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr(<f(x), M'>)))"
+ "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
lmap_def
- "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr(<f(y), z>)))"
+ "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
- iterates_def "iterates f a == llist_corec a (%x. Inr(<x, f(x)>))"
+ iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
(*Append generates its result by applying f, where
- f(<NIL,NIL>) = Inl(Unity)
- f(<NIL, CONS N1 N2>) = Inr(<N1, <NIL,N2>)
- f(<CONS M1 M2, N>) = Inr(<M1, <M2,N>)
+ f((NIL,NIL)) = Inl(())
+ f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
+ f((CONS M1 M2, N)) = Inr((M1, (M2,N))
*)
Lappend_def
- "Lappend M N == LList_corec <M,N> \
-\ (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(<N1, <NIL,N2>>))) \
-\ (%M1 M2 N. Inr(<M1, <M2,N>>))))"
+ "Lappend M N == LList_corec (M,N) \
+\ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
+\ (%M1 M2 N. Inr((M1, (M2,N))))))"
lappend_def
- "lappend l n == llist_corec <l,n> \
-\ (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(<n1, <LNil,n2>>))) \
-\ (%l1 l2 n. Inr(<l1, <l2,n>>))))"
+ "lappend l n == llist_corec (l,n) \
+\ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
+\ (%l1 l2 n. Inr((l1, (l2,n))))))"
rules
(*faking a type definition...*)
--- a/src/HOL/ex/LexProd.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/LexProd.ML Fri Mar 24 12:30:35 1995 +0100
@@ -7,7 +7,7 @@
The lexicographic product of two wellfounded relations is again wellfounded.
*)
-val prems = goal Prod.thy "!a b. P(<a,b>) ==> !p.P(p)";
+val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)";
by (cut_facts_tac prems 1);
by (rtac allI 1);
by (rtac (surjective_pairing RS ssubst) 1);
--- a/src/HOL/ex/LexProd.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/LexProd.thy Fri Mar 24 12:30:35 1995 +0100
@@ -10,6 +10,6 @@
consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
rules
lex_prod_def "ra**rb == {p. ? a a' b b'. \
-\ p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}"
+\ p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
end
--- a/src/HOL/ex/MT.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/MT.ML Fri Mar 24 12:30:35 1995 +0100
@@ -45,13 +45,13 @@
(REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
);
-val prems = goal MT.thy "P a b ==> P (fst <a,b>) (snd <a,b>)";
+val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
by (rtac (fst_conv RS ssubst) 1);
by (rtac (snd_conv RS ssubst) 1);
by (resolve_tac prems 1);
qed "infsys_p1";
-val prems = goal MT.thy "P (fst <a,b>) (snd <a,b>) ==> P a b";
+val prems = goal MT.thy "P (fst (a,b)) (snd (a,b)) ==> P a b";
by (cut_facts_tac prems 1);
by (dtac (fst_conv RS subst) 1);
by (dtac (snd_conv RS subst) 1);
@@ -59,7 +59,7 @@
qed "infsys_p2";
val prems = goal MT.thy
- "P a b c ==> P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>)";
+ "P a b c ==> P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
by (rtac (fst_conv RS ssubst) 1);
by (rtac (fst_conv RS ssubst) 1);
by (rtac (snd_conv RS ssubst) 1);
@@ -68,7 +68,7 @@
qed "infsys_pp1";
val prems = goal MT.thy
- "P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>) ==> P a b c";
+ "P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c)) ==> P a b c";
by (cut_facts_tac prems 1);
by (dtac (fst_conv RS subst) 1);
by (dtac (fst_conv RS subst) 1);
@@ -240,23 +240,23 @@
val prems = goalw MT.thy [eval_def, eval_rel_def]
" [| ve |- e ---> v; \
-\ !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
-\ !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app ve ev>); \
-\ !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
+\ !!ve c. P(((ve,e_const(c)),v_const(c))); \
+\ !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
+\ !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
\ !!ev1 ev2 ve cl e. \
\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
-\ P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
+\ P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
\ !!ve c1 c2 e1 e2. \
-\ [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
-\ P(<<ve,e1 @ e2>,v_const(c_app c1 c2)>); \
+\ [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
+\ P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
\ !!ve vem xm e1 e2 em v v2. \
-\ [| P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
-\ P(<<ve,e2>,v2>); \
-\ P(<<vem + {xm |-> v2},em>,v>) \
+\ [| P(((ve,e1),v_clos(<|xm,em,vem|>))); \
+\ P(((ve,e2),v2)); \
+\ P(((vem + {xm |-> v2},em),v)) \
\ |] ==> \
-\ P(<<ve,e1 @ e2>,v>) \
+\ P(((ve,e1 @ e2),v)) \
\ |] ==> \
-\ P(<<ve,e>,v>)";
+\ P(((ve,e),v))";
by (resolve_tac (prems RL [lfp_ind2]) 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
@@ -356,23 +356,23 @@
val prems = goalw MT.thy [elab_def, elab_rel_def]
" [| te |- e ===> t; \
-\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
-\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
+\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
+\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
\ !!te x e t1 t2. \
-\ [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
-\ P(<<te,fn x => e>,t1->t2>); \
+\ [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
+\ P(((te,fn x => e),t1->t2)); \
\ !!te f x e t1 t2. \
\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
-\ P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
+\ P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
\ |] ==> \
-\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ P(((te,fix f(x) = e),t1->t2)); \
\ !!te e1 e2 t1 t2. \
-\ [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
-\ te |- e2 ===> t1; P(<<te,e2>,t1>) \
+\ [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
+\ te |- e2 ===> t1; P(((te,e2),t1)) \
\ |] ==> \
-\ P(<<te,e1 @ e2>,t2>) \
+\ P(((te,e1 @ e2),t2)) \
\ |] ==> \
-\ P(<<te,e>,t>)";
+\ P(((te,e),t))";
by (resolve_tac (prems RL [lfp_ind2]) 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
@@ -412,18 +412,18 @@
val prems = goalw MT.thy [elab_def, elab_rel_def]
" [| te |- e ===> t; \
-\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
-\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
+\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
+\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
\ !!te x e t1 t2. \
-\ te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
+\ te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
\ !!te f x e t1 t2. \
\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
-\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ P(((te,fix f(x) = e),t1->t2)); \
\ !!te e1 e2 t1 t2. \
\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
-\ P(<<te,e1 @ e2>,t2>) \
+\ P(((te,e1 @ e2),t2)) \
\ |] ==> \
-\ P(<<te,e>,t>)";
+\ P(((te,e),t))";
by (resolve_tac (prems RL [lfp_elim2]) 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
@@ -545,7 +545,7 @@
(* First strong indtroduction (co-induction) rule for hasty_rel *)
-val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
+val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
by (cut_facts_tac prems 1);
by (rtac gfp_coind2 1);
by (rewtac MT.hasty_fun_def);
@@ -561,9 +561,9 @@
\ ve_dom(ve) = te_dom(te); \
\ ! ev1. \
\ ev1:ve_dom(ve) --> \
-\ <ve_app ve ev1,te_app te ev1> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
+\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
\ |] ==> \
-\ <v_clos(<|ev,e,ve|>),t> : hasty_rel";
+\ (v_clos(<|ev,e,ve|>),t) : hasty_rel";
by (cut_facts_tac prems 1);
by (rtac gfp_coind2 1);
by (rewtac hasty_fun_def);
@@ -575,14 +575,14 @@
(* Elimination rule for hasty_rel *)
val prems = goalw MT.thy [hasty_rel_def]
- " [| !! c t.c isof t ==> P(<v_const(c),t>); \
+ " [| !! c t.c isof t ==> P((v_const(c),t)); \
\ !! te ev e t ve. \
\ [| te |- fn ev => e ===> t; \
\ ve_dom(ve) = te_dom(te); \
-\ !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
-\ |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
-\ <v,t> : hasty_rel \
-\ |] ==> P(<v,t>)";
+\ !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
+\ |] ==> P((v_clos(<|ev,e,ve|>),t)); \
+\ (v,t) : hasty_rel \
+\ |] ==> P((v,t))";
by (cut_facts_tac prems 1);
by (etac gfp_elim2 1);
by (rtac mono_hasty_fun 1);
@@ -595,12 +595,12 @@
qed "hasty_rel_elim0";
val prems = goal MT.thy
- " [| <v,t> : hasty_rel; \
+ " [| (v,t) : hasty_rel; \
\ !! c t.c isof t ==> P (v_const c) t; \
\ !! te ev e t ve. \
\ [| te |- fn ev => e ===> t; \
\ ve_dom(ve) = te_dom(te); \
-\ !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
+\ !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
\ |] ==> P (v_clos <|ev,e,ve|>) t \
\ |] ==> P v t";
by (res_inst_tac [("P","P")] infsys_p2 1);
--- a/src/HOL/ex/MT.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/MT.thy Fri Mar 24 12:30:35 1995 +0100
@@ -196,27 +196,27 @@
eval_fun_def
" eval_fun(s) == \
\ { pp. \
-\ (? ve c. pp=<<ve,e_const(c)>,v_const(c)>) | \
-\ (? ve x. pp=<<ve,e_var(x)>,ve_app ve x> & x:ve_dom(ve)) |\
-\ (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
+\ (? ve c. pp=((ve,e_const(c)),v_const(c))) | \
+\ (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\
+\ (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \
\ ( ? ve e x f cl. \
-\ pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
+\ pp=((ve,fix f(x) = e),v_clos(cl)) & \
\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \
\ ) | \
\ ( ? ve e1 e2 c1 c2. \
-\ pp=<<ve,e1 @ e2>,v_const(c_app c1 c2)> & \
-\ <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
+\ pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \
+\ ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \
\ ) | \
\ ( ? ve vem e1 e2 em xm v v2. \
-\ pp=<<ve,e1 @ e2>,v> & \
-\ <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
-\ <<ve,e2>,v2>:s & \
-\ <<vem+{xm |-> v2},em>,v>:s \
+\ pp=((ve,e1 @ e2),v) & \
+\ ((ve,e1),v_clos(<|xm,em,vem|>)):s & \
+\ ((ve,e2),v2):s & \
+\ ((vem+{xm |-> v2},em),v):s \
\ ) \
\ }"
eval_rel_def "eval_rel == lfp(eval_fun)"
- eval_def "ve |- e ---> v == <<ve,e>,v>:eval_rel"
+ eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
(* The static semantics is defined in the same way as the dynamic
semantics. The relation te |- e ===> t express the expression e has the
@@ -226,19 +226,19 @@
elab_fun_def
"elab_fun(s) == \
\ { pp. \
-\ (? te c t. pp=<<te,e_const(c)>,t> & c isof t) | \
-\ (? te x. pp=<<te,e_var(x)>,te_app te x> & x:te_dom(te)) | \
-\ (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
+\ (? te c t. pp=((te,e_const(c)),t) & c isof t) | \
+\ (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \
+\ (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \
\ (? te f x e t1 t2. \
-\ pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
+\ pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \
\ ) | \
\ (? te e1 e2 t1 t2. \
-\ pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
+\ pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \
\ ) \
\ }"
elab_rel_def "elab_rel == lfp(elab_fun)"
- elab_def "te |- e ===> t == <<te,e>,t>:elab_rel"
+ elab_def "te |- e ===> t == ((te,e),t):elab_rel"
(* The original correspondence relation *)
@@ -258,18 +258,18 @@
hasty_fun_def
" hasty_fun(r) == \
\ { p. \
-\ ( ? c t. p = <v_const(c),t> & c isof t) | \
+\ ( ? c t. p = (v_const(c),t) & c isof t) | \
\ ( ? ev e ve t te. \
-\ p = <v_clos(<|ev,e,ve|>),t> & \
+\ p = (v_clos(<|ev,e,ve|>),t) & \
\ te |- fn ev => e ===> t & \
\ ve_dom(ve) = te_dom(te) & \
-\ (! ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : r) \
+\ (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \
\ ) \
\ } \
\ "
hasty_rel_def "hasty_rel == gfp(hasty_fun)"
- hasty_def "v hasty t == <v,t> : hasty_rel"
+ hasty_def "v hasty t == (v,t) : hasty_rel"
hasty_env_def
" ve hastyenv te == \
\ ve_dom(ve) = te_dom(te) & \
--- a/src/HOL/ex/ROOT.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Mar 24 12:30:35 1995 +0100
@@ -8,7 +8,7 @@
CHOL_build_completed; (*Cause examples to fail if CHOL did*)
-(writeln"Root file for CHOL examples";
+(writeln "Root file for CHOL examples";
proof_timing := true;
loadpath := ["ex"];
time_use "ex/cla.ML";
@@ -28,5 +28,5 @@
time_use_thy "Term";
time_use_thy "Simult";
time_use_thy "MT";
- writeln "END: Root file for HOL examples"
+ writeln "END: Root file for CHOL examples"
) handle _ => exit 1;
--- a/src/HOL/ex/SList.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/SList.ML Fri Mar 24 12:30:35 1995 +0100
@@ -156,18 +156,18 @@
(** pred_sexp lemmas **)
goalw SList.thy [CONS_def,In1_def]
- "!!M. [| M: sexp; N: sexp |] ==> <M, CONS M N> : pred_sexp^+";
+ "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
by (asm_simp_tac pred_sexp_ss 1);
qed "pred_sexp_CONS_I1";
goalw SList.thy [CONS_def,In1_def]
- "!!M. [| M: sexp; N: sexp |] ==> <N, CONS M N> : pred_sexp^+";
+ "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
by (asm_simp_tac pred_sexp_ss 1);
qed "pred_sexp_CONS_I2";
val [prem] = goal SList.thy
- "<CONS M1 M2, N> : pred_sexp^+ ==> \
-\ <M1,N> : pred_sexp^+ & <M2,N> : pred_sexp^+";
+ "(CONS M1 M2, N) : pred_sexp^+ ==> \
+\ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS
subsetD RS SigmaE2)) 1);
by (etac (sexp_CONS_D RS conjE) 1);
--- a/src/HOL/ex/Term.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/Term.ML Fri Mar 24 12:30:35 1995 +0100
@@ -119,7 +119,7 @@
val [prem] = goal Term.thy
"N: list(term(A)) ==> \
-\ !M. <N,M>: pred_sexp^+ --> \
+\ !M. (N,M): pred_sexp^+ --> \
\ Abs_map (cut h (pred_sexp^+) M) N = \
\ Abs_map h N";
by (rtac (prem RS list.induct) 1);
--- a/src/HOL/ex/rel.ML Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/rel.ML Fri Mar 24 12:30:35 1995 +0100
@@ -17,8 +17,8 @@
],
None)
[
- ("domain_def", "domain(r) == {a. ? b. <a,b> : r}" ),
- ("range2_def", "range2(r) == {b. ? a. <a,b> : r}" ),
+ ("domain_def", "domain(r) == {a. ? b. (a,b) : r}" ),
+ ("range2_def", "range2(r) == {b. ? a. (a,b) : r}" ),
("field_def", "field(r) == domain(r) Un range2(r)" )
];
end;
@@ -33,12 +33,12 @@
(*** domain ***)
-val [prem] = goalw Rel.thy [domain_def,Pair_def] "<a,b>: r ==> a : domain(r)";
+val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
by (fast_tac (set_cs addIs [prem]) 1);
qed "domainI";
val major::prems = goalw Rel.thy [domain_def]
- "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P";
+ "[| a : domain(r); !!y. (a,y): r ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (REPEAT (ares_tac prems 1));
@@ -47,12 +47,12 @@
(*** range2 ***)
-val [prem] = goalw Rel.thy [range2_def,Pair_def] "<a,b>: r ==> b : range2(r)";
+val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
by (fast_tac (set_cs addIs [prem]) 1);
qed "range2I";
val major::prems = goalw Rel.thy [range2_def]
- "[| b : range2(r); !!x. <x,b>: r ==> P |] ==> P";
+ "[| b : range2(r); !!x. (x,b): r ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (REPEAT (ares_tac prems 1));
@@ -61,16 +61,16 @@
(*** field ***)
-val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> a : field(r)";
+val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)";
by (rtac (prem RS domainI RS UnI1) 1);
qed "fieldI1";
-val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> b : field(r)";
+val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)";
by (rtac (prem RS range2I RS UnI2) 1);
qed "fieldI2";
val [prem] = goalw Rel.thy [field_def]
- "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
+ "(~ (c,a):r ==> (a,b): r) ==> a : field(r)";
by (rtac (prem RS domainI RS UnCI) 1);
by (swap_res_tac [range2I] 1);
by (etac notnotD 1);
@@ -78,8 +78,8 @@
val major::prems = goalw Rel.thy [field_def]
"[| a : field(r); \
-\ !!x. <a,x>: r ==> P; \
-\ !!x. <x,a>: r ==> P |] ==> P";
+\ !!x. (a,x): r ==> P; \
+\ !!x. (x,a): r ==> P |] ==> P";
by (rtac (major RS UnE) 1);
by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1));
qed "fieldE";
@@ -98,7 +98,7 @@
(*If r allows well-founded induction then wf(r)*)
val [prem1,prem2] = goalw Rel.thy [wf_def]
"[| field(r)<=A; \
-\ !!P u. ! x:A. (! y. <y,x>: r --> P(y)) --> P(x) ==> P(u) |] \
+\ !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |] \
\ ==> wf(r)";
by (rtac (prem1 RS wfI) 1);
by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);