--- a/src/HOL/Arith.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Arith.ML Fri Oct 10 19:02:28 1997 +0200
@@ -255,7 +255,7 @@
(*non-strict, in 1st argument*)
goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
-by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
by (etac add_less_mono1 1);
by (assume_tac 1);
qed "add_le_mono1";
--- a/src/HOL/Finite.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Finite.ML Fri Oct 10 19:02:28 1997 +0200
@@ -215,8 +215,8 @@
qed "finite_has_card";
goal Finite.thy
- "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
-\ ? m::nat. m<n & (? g. A = {g i|i.i<m})";
+ "!!A.[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
+\ ? m::nat. m<n & (? g. A = {g i|i. i<m})";
by (res_inst_tac [("n","n")] natE 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
@@ -277,11 +277,11 @@
val lemma = result();
goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
-\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
+\ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
by (rtac Least_equality 1);
by (dtac finite_has_card 1);
by (etac exE 1);
- by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
+ by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1);
by (etac exE 1);
by (res_inst_tac
[("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
--- a/src/HOL/Fun.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Fun.ML Fri Oct 10 19:02:28 1997 +0200
@@ -46,7 +46,7 @@
by (etac arg_cong 1);
qed "inj_eq";
-val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
+val [major] = goal Fun.thy "inj(f) ==> (@x. f(x)=f(y)) = y";
by (rtac (major RS injD) 1);
by (rtac selectI 1);
by (rtac refl 1);
--- a/src/HOL/Gfp.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Gfp.ML Fri Oct 10 19:02:28 1997 +0200
@@ -73,13 +73,13 @@
- instead of the condition X <= f(X)
consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un X Un B)";
+val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)";
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
qed "coinduct3_mono_lemma";
val [prem,mono] = goal Gfp.thy
- "[| X <= f(lfp(%x.f(x) Un X Un gfp(f))); mono(f) |] ==> \
-\ lfp(%x.f(x) Un X Un gfp(f)) <= f(lfp(%x.f(x) Un X Un gfp(f)))";
+ "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \
+\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
by (rtac subset_trans 1);
by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
by (rtac (Un_least RS Un_least) 1);
@@ -92,7 +92,7 @@
qed "coinduct3_lemma";
val prems = goal Gfp.thy
- "[| mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
+ "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
by (rtac (UnI2 RS UnI1) 1);
@@ -123,7 +123,7 @@
qed "def_Collect_coinduct";
val rew::prems = goal Gfp.thy
- "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A";
+ "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
qed "def_coinduct3";
--- a/src/HOL/HOL.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/HOL.ML Fri Oct 10 19:02:28 1997 +0200
@@ -90,15 +90,15 @@
qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
(fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
-qed_goalw "spec" HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
(fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
-qed_goal "allE" HOL.thy "[| !x.P(x); P(x) ==> R |] ==> R"
+qed_goal "allE" HOL.thy "[| !x. P(x); P(x) ==> R |] ==> R"
(fn major::prems=>
[ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
qed_goal "all_dupE" HOL.thy
- "[| ! x.P(x); [| P(x); ! x.P(x) |] ==> R |] ==> R"
+ "[| ! x. P(x); [| P(x); ! x. P(x) |] ==> R |] ==> R"
(fn prems =>
[ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
@@ -155,11 +155,11 @@
(** Existential quantifier **)
section "?";
-qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a. P(x)"
(fn prems => [rtac selectI 1, resolve_tac prems 1]);
qed_goalw "exE" HOL.thy [Ex_def]
- "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+ "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
(fn prems => [REPEAT(resolve_tac prems 1)]);
@@ -237,12 +237,12 @@
(*Sometimes easier to use: the premises have no shared variables. Safe!*)
qed_goal "ex_ex1I" HOL.thy
- "[| ? x.P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
+ "[| ? x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
(fn [ex,eq] => [ (rtac (ex RS exE) 1),
(REPEAT (ares_tac [ex1I,eq] 1)) ]);
qed_goalw "ex1E" HOL.thy [Ex1_def]
- "[| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
+ "[| ?! x. P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
(fn major::prems =>
[rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
@@ -252,23 +252,23 @@
(*Easier to apply than selectI: conclusion has only one occurrence of P*)
qed_goal "selectI2" HOL.thy
- "[| P(a); !!x. P(x) ==> Q(x) |] ==> Q(@x.P(x))"
+ "[| P(a); !!x. P(x) ==> Q(x) |] ==> Q(@x. P(x))"
(fn prems => [ resolve_tac prems 1,
rtac selectI 1,
resolve_tac prems 1 ]);
(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
qed_goal "selectI2EX" HOL.thy
- "[| ? a.P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
+ "[| ? a. P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
qed_goal "select_equality" HOL.thy
- "[| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
+ "[| P(a); !!x. P(x) ==> x=a |] ==> (@x. P(x)) = a"
(fn prems => [ rtac selectI2 1,
REPEAT (ares_tac prems 1) ]);
qed_goalw "select1_equality" HOL.thy [Ex1_def]
- "!!P. [| ?!x.P(x); P(a) |] ==> (@x.P(x)) = a"
+ "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a"
(fn _ => [rtac select_equality 1, atac 1,
etac exE 1, etac conjE 1,
rtac allE 1, atac 1,
@@ -313,7 +313,7 @@
(REPEAT (DEPTH_SOLVE_1
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
-qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)"
+qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
(fn prems=>
[ (rtac ccontr 1),
(REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ]);
--- a/src/HOL/HOL.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/HOL.thy Fri Oct 10 19:02:28 1997 +0200
@@ -106,7 +106,7 @@
translations
"x ~= y" == "~ (x = y)"
- "@ x.b" == "Eps (%x. b)"
+ "@ x. b" == "Eps (%x. b)"
"ALL xs. P" => "! xs. P"
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
@@ -149,18 +149,18 @@
refl "t = (t::'a)"
subst "[| s = t; P(s) |] ==> P(t::'a)"
- ext "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
- selectI "P(x::'a) ==> P(@x.P(x))"
+ ext "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
+ selectI "P (x::'a) ==> P (@x. P x)"
impI "(P ==> Q) ==> P-->Q"
mp "[| P-->Q; P |] ==> Q"
defs
- True_def "True == ((%x::bool.x)=(%x.x))"
- All_def "All(P) == (P = (%x.True))"
- Ex_def "Ex(P) == P(@x.P(x))"
- False_def "False == (!P.P)"
+ True_def "True == ((%x::bool. x) = (%x. x))"
+ All_def "All(P) == (P = (%x. True))"
+ Ex_def "Ex(P) == P(@x. P(x))"
+ False_def "False == (!P. P)"
not_def "~ P == P-->False"
and_def "P & Q == !R. (P-->Q-->R) --> R"
or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R"
--- a/src/HOL/Hoare/Arith2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Arith2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -62,7 +62,7 @@
val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
by (cut_facts_tac prems 1);
-by (subgoal_tac "n<=m ==> !x.cd x m n = cd x (m-n) n" 1);
+by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
by (Asm_simp_tac 1);
by (rtac allI 1);
by (etac cd_diff_l 1);
@@ -70,7 +70,7 @@
val prems=goalw thy [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
by (cut_facts_tac prems 1);
-by (subgoal_tac "m<=n ==> !x.cd x m n = cd x m (n-m)" 1);
+by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
by (Asm_simp_tac 1);
by (rtac allI 1);
by (etac cd_diff_r 1);
--- a/src/HOL/Hoare/Arith2.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Arith2.thy Fri Oct 10 19:02:28 1997 +0200
@@ -16,7 +16,7 @@
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
pow :: [nat, nat] => nat (infixl 75)
- "m pow n == nat_rec (Suc 0) (%u v.m*v) n"
+ "m pow n == nat_rec (Suc 0) (%u v. m*v) n"
fac :: nat => nat
"fac m == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
--- a/src/HOL/Hoare/Hoare.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Hoare.ML Fri Oct 10 19:02:28 1997 +0200
@@ -11,20 +11,20 @@
(*** Hoare rules ***)
val SkipRule = prove_goalw thy [Spec_def,Skip_def]
- "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
+ "(!!s. p(s) ==> q(s)) ==> Spec p Skip q"
(fn prems => [fast_tac (!claset addIs prems) 1]);
val AssignRule = prove_goalw thy [Spec_def,Assign_def]
- "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
+ "(!!s. p s ==> q(%x. if x=v then e s else s x)) ==> Spec p (Assign v e) q"
(fn prems => [fast_tac (!claset addIs prems) 1]);
val SeqRule = prove_goalw thy [Spec_def,Seq_def]
- "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
+ "[| Spec p c (%s. q s); Spec (%s. q s) c' r |] ==> Spec p (Seq c c') r"
(fn prems => [cut_facts_tac prems 1, Fast_tac 1]);
val IfRule = prove_goalw thy [Spec_def,Cond_def]
"[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
-\ Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
+\ Spec (%s. q s) c r; Spec (%s. q' s) c' r |] \
\ ==> Spec p (Cond b c c') r"
(fn [prem1,prem2,prem3] =>
[REPEAT (rtac allI 1),
@@ -39,7 +39,7 @@
fast_tac (!claset addIs [prem1]) 1]);
val lemma = prove_goalw thy [Spec_def,While_def]
- "[| Spec (%s.I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \
+ "[| Spec (%s. I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \
\ ==> Spec I (While b I c) q"
(fn [prem1,prem2] =>
[REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
@@ -134,7 +134,7 @@
(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
- v::vl:(term) list Liste der zu eliminierenden Programmvariablen
- meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird
- z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+ z.B.: "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))"
- namexAll:string Name von ^ (hier "x")
- varx:term Term zu ^ (hier Var(("x",0),...))
- varP:term Term zu ^ (hier Var(("P",0),...))
@@ -144,25 +144,25 @@
- eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
- Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
- meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
+ meta_spec zu "(!! s a. PROP P(s,a)) ==> (!! s. PROP P(s,x(s)))"
- Instanziierungen in meta_spec:
- varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
+ varx wird mit "%s:(type_pvar) state. s(pvar)" instanziiert
varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
- - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
+ - zu Subgoal "!!s. s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
- substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
trm1 = "s(Suc(0)) = xs ==> xs = 1"
- abstrahiere ueber xs:
- trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
+ trm2 = "%xs. s(Suc(0)) = xs ==> xs = 1"
- abstrahiere ueber restliche Vorkommen von s:
- trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
+ trm3 = "%s xs. s(Suc(0)) = xs ==> xs = 1"
- instanziiere varP mit trm3
*)
(* StateElimTac: tactic to eliminate all program variable from subgoal i
- - applies to subgoals of the form "!!s:('a) state.P(s)",
+ - applies to subgoals of the form "!!s:('a) state. P(s)",
i.e. the term Const("all",_) $ Abs ("s",pvar --> 'a,_)
- - meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+ - meta_spec has the form "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))"
*)
val StateElimTac = SUBGOAL (fn (Bi,i) =>
--- a/src/HOL/Hoare/Hoare.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Hoare.thy Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
"Skip s s' == (s=s')"
Assign :: [pvar, 'a exp] => 'a com
- "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+ "Assign v e s s' == (s' = (%x. if x=v then e(s) else s(x)))"
Seq :: ['a com, 'a com] => 'a com
"Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
--- a/src/HOL/IMP/Hoare.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML Fri Oct 10 19:02:28 1997 +0200
@@ -27,7 +27,7 @@
by (Simp_tac 1);
qed "wp_SKIP";
-goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
by (Simp_tac 1);
qed "wp_Ass";
@@ -66,7 +66,7 @@
goal thy
"wp (WHILE b DO c) Q s = \
-\ (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
+\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
by (rtac iffI 1);
by (rtac weak_coinduct 1);
--- a/src/HOL/IMP/Hoare.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/Hoare.thy Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
inductive hoare
intrs
skip "|- {P}SKIP{P}"
- ass "|- {%s.P(s[a s/x])} x:=a {P}"
+ ass "|- {%s. P(s[a s/x])} x:=a {P}"
semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
|- {P} IF b THEN c ELSE d {Q}"
--- a/src/HOL/IMP/VC.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/VC.ML Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
AddIs hoare.intrs;
-val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
+val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
goal VC.thy "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
by (acom.induct_tac "c" 1);
--- a/src/HOL/IMP/VC.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/VC.thy Fri Oct 10 19:02:28 1997 +0200
@@ -23,14 +23,14 @@
primrec awp acom
"awp Askip Q = Q"
- "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
+ "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
"awp (Asemi c d) Q = awp c (awp d Q)"
"awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
"awp (Awhile b I c) Q = I"
primrec vc acom
- "vc Askip Q = (%s.True)"
- "vc (Aass x a) Q = (%s.True)"
+ "vc Askip Q = (%s. True)"
+ "vc (Aass x a) Q = (%s. True)"
"vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
"vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"
"vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
@@ -45,8 +45,8 @@
(* simultaneous computation of vc and awp: *)
primrec vcawp acom
- "vcawp Askip Q = (%s.True, Q)"
- "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
+ "vcawp Askip Q = (%s. True, Q)"
+ "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
"vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
(vcc,wpc) = vcawp c wpd
in (%s. vcc s & vcd s, wpc))"
--- a/src/HOL/IOA/IOA.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/IOA.ML Fri Oct 10 19:02:28 1997 +0200
@@ -47,7 +47,7 @@
qed "mk_trace_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 1);
by (asm_simp_tac (!simpset addsimps exec_rws) 1);
qed "reachable_0";
@@ -56,9 +56,9 @@
"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
by (asm_full_simp_tac (!simpset delsimps bex_simps) 1);
by (safe_tac (!claset));
- 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 1);
by (Asm_simp_tac 1);
--- a/src/HOL/IOA/IOA.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/IOA.thy Fri Oct 10 19:02:28 1997 +0200
@@ -104,13 +104,13 @@
(* Restrict the trace to those members of the set s *)
filter_oseq_def
"filter_oseq p s ==
- (%i.case s(i)
+ (%i. case s(i)
of None => None
| Some(x) => if p x then Some x else None)"
mk_trace_def
- "mk_trace(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"
+ "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
(* Does an ioa have an execution with the given trace *)
--- a/src/HOL/IOA/Solve.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/Solve.ML Fri Oct 10 19:02:28 1997 +0200
@@ -22,7 +22,7 @@
by (Asm_full_simp_tac 1);
(* give execution of abstract automata *)
- by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1);
+ by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
(* Traces coincide *)
by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1);
@@ -68,9 +68,9 @@
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
- "(filter_oseq (%a.a:actions(asig_of(C1))) \
+ "(filter_oseq (%a. a:actions(asig_of(C1))) \
\ (fst ex), \
-\ %i.fst (snd ex i))")] bexI 1);
+\ %i. fst (snd ex i))")] bexI 1);
(* fst(s) is in projected execution *)
by (Simp_tac 1);
by (Fast_tac 1);
@@ -88,9 +88,9 @@
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
- "(filter_oseq (%a.a:actions(asig_of(C2)))\
+ "(filter_oseq (%a. a:actions(asig_of(C2)))\
\ (fst ex), \
-\ %i.snd (snd ex i))")] bexI 1);
+\ %i. snd (snd ex i))")] bexI 1);
(* fst(s) is in projected execution *)
by (Simp_tac 1);
by (Fast_tac 1);
--- a/src/HOL/Induct/LFilter.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML Fri Oct 10 19:02:28 1997 +0200
@@ -178,7 +178,7 @@
(*** lfilter: simple facts by coinduction ***)
-goal thy "lfilter (%x.True) l = l";
+goal thy "lfilter (%x. True) l = l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS Simp_tac);
by (Blast_tac 1);
--- a/src/HOL/Induct/LList.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LList.ML Fri Oct 10 19:02:28 1997 +0200
@@ -62,16 +62,16 @@
(*** LList_corec satisfies the desired recurion equation ***)
(*A continuity result?*)
-goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))";
+goalw LList.thy [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))";
by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
qed "CONS_UN1";
(*UNUSED; obsolete?
-goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
+goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
qed "split_UN1";
-goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
+goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
qed "sum_case2_UN1";
*)
@@ -87,7 +87,7 @@
(** The directions of the equality are proved separately **)
goalw LList.thy [LList_corec_def]
- "LList_corec a f <= sum_case (%u.NIL) \
+ "LList_corec a f <= sum_case (%u. NIL) \
\ (split(%z w. CONS z (LList_corec w f))) (f a)";
by (rtac UN1_least 1);
by (res_inst_tac [("n","k")] natE 1);
@@ -96,7 +96,7 @@
qed "LList_corec_subset1";
goalw LList.thy [LList_corec_def]
- "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
+ "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
\ LList_corec a f";
by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
by (safe_tac (!claset));
@@ -114,15 +114,15 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == LList_corec x f |] ==> \
-\ h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
+\ h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)";
by (rewtac rew);
by (rtac LList_corec 1);
qed "def_LList_corec";
(*A typical use of co-induction to show membership in the gfp.
Bisimulation is range(%x. LList_corec x f) *)
-goal LList.thy "LList_corec a f : llist({u.True})";
-by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
+goal LList.thy "LList_corec a f : llist({u. True})";
+by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
by (safe_tac (!claset));
by (stac LList_corec 1);
@@ -132,9 +132,9 @@
(*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 (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
by (safe_tac (!claset));
by (stac LList_corec 1);
@@ -263,12 +263,12 @@
(*abstract proof using a bisimulation*)
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \
-\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+ "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
+\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
\ ==> h1=h2";
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "{u.True}"),
+by (res_inst_tac [("A", "{u. True}"),
("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
by (rtac rangeI 1);
by (safe_tac (!claset));
@@ -280,8 +280,8 @@
qed "LList_corec_unique";
val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
-\ ==> h = (%x.LList_corec x f)";
+ "[| !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) |] \
+\ ==> h = (%x. LList_corec x f)";
by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
qed "equals_LList_corec";
@@ -298,8 +298,8 @@
qed "ntrunc_CONS";
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \
-\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+ "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
+\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
\ ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
by (rename_tac "x k" 1);
@@ -338,14 +338,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 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 1);
by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
@@ -485,7 +485,7 @@
rangeI RS LListD_Fun_CONS_I] 1));
qed "Lmap_compose";
-val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
+val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
by (rtac (prem RS imageI RS LList_equalityI) 1);
by (safe_tac (!claset));
by (etac llist.elim 1);
@@ -547,7 +547,7 @@
(*strong co-induction: bisimulation and case analysis on one variable*)
goal LList.thy
"!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1);
+by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
by (etac imageI 1);
by (rtac subsetI 1);
by (etac imageE 1);
@@ -605,7 +605,7 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == llist_corec x f |] ==> \
-\ h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
+\ h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)";
by (rewtac rew);
by (rtac llist_corec 1);
qed "def_llist_corec";
@@ -740,7 +740,7 @@
by (ALLGOALS Simp_tac);
qed "lmap_compose";
-goal LList.thy "lmap (%x.x) l = l";
+goal LList.thy "lmap (%x. x) l = l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS Simp_tac);
qed "lmap_ident";
@@ -793,8 +793,8 @@
"(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
by (rtac ext 1);
by (res_inst_tac [("r",
- "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
-\ nat_rec (iterates f u) (%m y.lmap f y) n))")]
+ "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
+\ nat_rec (iterates f u) (%m y. lmap f y) n))")]
llist_equalityI 1);
by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
by (safe_tac (!claset));
--- a/src/HOL/Induct/LList.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LList.thy Fri Oct 10 19:02:28 1997 +0200
@@ -11,7 +11,7 @@
bounds on the amount of lookahead required.
Could try (but would it work for the gfp analogue of term?)
- LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
+ LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)"
A nice but complex example would be [ML for the Working Programmer, page 176]
from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
@@ -74,7 +74,7 @@
|] ==> (CONS a M, CONS b N) : LListD(r)"
translations
- "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
+ "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
defs
@@ -108,7 +108,7 @@
llist_corec_def
"llist_corec a f ==
Abs_llist(LList_corec a
- (%z.case f z of Inl x => Inl(x)
+ (%z. case f z of Inl x => Inl(x)
| Inr(v,w) => Inr(Leaf(v), w)))"
llistD_Fun_def
--- a/src/HOL/Induct/PropLog.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/PropLog.thy Fri Oct 10 19:02:28 1997 +0200
@@ -33,14 +33,14 @@
eval_def "tt[p] == eval2 p tt"
primrec eval2 pl
- "eval2(false) = (%x.False)"
- "eval2(#v) = (%tt.v:tt)"
- "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
+ "eval2(false) = (%x. False)"
+ "eval2(#v) = (%tt. v:tt)"
+ "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
primrec hyps pl
"hyps(false) = (%tt.{})"
"hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
- "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
+ "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
end
--- a/src/HOL/Induct/SList.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/SList.ML Fri Oct 10 19:02:28 1997 +0200
@@ -315,7 +315,7 @@
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_append2";
-goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
by (list_ind_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_filter2";
@@ -347,7 +347,7 @@
(** Additional mapping lemmas **)
-goal SList.thy "map (%x.x) xs = xs";
+goal SList.thy "map (%x. x) xs = xs";
by (list_ind_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_ident2";
--- a/src/HOL/Induct/SList.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/SList.thy Fri Oct 10 19:02:28 1997 +0200
@@ -56,9 +56,9 @@
"[x]" == "x#[]"
"[]" == "Nil"
- "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
+ "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
- "[x:xs . P]" == "filter (%x.P) xs"
+ "[x:xs . P]" == "filter (%x. P) xs"
defs
(* Defining the Concrete Constructors *)
@@ -82,7 +82,7 @@
Nil_def "Nil == Abs_list(NIL)"
Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
- List_case_def "List_case c d == Case (%x.c) (Split d)"
+ List_case_def "List_case c d == Case (%x. c) (Split d)"
(* list Recursion -- the trancl is Essential; see list.ML *)
@@ -99,11 +99,11 @@
Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
- null_def "null(xs) == list_rec xs True (%x xs r.False)"
- hd_def "hd(xs) == list_rec xs arbitrary (%x xs r.x)"
- tl_def "tl(xs) == list_rec xs arbitrary (%x xs r.xs)"
+ null_def "null(xs) == list_rec xs True (%x xs r. False)"
+ hd_def "hd(xs) == list_rec xs arbitrary (%x xs r. x)"
+ tl_def "tl(xs) == list_rec xs arbitrary (%x xs r. xs)"
(* a total version of tl: *)
- ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
+ ttl_def "ttl(xs) == list_rec xs [] (%x xs r. xs)"
set_def "set xs == list_rec xs {} (%x l r. insert x r)"
@@ -114,6 +114,6 @@
filter_def "filter P xs ==
list_rec xs [] (%x xs r. if P(x) then x#r else r)"
- list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
+ list_case_def "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
end
--- a/src/HOL/Induct/Simult.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/Simult.ML Fri Oct 10 19:02:28 1997 +0200
@@ -87,8 +87,8 @@
\ Q(Fnil); \
\ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons t ts) \
\ |] ==> (! t. P(t)) & (! ts. Q(ts))";
-by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
- ("Q1","%z.Q(Abs_Forest(z))")]
+by (res_inst_tac [("P1","%z. P(Abs_Tree(z))"),
+ ("Q1","%z. Q(Abs_Forest(z))")]
(Tree_Forest_induct RS conjE) 1);
(*Instantiates ?A1 to range(Leaf). *)
by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst,
--- a/src/HOL/Induct/Term.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/Term.ML Fri Oct 10 19:02:28 1997 +0200
@@ -37,7 +37,7 @@
(*Induction for the set term(A) *)
val [major,minor] = goal Term.thy
"[| M: term(A); \
-\ !!x zs. [| x: A; zs: list(term(A)); zs: list({x.R(x)}) \
+\ !!x zs. [| x: A; zs: list(term(A)); zs: list({x. R(x)}) \
\ |] ==> R(x$zs) \
\ |] ==> R(M)";
by (rtac (major RS term.induct) 1);
--- a/src/HOL/Lex/AutoChopper.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Fri Oct 10 19:02:28 1997 +0200
@@ -42,7 +42,7 @@
bind_thm("no_acc", result() RS spec RS spec RS mp);
-val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
+val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)";
by (cut_facts_tac [prem] 1);
by (Fast_tac 1);
val ex_special = result();
@@ -108,9 +108,9 @@
by (Asm_simp_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
by (strip_tac 1);
- by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+ by (res_inst_tac [("f","%k. a#k")] ex_special 1);
by (Simp_tac 1);
- by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
by (Simp_tac 1);
by (Fast_tac 1);
by (strip_tac 1);
@@ -121,9 +121,9 @@
by (Fast_tac 1);
by (Simp_tac 1);
by (strip_tac 1);
-by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+by (res_inst_tac [("f","%k. a#k")] ex_special 1);
by (Simp_tac 1);
-by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
by (Simp_tac 1);
by (Fast_tac 1);
val step2_c = (result() repeat_RS spec) RS mp;
@@ -172,7 +172,7 @@
"! st erk r p ys yss zs. \
\ acc xs st erk r p A = (ys#yss, zs) --> \
\ (if acc_prefix A st xs \
-\ then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
+\ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
\ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (list.induct_tac "xs" 1);
@@ -183,10 +183,10 @@
by (case_tac "acc_prefix A (next A st a) list" 1);
by (rtac conjI 1);
by (strip_tac 1);
- by (res_inst_tac [("f","%k.a#k")] ex_special 1);
- by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (res_inst_tac [("f","%k. a#k")] ex_special 1);
+ by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
by (Simp_tac 1);
- by (res_inst_tac [("P","%k.ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+ by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
@@ -194,10 +194,10 @@
by (Simp_tac 1);
by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
by (strip_tac 1);
- by (res_inst_tac [("f","%k.a#k")] ex_special 1);
- by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (res_inst_tac [("f","%k. a#k")] ex_special 1);
+ by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
by (Simp_tac 1);
- by (res_inst_tac [("P","%k.ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+ by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
--- a/src/HOL/Lex/Prefix.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lex/Prefix.ML Fri Oct 10 19:02:28 1997 +0200
@@ -6,7 +6,7 @@
open Prefix;
-val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)";
+val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
by (rtac allI 1);
by (list.induct_tac "l" 1);
by (rtac maj 1);
--- a/src/HOL/Lfp.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lfp.ML Fri Oct 10 19:02:28 1997 +0200
@@ -41,7 +41,7 @@
val [lfp,mono,indhyp] = goal Lfp.thy
"[| a: lfp(f); mono(f); \
-\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \
+\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
@@ -66,7 +66,7 @@
val rew::prems = goal Lfp.thy
"[| A == lfp(f); mono(f); a:A; \
-\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \
+\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
--- a/src/HOL/List.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/List.ML Fri Oct 10 19:02:28 1997 +0200
@@ -174,7 +174,7 @@
by (ALLGOALS Asm_simp_tac);
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
-goal thy "map (%x.x) = (%xs.xs)";
+goal thy "map (%x. x) = (%xs. xs)";
by (rtac ext 1);
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -235,7 +235,7 @@
qed "mem_append";
Addsimps[mem_append];
-goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
by (induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_filter";
@@ -285,7 +285,7 @@
section "list_all";
-goal thy "list_all (%x.True) xs = True";
+goal thy "list_all (%x. True) xs = True";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "list_all_True";
@@ -599,7 +599,7 @@
Addsimps [takeWhile_append1];
goal thy
- "(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
+ "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -616,7 +616,7 @@
Addsimps [dropWhile_append1];
goal thy
- "(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
+ "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
--- a/src/HOL/List.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/List.thy Fri Oct 10 19:02:28 1997 +0200
@@ -38,7 +38,7 @@
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
- "[x:xs . P]" == "filter (%x.P) xs"
+ "[x:xs . P]" == "filter (%x. P) xs"
syntax (symbols)
"@filter" :: [idt, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
--- a/src/HOL/MiniML/Instance.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Instance.ML Fri Oct 10 19:02:28 1997 +0200
@@ -211,7 +211,7 @@
goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
by (strip_tac 1);
-by (res_inst_tac [("x","%a.t")]exI 1);
+by (res_inst_tac [("x","%a. t")]exI 1);
by (Simp_tac 1);
qed "bound_typ_instance_BVar";
AddIffs [bound_typ_instance_BVar];
--- a/src/HOL/MiniML/Maybe.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Maybe.thy Fri Oct 10 19:02:28 1997 +0200
@@ -13,6 +13,6 @@
"option_bind m f == case m of None => None | Some r => f r"
syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "option_bind E (%P.F)"
+translations "P := E; F" == "option_bind E (%P. F)"
end
--- a/src/HOL/MiniML/Type.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Type.ML Fri Oct 10 19:02:28 1997 +0200
@@ -16,7 +16,7 @@
by (Fast_tac 1);
qed_spec_mp "mk_scheme_Fun";
-goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
+goal thy "!t'. mk_scheme t = mk_scheme t' --> t=t'";
by (typ.induct_tac "t" 1);
by (rtac allI 1);
by (typ.induct_tac "t'" 1);
@@ -110,14 +110,14 @@
Addsimps[new_tv_id_subst];
goal thy "new_tv n (sch::type_scheme) --> \
-\ $(%k.if k<n then S k else S' k) sch = $S sch";
+\ $(%k. if k<n then S k else S' k) sch = $S sch";
by (type_scheme.induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme";
Addsimps [new_if_subst_type_scheme];
goal thy "new_tv n (A::type_scheme list) --> \
-\ $(%k.if k<n then S k else S' k) A = $S A";
+\ $(%k. if k<n then S k else S' k) A = $S A";
by (list.induct_tac "A" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme_list";
@@ -673,7 +673,7 @@
(* application of id_subst does not change type expression *)
goalw thy [id_subst_def]
- "$ id_subst = (%t::typ.t)";
+ "$ id_subst = (%t::typ. t)";
by (rtac ext 1);
by (typ.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
@@ -681,7 +681,7 @@
Addsimps [app_subst_id_te];
goalw thy [id_subst_def]
- "$ id_subst = (%sch::type_scheme.sch)";
+ "$ id_subst = (%sch::type_scheme. sch)";
by (rtac ext 1);
by (type_scheme.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
@@ -690,7 +690,7 @@
(* application of id_subst does not change list of type expressions *)
goalw thy [app_subst_list]
- "$ id_subst = (%A::type_scheme list.A)";
+ "$ id_subst = (%A::type_scheme list. A)";
by (rtac ext 1);
by (list.induct_tac "A" 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/MiniML/Type.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Type.thy Fri Oct 10 19:02:28 1997 +0200
@@ -112,7 +112,7 @@
(* identity *)
constdefs
id_subst :: subst
- "id_subst == (%n.TVar n)"
+ "id_subst == (%n. TVar n)"
(* extension of substitution to type structures *)
consts
--- a/src/HOL/MiniML/W.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/W.ML Fri Oct 10 19:02:28 1997 +0200
@@ -485,7 +485,7 @@
(* case Abs e *)
by (strip_tac 1);
by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
+by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1);
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -515,9 +515,9 @@
conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
(** LEVEL 35 **)
by (subgoal_tac
- "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+ "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
\ else Ra x)) ($ Sa t) = \
-\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+\ $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
\ else Ra x)) (ta -> (TVar ma))" 1);
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
\ (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
--- a/src/HOL/Modelcheck/MuCalculus.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy Fri Oct 10 19:02:28 1997 +0200
@@ -18,7 +18,7 @@
defs
-Charfun_def "Charfun == (% A.% x.x:A)"
+Charfun_def "Charfun == (% A.% x. x:A)"
monoP_def "monoP f == mono(Collect o f o Charfun)"
mu_def "mu f == Charfun(lfp(Collect o f o Charfun))"
nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
--- a/src/HOL/NatDef.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/NatDef.ML Fri Oct 10 19:02:28 1997 +0200
@@ -585,14 +585,14 @@
qed "Least_nat_def";
val [prem1,prem2] = goalw thy [Least_nat_def]
- "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
+ "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
by (rtac select_equality 1);
by (blast_tac (!claset addSIs [prem1,prem2]) 1);
by (cut_facts_tac [less_linear] 1);
by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
qed "Least_equality";
-val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
+val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("n","k")] less_induct 1);
by (rtac impI 1);
@@ -604,7 +604,7 @@
qed "LeastI";
(*Proof is almost identical to the one above!*)
-val [prem] = goal thy "P(k::nat) ==> (LEAST x.P(x)) <= k";
+val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("n","k")] less_induct 1);
by (rtac impI 1);
@@ -615,7 +615,7 @@
by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1);
qed "Least_le";
-val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
+val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
by (rtac notI 1);
by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
by (rtac prem 1);
--- a/src/HOL/NatDef.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/NatDef.thy Fri Oct 10 19:02:28 1997 +0200
@@ -56,7 +56,7 @@
translations
"1" == "Suc 0"
"2" == "Suc 1"
- "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
+ "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
defs
--- a/src/HOL/Prod.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Prod.ML Fri Oct 10 19:02:28 1997 +0200
@@ -88,7 +88,7 @@
!!a b. ... = ?P(a,b)
which cannot be solved by reflexivity.
-val [prem] = goal Prod.thy "(!!x.PROP P x) ==> (!!a b. PROP P(a,b))";
+val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
br prem 1;
val lemma1 = result();
@@ -226,7 +226,7 @@
by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
qed "prod_fun_compose";
-goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
+goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
by (rtac ext 1);
by (res_inst_tac [("p","z")] PairE 1);
by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
--- a/src/HOL/Prod.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Prod.thy Fri Oct 10 19:02:28 1997 +0200
@@ -52,17 +52,17 @@
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80)
translations
- "(x, y, z)" == "(x, (y, z))"
- "(x, y)" == "Pair x y"
+ "(x, y, z)" == "(x, (y, z))"
+ "(x, y)" == "Pair x y"
- "%(x,y,zs).b" == "split(%x (y,zs).b)"
- "%(x,y).b" == "split(%x y.b)"
+ "%(x,y,zs).b" == "split(%x (y,zs).b)"
+ "%(x,y).b" == "split(%x y. b)"
"_abs (Pair x y) t" => "%(x,y).t"
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
- "SIGMA x:A.B" => "Sigma A (%x.B)"
- "A Times B" => "Sigma A (_K B)"
+ "SIGMA x:A. B" => "Sigma A (%x. B)"
+ "A Times B" => "Sigma A (_K B)"
syntax (symbols)
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10)
--- a/src/HOL/Quot/FRACT.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/FRACT.ML Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
open FRACT;
goalw thy [per_def,per_NP_def]
-"(op ===)=(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
+"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
fr refl;
qed "inst_NP_per";
--- a/src/HOL/Quot/HQUOT.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.ML Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
open HQUOT;
(* first prove some helpful lemmas *)
-goalw thy [quot_def] "{y.y===x}:quot";
+goalw thy [quot_def] "{y. y===x}:quot";
by (Asm_simp_tac 1);
by (fast_tac (set_cs addIs [per_sym]) 1);
qed "per_class_rep_quot";
@@ -20,7 +20,7 @@
qed "quot_eq";
(* prepare induction and exhaustiveness *)
-val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
+val prems = goal thy "!s. s:quot --> P (Abs_quot s) ==> P x";
by (cut_facts_tac prems 1);
by (rtac (Abs_quot_inverse RS subst) 1);
by (rtac Rep_quot 1);
@@ -28,7 +28,7 @@
by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
qed "all_q";
-goal thy "? s.s:quot & x=Abs_quot s";
+goal thy "? s. s:quot & x=Abs_quot s";
by (res_inst_tac [("x","Rep_quot x")] exI 1);
by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
qed "exh_q";
@@ -113,7 +113,7 @@
qed "er_class_not";
(* exhaustiveness and induction *)
-goalw thy [peclass_def] "? s.x=<[s]>";
+goalw thy [peclass_def] "? s. x=<[s]>";
by (rtac all_q 1);
by (strip_tac 1);
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
@@ -128,7 +128,7 @@
by (fast_tac set_cs 1);
qed "per_class_exh";
-val prems = goal thy "!x.P<[x]> ==> P s";
+val prems = goal thy "!x. P<[x]> ==> P s";
by (cut_facts_tac (prems@[
read_instantiate[("x","s::'a::per quot")] per_class_exh]) 1);
by (fast_tac set_cs 1);
@@ -160,7 +160,7 @@
qed "er_class_any_in";
(* equivalent theorem for per would need !x.x:D *)
-val prems = goal thy "!x::'a::per.x:D==><[any_in (q::'a::per quot)]> = q";
+val prems = goal thy "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
by (cut_facts_tac prems 1);
fr per_class_all;
fr allI;
--- a/src/HOL/Quot/HQUOT.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.thy Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
HQUOT = PER +
-typedef 'a quot = "{s::'a::per set. ? r.!y.y:s=y===r}" (quotNE)
+typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
(* constants for equivalence classes *)
consts
@@ -21,7 +21,7 @@
translations "<[x]>" == "peclass x"
defs
- peclass_def "<[x]> == Abs_quot {y.y===x}"
+ peclass_def "<[x]> == Abs_quot {y. y===x}"
any_in_def "any_in f == @x.<[x]>=f"
end
--- a/src/HOL/Quot/NPAIR.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.thy Fri Oct 10 19:02:28 1997 +0200
@@ -18,7 +18,7 @@
(* NPAIR (continued) *)
defs per_NP_def
- "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
+ "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
(* for proves of this rule see [Slo97diss] *)
rules
--- a/src/HOL/Quot/PER.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/PER.ML Fri Oct 10 19:02:28 1997 +0200
@@ -6,12 +6,12 @@
*)
open PER;
-goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
+goalw thy [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
by (rtac refl 1);
qed "inst_fun_per";
(* Witness that quot is not empty *)
-goal thy "?z:{s.? r.!y.y:s=y===r}";
+goal thy "?z:{s.? r.!y. y:s=y===r}";
fr CollectI;
by (res_inst_tac [("x","x")] exI 1);
by (rtac allI 1);
--- a/src/HOL/Quot/PER0.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/PER0.thy Fri Oct 10 19:02:28 1997 +0200
@@ -27,9 +27,9 @@
D :: "'a::per set"
defs
per_def "(op ===) == eqv"
- Dom "D=={x.x===x}"
+ Dom "D=={x. x===x}"
(* define ==== on and function type => *)
- fun_per_def "eqv f g == !x y.x:D & y:D & x===y --> f x === g y"
+ fun_per_def "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
syntax (symbols)
"op ===" :: "['a,'a::per] => bool" (infixl "\\<sim>" 50)
--- a/src/HOL/Set.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Set.ML Fri Oct 10 19:02:28 1997 +0200
@@ -13,11 +13,11 @@
Addsimps [Collect_mem_eq];
AddIffs [mem_Collect_eq];
-goal Set.thy "!!a. P(a) ==> a : {x.P(x)}";
+goal Set.thy "!!a. P(a) ==> a : {x. P(x)}";
by (Asm_simp_tac 1);
qed "CollectI";
-val prems = goal Set.thy "!!a. a : {x.P(x)} ==> P(a)";
+val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
by (Asm_full_simp_tac 1);
qed "CollectD";
@@ -67,7 +67,7 @@
qed "bexI";
qed_goal "bexCI" Set.thy
- "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x)"
+ "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
@@ -82,12 +82,12 @@
AddSEs [bexE];
(*Trival rewrite rule*)
-goal Set.thy "(! x:A.P) = ((? x. x:A) --> P)";
+goal Set.thy "(! x:A. P) = ((? x. x:A) --> P)";
by (simp_tac (!simpset addsimps [Ball_def]) 1);
qed "ball_triv";
(*Dual form for existentials*)
-goal Set.thy "(? x:A.P) = ((? x. x:A) & P)";
+goal Set.thy "(? x:A. P) = ((? x. x:A) & P)";
by (simp_tac (!simpset addsimps [Bex_def]) 1);
qed "bex_triv";
@@ -113,7 +113,7 @@
section "Subsets";
-val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
+val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
by (REPEAT (ares_tac (prems @ [ballI]) 1));
qed "subsetI";
@@ -415,7 +415,7 @@
AddSDs [singleton_inject];
AddSEs [singletonE];
-goal Set.thy "{x.x=a} = {a}";
+goal Set.thy "{x. x=a} = {a}";
by(Blast_tac 1);
qed "singleton_conv";
Addsimps [singleton_conv];
@@ -606,7 +606,7 @@
(*The eta-expansion gives variable-name preservation.*)
val major::prems = goalw thy [image_def]
- "[| b : (%x.f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
+ "[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
by (rtac (major RS CollectD RS bexE) 1);
by (REPEAT (ares_tac prems 1));
qed "imageE";
@@ -632,7 +632,7 @@
bind_thm ("rangeI", UNIV_I RS imageI);
val [major,minor] = goal thy
- "[| b : range(%x.f(x)); !!x. b=f(x) ==> P |] ==> P";
+ "[| b : range(%x. f(x)); !!x. b=f(x) ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (etac minor 1);
qed "rangeE";
--- a/src/HOL/Set.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Set.thy Fri Oct 10 19:02:28 1997 +0200
@@ -125,8 +125,8 @@
(* Isomorphisms between Predicates and Sets *)
- mem_Collect_eq "(a : {x.P(x)}) = P(a)"
- Collect_mem_eq "{x.x:A} = A"
+ mem_Collect_eq "(a : {x. P(x)}) = P(a)"
+ Collect_mem_eq "{x. x:A} = A"
defs
@@ -136,18 +136,18 @@
subset_def "A <= B == ! x:A. x:B"
psubset_def "A < B == (A::'a set) <= B & ~ A=B"
Compl_def "Compl A == {x. ~x:A}"
- Un_def "A Un B == {x.x:A | x:B}"
- Int_def "A Int B == {x.x:A & x:B}"
+ Un_def "A Un B == {x. x:A | x:B}"
+ Int_def "A Int B == {x. x:A & x:B}"
set_diff_def "A - B == {x. x:A & ~x:B}"
INTER_def "INTER A B == {y. ! x:A. y: B(x)}"
UNION_def "UNION A B == {y. ? x:A. y: B(x)}"
- INTER1_def "INTER1 B == INTER {x.True} B"
- UNION1_def "UNION1 B == UNION {x.True} B"
+ INTER1_def "INTER1 B == INTER {x. True} B"
+ UNION1_def "UNION1 B == UNION {x. True} B"
Inter_def "Inter S == (INT x:S. x)"
Union_def "Union S == (UN x:S. x)"
Pow_def "Pow A == {B. B <= A}"
empty_def "{} == {x. False}"
- insert_def "insert a B == {x.x=a} Un B"
+ insert_def "insert a B == {x. x=a} Un B"
image_def "f``A == {y. ? x:A. y=f(x)}"
end
--- a/src/HOL/Subst/AList.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/AList.thy Fri Oct 10 19:02:28 1997 +0200
@@ -17,6 +17,6 @@
alist_rec_def "alist_rec al b c == list_rec b (split c) al"
- assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
+ assoc_def "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
end
--- a/src/HOL/Subst/Subst.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/Subst.ML Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
qed_spec_mp "Var_not_occs";
goal Subst.thy
- "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
+ "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_full_simp_tac);
by (ALLGOALS Blast_tac);
@@ -54,7 +54,7 @@
(**** Equality between Substitutions ****)
-goalw Subst.thy [subst_eq_def] "r =$= s = (! t.t <| r = t <| s)";
+goalw Subst.thy [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)";
by (Simp_tac 1);
qed "subst_eq_iff";
@@ -150,7 +150,7 @@
goalw Subst.thy [srange_def]
- "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
+ "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
by (Blast_tac 1);
qed "srange_iff";
@@ -186,12 +186,12 @@
qed_spec_mp "Var_intro";
goal Subst.thy
- "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
+ "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
by (simp_tac (!simpset addsimps [srange_iff]) 1);
qed_spec_mp "srangeD";
goal Subst.thy
- "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})";
+ "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
by (simp_tac (!simpset addsimps [empty_iff_all_not]) 1);
by (fast_tac (!claset addIs [Var_in_srange] addDs [srangeD]) 1);
qed "dom_range_disjoint";
--- a/src/HOL/Subst/Subst.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/Subst.thy Fri Oct 10 19:02:28 1997 +0200
@@ -26,7 +26,7 @@
defs
- subst_eq_def "r =$= s == ALL t.t <| r = t <| s"
+ subst_eq_def "r =$= s == ALL t. t <| r = t <| s"
comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
--- a/src/HOL/Sum.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Sum.ML Fri Oct 10 19:02:28 1997 +0200
@@ -194,7 +194,7 @@
by (etac IntD1 1);
qed "PartD1";
-goal Sum.thy "Part A (%x.x) = A";
+goal Sum.thy "Part A (%x. x) = A";
by (Blast_tac 1);
qed "Part_id";
@@ -203,6 +203,6 @@
qed "Part_Int";
(*For inductive definitions*)
-goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
+goal Sum.thy "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
by (Blast_tac 1);
qed "Part_Collect";
--- a/src/HOL/Sum.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Sum.thy Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
Part :: ['a set, 'b => 'a] => 'a set
translations
- "case p of Inl x => a | Inr y => b" == "sum_case (%x.a) (%y.b) p"
+ "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
defs
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
--- a/src/HOL/TLA/IntLemmas.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/IntLemmas.ML Fri Oct 10 19:02:28 1997 +0200
@@ -359,24 +359,24 @@
qed_goal "allEW" Intensional.thy
- "[| RALL x.P(x); P(x) ==> R |] ==> R::('w::world) form"
+ "[| RALL x. P(x); P(x) ==> R |] ==> R::('w::world) form"
(fn major::prems=>
[ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]);
qed_goal "all_dupEW" Intensional.thy
- "[| RALL x.P(x); [| P(x); RALL x.P(x) |] ==> R |] ==> R::('w::world) form"
+ "[| RALL x. P(x); [| P(x); RALL x. P(x) |] ==> R |] ==> R::('w::world) form"
(fn prems =>
[ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
-qed_goal "exIW" Intensional.thy "P(x) ==> REX x.P(x)"
+qed_goal "exIW" Intensional.thy "P(x) ==> REX x. P(x)"
(fn [prem] => [rtac intI 1,
rewrite_goals_tac intensional_rews,
rtac exI 1,
rtac (prem RS intD) 1]);
qed_goal "exEW" Intensional.thy
- "[| w |= REX x.P(x); !!x. P(x) .-> Q |] ==> w |= Q"
+ "[| w |= REX x. P(x); !!x. P(x) .-> Q |] ==> w |= Q"
(fn [major,minor] => [rtac exE 1,
rtac (rewrite_rule intensional_rews major) 1,
etac rev_mpW 1,
@@ -385,7 +385,7 @@
(** Classical quantifier reasoning **)
qed_goal "exCIW" Intensional.thy
- "(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x.P(x)"
+ "(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x. P(x)"
(fn prems => [cut_facts_tac prems 1,
rewrite_goals_tac intensional_rews,
fast_tac HOL_cs 1]);
--- a/src/HOL/TLA/Intensional.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/Intensional.ML Fri Oct 10 19:02:28 1997 +0200
@@ -35,7 +35,7 @@
"(P .| #True) .= #True", "(#True .| P) .= #True",
"(P .| #False) .= P", "(#False .| P) .= P",
"(P .| P) .= P", "(P .| .~P) .= #True", "(.~P .| P) .= #True",
- "(RALL x.P) .= P", "(REX x.P) .= P",
+ "(RALL x. P) .= P", "(REX x. P) .= P",
"(.~Q .-> .~P) .= (P .-> Q)",
"(P.|Q .-> R) .= ((P.->R).&(Q.->R))" ];
--- a/src/HOL/TLA/Stfun.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/Stfun.ML Fri Oct 10 19:02:28 1997 +0200
@@ -8,7 +8,7 @@
(* A stronger version of existential elimination (goal needn't be boolean) *)
qed_goalw "exE_prop" HOL.thy [Ex_def]
- "[| ? x::'a.P(x); !!x. P(x) ==> PROP R |] ==> PROP R"
+ "[| ? x::'a. P(x); !!x. P(x) ==> PROP R |] ==> PROP R"
(fn prems => [REPEAT(resolve_tac prems 1)]);
(* Might as well use that version in automated proofs *)
--- a/src/HOL/Univ.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Univ.ML Fri Oct 10 19:02:28 1997 +0200
@@ -439,23 +439,23 @@
(**** UN x. B(x) rules ****)
-goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
+goalw Univ.thy [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
by (Blast_tac 1);
qed "ntrunc_UN1";
-goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
+goalw Univ.thy [Scons_def] "(UN x. f(x)) $ M = (UN x. f(x) $ M)";
by (Blast_tac 1);
qed "Scons_UN1_x";
-goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
+goalw Univ.thy [Scons_def] "M $ (UN x. f(x)) = (UN x. M $ f(x))";
by (Blast_tac 1);
qed "Scons_UN1_y";
-goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
+goalw Univ.thy [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))";
by (rtac Scons_UN1_y 1);
qed "In0_UN1";
-goalw Univ.thy [In1_def] "In1(UN x.f(x)) = (UN x. In1(f(x)))";
+goalw Univ.thy [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))";
by (rtac Scons_UN1_y 1);
qed "In1_UN1";
--- a/src/HOL/W0/Maybe.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Maybe.thy Fri Oct 10 19:02:28 1997 +0200
@@ -15,6 +15,6 @@
"m bind f == case m of Ok r => f r | Fail => Fail"
syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "E bind (%P.F)"
+translations "P := E; F" == "E bind (%P. F)"
end
--- a/src/HOL/W0/Type.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Type.ML Fri Oct 10 19:02:28 1997 +0200
@@ -15,7 +15,7 @@
(* application of id_subst does not change type expression *)
goalw thy [id_subst_def]
- "$ id_subst = (%t::typ.t)";
+ "$ id_subst = (%t::typ. t)";
by (rtac ext 1);
by (typ.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
@@ -24,7 +24,7 @@
(* application of id_subst does not change list of type expressions *)
goalw thy [app_subst_list]
- "$ id_subst = (%ts::typ list.ts)";
+ "$ id_subst = (%ts::typ list. ts)";
by (rtac ext 1);
by (list.induct_tac "ts" 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/W0/Type.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Type.thy Fri Oct 10 19:02:28 1997 +0200
@@ -30,7 +30,7 @@
(* identity *)
constdefs
id_subst :: subst
- "id_subst == (%n.TVar n)"
+ "id_subst == (%n. TVar n)"
(* extension of substitution to type structures *)
consts
--- a/src/HOL/W0/W.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/W.ML Fri Oct 10 19:02:28 1997 +0200
@@ -237,7 +237,7 @@
(* case Abs e *)
by (strip_tac 1);
by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
+by (eres_inst_tac [("x","%x. if x=n then t1 else (s' x)")] allE 1);
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -268,9 +268,9 @@
(** LEVEL 35 **)
by (subgoal_tac
- "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
+ "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
\ else ra x)) ($ sa t) = \
-\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
+\ $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
\ else ra x)) (ta -> (TVar ma))" 1);
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
--- a/src/HOL/WF.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/WF.thy Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
constdefs
wf :: "('a * 'a)set => bool"
- "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
+ "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
acyclic :: "('a*'a)set => bool"
"acyclic r == !x. (x,x) ~: r^+"
--- a/src/HOL/cladata.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/cladata.ML Fri Oct 10 19:02:28 1997 +0200
@@ -68,7 +68,7 @@
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
qed_goal "alt_ex1E" thy
- "[| ?! x.P(x); \
+ "[| ?! x. P(x); \
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
\ |] ==> R"
(fn major::prems =>
--- a/src/HOL/datatype.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/datatype.ML Fri Oct 10 19:02:28 1997 +0200
@@ -341,7 +341,7 @@
fun t_inducting ((_, name, types, vns, _) :: cs) =
let
val h = if null types then " P(" ^ name ^ ")"
- else " !!" ^ (space_implode " " vns) ^ "." ^
+ else " !!" ^ (space_implode " " vns) ^ ". " ^
(assumpt (types, vns, false)) ^
"P(" ^ C_exp name vns ^ ")";
val rest = t_inducting cs;
--- a/src/HOL/equalities.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/equalities.ML Fri Oct 10 19:02:28 1997 +0200
@@ -12,7 +12,7 @@
section "{}";
-goal Set.thy "{x.False} = {}";
+goal Set.thy "{x. False} = {}";
by (Blast_tac 1);
qed "Collect_False_empty";
Addsimps [Collect_False_empty];
@@ -118,7 +118,7 @@
goalw Set.thy [image_def]
"(%x. if P x then f x else g x) `` S \
-\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
+\ = (f `` ({x. x:S & P x})) Un (g `` ({x. x:S & ~(P x)}))";
by (split_tac [expand_if] 1);
by (Blast_tac 1);
qed "if_image_distrib";
@@ -421,11 +421,11 @@
by (Blast_tac 1);
qed "INT1_insert_distrib";
-goal Set.thy "Union(range(f)) = (UN x.f(x))";
+goal Set.thy "Union(range(f)) = (UN x. f(x))";
by (Blast_tac 1);
qed "Union_range_eq";
-goal Set.thy "Inter(range(f)) = (INT x.f(x))";
+goal Set.thy "Inter(range(f)) = (INT x. f(x))";
by (Blast_tac 1);
qed "Inter_range_eq";
@@ -445,12 +445,12 @@
by (Blast_tac 1);
qed "INT_constant";
-goal Set.thy "(UN x.B) = B";
+goal Set.thy "(UN x. B) = B";
by (Blast_tac 1);
qed "UN1_constant";
Addsimps[UN1_constant];
-goal Set.thy "(INT x.B) = B";
+goal Set.thy "(INT x. B) = B";
by (Blast_tac 1);
qed "INT1_constant";
Addsimps[INT1_constant];
@@ -524,11 +524,11 @@
(** These are not added to the default simpset because (a) they duplicate the
body and (b) there are no similar rules for Int. **)
-goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
+goal Set.thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
by (Blast_tac 1);
qed "ball_Un";
-goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
+goal Set.thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
by (Blast_tac 1);
qed "bex_Un";
@@ -620,7 +620,7 @@
by (Blast_tac 1);
qed "set_eq_subset";
-goal Set.thy "A <= B = (! t.t:A --> t:B)";
+goal Set.thy "A <= B = (! t. t:A --> t:B)";
by (Blast_tac 1);
qed "subset_iff";
@@ -647,32 +647,32 @@
in
val UN1_simps = map prover
["(UN x. insert a (B x)) = insert a (UN x. B x)",
- "(UN x. A x Int B) = ((UN x.A x) Int B)",
- "(UN x. A Int B x) = (A Int (UN x.B x))",
- "(UN x. A x Un B) = ((UN x.A x) Un B)",
- "(UN x. A Un B x) = (A Un (UN x.B x))",
- "(UN x. A x - B) = ((UN x.A x) - B)",
- "(UN x. A - B x) = (A - (INT x.B x))"];
+ "(UN x. A x Int B) = ((UN x. A x) Int B)",
+ "(UN x. A Int B x) = (A Int (UN x. B x))",
+ "(UN x. A x Un B) = ((UN x. A x) Un B)",
+ "(UN x. A Un B x) = (A Un (UN x. B x))",
+ "(UN x. A x - B) = ((UN x. A x) - B)",
+ "(UN x. A - B x) = (A - (INT x. B x))"];
val INT1_simps = map prover
["(INT x. insert a (B x)) = insert a (INT x. B x)",
- "(INT x. A x Int B) = ((INT x.A x) Int B)",
- "(INT x. A Int B x) = (A Int (INT x.B x))",
- "(INT x. A x Un B) = ((INT x.A x) Un B)",
- "(INT x. A Un B x) = (A Un (INT x.B x))",
- "(INT x. A x - B) = ((INT x.A x) - B)",
- "(INT x. A - B x) = (A - (UN x.B x))"];
+ "(INT x. A x Int B) = ((INT x. A x) Int B)",
+ "(INT x. A Int B x) = (A Int (INT x. B x))",
+ "(INT x. A x Un B) = ((INT x. A x) Un B)",
+ "(INT x. A Un B x) = (A Un (INT x. B x))",
+ "(INT x. A x - B) = ((INT x. A x) - B)",
+ "(INT x. A - B x) = (A - (UN x. B x))"];
val UN_simps = map prover
- ["(UN x:C. A x Int B) = ((UN x:C.A x) Int B)",
- "(UN x:C. A Int B x) = (A Int (UN x:C.B x))",
- "(UN x:C. A x - B) = ((UN x:C.A x) - B)",
- "(UN x:C. A - B x) = (A - (INT x:C.B x))"];
+ ["(UN x:C. A x Int B) = ((UN x:C. A x) Int B)",
+ "(UN x:C. A Int B x) = (A Int (UN x:C. B x))",
+ "(UN x:C. A x - B) = ((UN x:C. A x) - B)",
+ "(UN x:C. A - B x) = (A - (INT x:C. B x))"];
val INT_simps = map prover
["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
- "(INT x:C. A x Un B) = ((INT x:C.A x) Un B)",
- "(INT x:C. A Un B x) = (A Un (INT x:C.B x))"];
+ "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)",
+ "(INT x:C. A Un B x) = (A Un (INT x:C. B x))"];
(*The missing laws for bounded Unions and Intersections are conditional
on the index set's being non-empty. Thus they are probably NOT worth
--- a/src/HOL/ex/MT.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/MT.ML Fri Oct 10 19:02:28 1997 +0200
@@ -66,7 +66,7 @@
qed "lfp_elim2";
val prems = goal MT.thy
- " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
+ " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
\ P(x)";
by (cut_facts_tac prems 1);
by (etac induct 1);
@@ -446,7 +446,7 @@
val prems = goal MT.thy
" te |- e ===> t ==> \
\ ( e = fn x1 => e1 --> \
-\ (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
+\ (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
\ )";
by (elab_e_elim_tac prems);
qed "elab_fn_elim_lem";
@@ -538,11 +538,11 @@
(* 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 \
+\ !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))";
@@ -558,11 +558,11 @@
val prems = goal MT.thy
" [| (v,t) : hasty_rel; \
-\ !! 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 \
+\ !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);
@@ -602,7 +602,7 @@
val prems = goalw MT.thy [hasty_env_def,hasty_def]
" v hasty t ==> \
\ ! x e ve. \
-\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
+\ v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
by (cut_facts_tac prems 1);
by (rtac hasty_rel_elim 1);
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
@@ -610,7 +610,7 @@
goal MT.thy
"!!t. v_clos(<|ev,e,ve|>) hasty t ==> \
-\ ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+\ ? te. te |- fn ev => e ===> t & ve hastyenv te ";
by (dtac hasty_elim_clos_lem 1);
by (Blast_tac 1);
qed "hasty_elim_clos";
--- a/src/HOL/ex/MT.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/MT.thy Fri Oct 10 19:02:28 1997 +0200
@@ -247,7 +247,7 @@
ve_dom(ve) = te_dom(te) &
( ! x.
x:ve_dom(ve) -->
- (? c.ve_app ve x = v_const(c) & c isof te_app te x)
+ (? c. ve_app ve x = v_const(c) & c isof te_app te x)
)
"
@@ -263,7 +263,7 @@
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)
)
}
"
--- a/src/HOL/ex/NatSum.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/NatSum.ML Fri Oct 10 19:02:28 1997 +0200
@@ -11,7 +11,7 @@
Addsimps [add_mult_distrib, add_mult_distrib2];
(*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
+goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
@@ -19,7 +19,7 @@
qed "sum_of_naturals";
goal NatSum.thy
- "Suc(Suc(Suc(Suc 2)))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
+ "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
@@ -27,7 +27,7 @@
qed "sum_of_squares";
goal NatSum.thy
- "Suc(Suc 2)*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
+ "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
@@ -35,7 +35,7 @@
qed "sum_of_cubes";
(*The sum of the first n odd numbers equals n squared.*)
-goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n";
+goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n";
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
--- a/src/HOL/ex/Puzzle.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Puzzle.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
*)
(*specialized form of induction needed below*)
-val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n.P(n)";
+val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
qed "nat_exh";
@@ -35,7 +35,7 @@
by (deepen_tac (!claset addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1);
qed "lemma2";
-val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
+val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
by (res_inst_tac[("n","n")]nat_induct 1);
by (Simp_tac 1);
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
--- a/src/HOL/ex/Qsort.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Qsort.ML Fri Oct 10 19:02:28 1997 +0200
@@ -35,7 +35,7 @@
Addsimps [set_qsort];
goal List.thy
- "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
+ "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed"Ball_set_filter";
--- a/src/HOL/ex/Recdef.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Recdef.thy Fri Oct 10 19:02:28 1997 +0200
@@ -94,9 +94,9 @@
TFL requires (%x.mapf x) instead of mapf.
*)
consts mapf :: nat => nat list
-recdef mapf "measure(%m.m)"
+recdef mapf "measure(%m. m)"
congs "[map_cong]"
"mapf 0 = []"
-"mapf (Suc n) = concat(map (%x.mapf x) (replicate n n))"
+"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
end
--- a/src/HOL/ex/Sorting.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Sorting.ML Fri Oct 10 19:02:28 1997 +0200
@@ -6,12 +6,12 @@
Some general lemmas
*)
-goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
+goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mset_append";
-goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
+goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
\ mset xs x";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
@@ -19,7 +19,7 @@
Addsimps [mset_append, mset_compl_add];
-goal Sorting.thy "set xs = {x.mset xs x ~= 0}";
+goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
by (list.induct_tac "xs" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by (Fast_tac 1);
--- a/src/HOL/ex/cla.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/cla.ML Fri Oct 10 19:02:28 1997 +0200
@@ -129,15 +129,15 @@
by (Blast_tac 1);
result();
-goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))";
+goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x. Q(x)))";
by (Blast_tac 1);
result();
-goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
+goal HOL.thy "(? x. P(x)-->Q) = ((! x. P(x)) --> Q)";
by (Blast_tac 1);
result();
-goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)";
+goal HOL.thy "((! x. P(x)) | Q) = (! x. P(x) | Q)";
by (Blast_tac 1);
result();
@@ -204,7 +204,7 @@
writeln"Problem 24";
goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \
-\ (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x)) \
+\ (~(? x. P(x)) --> (? x. Q(x))) & (! x. Q(x)|R(x) --> S(x)) \
\ --> (? x. P(x)&R(x))";
by (Blast_tac 1);
result();
@@ -237,7 +237,7 @@
writeln"Problem 28. AMENDED";
goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \
\ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \
-\ ((? x.S(x)) --> (! x. L(x) --> M(x))) \
+\ ((? x. S(x)) --> (! x. L(x) --> M(x))) \
\ --> (! x. P(x) & L(x) --> M(x))";
by (Blast_tac 1);
result();
@@ -257,7 +257,7 @@
result();
writeln"Problem 31";
-goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \
+goal HOL.thy "~(? x. P(x) & (Q(x) | R(x))) & \
\ (? x. L(x) & P(x)) & \
\ (! x. ~ R(x) --> M(x)) \
\ --> (? x. L(x) & M(x))";
@@ -303,7 +303,7 @@
writeln"Problem 37";
goal HOL.thy "(! z. ? w. ! x. ? y. \
-\ (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \
+\ (P x z -->P y w) & P y z & (P y w --> (? u. Q u w))) & \
\ (! x z. ~(P x z) --> (? y. Q y z)) & \
\ ((? x y. Q x y) --> (! x. R x x)) \
\ --> (! x. ? y. R x y)";
@@ -380,7 +380,7 @@
(*Hard because it involves substitution for Vars;
the type constraint ensures that x,y,z have the same type as a,b,u. *)
goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
-\ --> (! u::'a.P(u))";
+\ --> (! u::'a. P(u))";
by (Classical.safe_tac (!claset));
by (res_inst_tac [("x","a")] allE 1);
by (assume_tac 1);
@@ -391,7 +391,7 @@
writeln"Problem 50";
(*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
+goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
by (Blast_tac 1);
result();
--- a/src/HOL/ex/meson.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/meson.ML Fri Oct 10 19:02:28 1997 +0200
@@ -25,8 +25,8 @@
val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q";
val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q";
val not_notD = prove_fun "~~P ==> P";
-val not_allD = prove_fun "~(! x.P(x)) ==> ? x. ~P(x)";
-val not_exD = prove_fun "~(? x.P(x)) ==> ! x. ~P(x)";
+val not_allD = prove_fun "~(! x. P(x)) ==> ? x. ~P(x)";
+val not_exD = prove_fun "~(? x. P(x)) ==> ! x. ~P(x)";
(*** Removal of --> and <-> (positive and negative occurrences) ***)
@@ -44,17 +44,17 @@
(*** Conjunction ***)
-val conj_exD1 = prove_fun "(? x.P(x)) & Q ==> ? x. P(x) & Q";
-val conj_exD2 = prove_fun "P & (? x.Q(x)) ==> ? x. P & Q(x)";
+val conj_exD1 = prove_fun "(? x. P(x)) & Q ==> ? x. P(x) & Q";
+val conj_exD2 = prove_fun "P & (? x. Q(x)) ==> ? x. P & Q(x)";
(*** Disjunction ***)
(*DO NOT USE with forall-Skolemization: makes fewer schematic variables!!
With ex-Skolemization, makes fewer Skolem constants*)
-val disj_exD = prove_fun "(? x.P(x)) | (? x.Q(x)) ==> ? x. P(x) | Q(x)";
+val disj_exD = prove_fun "(? x. P(x)) | (? x. Q(x)) ==> ? x. P(x) | Q(x)";
-val disj_exD1 = prove_fun "(? x.P(x)) | Q ==> ? x. P(x) | Q";
-val disj_exD2 = prove_fun "P | (? x.Q(x)) ==> ? x. P | Q(x)";
+val disj_exD1 = prove_fun "(? x. P(x)) | Q ==> ? x. P(x) | Q";
+val disj_exD2 = prove_fun "P | (? x. Q(x)) ==> ? x. P | Q(x)";
(**** Skolemization -- pulling "?" over "!" ****)
--- a/src/HOL/ex/mesontest.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/mesontest.ML Fri Oct 10 19:02:28 1997 +0200
@@ -247,15 +247,15 @@
by (safe_meson_tac 1);
result();
-goal HOL.thy "(? x. P --> Q x) = (P --> (? x.Q x))";
+goal HOL.thy "(? x. P --> Q x) = (P --> (? x. Q x))";
by (safe_meson_tac 1);
result();
-goal HOL.thy "(? x.P x --> Q) = ((! x.P x) --> Q)";
+goal HOL.thy "(? x. P x --> Q) = ((! x. P x) --> Q)";
by (safe_meson_tac 1);
result();
-goal HOL.thy "((! x.P x) | Q) = (! x. P x | Q)";
+goal HOL.thy "((! x. P x) | Q) = (! x. P x | Q)";
by (safe_meson_tac 1);
result();
@@ -307,7 +307,7 @@
writeln"Problem 24"; (*The first goal clause is useless*)
goal HOL.thy "~(? x. S x & Q x) & (! x. P x --> Q x | R x) & \
-\ (~(? x.P x) --> (? x.Q x)) & (! x. Q x | R x --> S x) \
+\ (~(? x. P x) --> (? x. Q x)) & (! x. Q x | R x --> S x) \
\ --> (? x. P x & R x)";
by (safe_meson_tac 1);
result();
@@ -340,7 +340,7 @@
writeln"Problem 28. AMENDED"; (*14 Horn clauses*)
goal HOL.thy "(! x. P x --> (! x. Q x)) & \
\ ((! x. Q x | R x) --> (? x. Q x & S x)) & \
-\ ((? x.S x) --> (! x. L x --> M x)) \
+\ ((? x. S x) --> (! x. L x --> M x)) \
\ --> (! x. P x & L x --> M x)";
by (safe_meson_tac 1);
result();
@@ -361,7 +361,7 @@
result();
writeln"Problem 31"; (*10 Horn clauses; first negative clauses is useless*)
-goal HOL.thy "~(? x.P x & (Q x | R x)) & \
+goal HOL.thy "~(? x. P x & (Q x | R x)) & \
\ (? x. L x & P x) & \
\ (! x. ~ R x --> M x) \
\ --> (? x. L x & M x)";
@@ -407,7 +407,7 @@
writeln"Problem 37"; (*10 Horn clauses*)
goal HOL.thy "(! z. ? w. ! x. ? y. \
-\ (P x z --> P y w) & P y z & (P y w --> (? u.Q u w))) & \
+\ (P x z --> P y w) & P y z & (P y w --> (? u. Q u w))) & \
\ (! x z. ~P x z --> (? y. Q y z)) & \
\ ((? x y. Q x y) --> (! x. R x x)) \
\ --> (! x. ? y. R x y)";
@@ -475,7 +475,7 @@
writeln"Problem 46"; (*26 Horn clauses; 21-step proof*)
goal HOL.thy
"(! x. f x & (! y. f y & h y x --> g y) --> g x) & \
-\ ((? x.f x & ~g x) --> \
+\ ((? x. f x & ~g x) --> \
\ (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) & \
\ (! x y. f x & f y & h x y --> ~j y x) \
\ --> (! x. f x --> g x)";
@@ -486,22 +486,22 @@
writeln"Problem 47. Schubert's Steamroller";
(*26 clauses; 63 Horn clauses*)
goal HOL.thy
- "(! x. P1 x --> P0 x) & (? x.P1 x) & \
-\ (! x. P2 x --> P0 x) & (? x.P2 x) & \
-\ (! x. P3 x --> P0 x) & (? x.P3 x) & \
-\ (! x. P4 x --> P0 x) & (? x.P4 x) & \
-\ (! x. P5 x --> P0 x) & (? x.P5 x) & \
-\ (! x. Q1 x --> Q0 x) & (? x.Q1 x) & \
-\ (! x. P0 x --> ((! y.Q0 y-->R x y) | \
-\ (! y.P0 y & S y x & \
-\ (? z.Q0 z&R y z) --> R x y))) & \
+ "(! x. P1 x --> P0 x) & (? x. P1 x) & \
+\ (! x. P2 x --> P0 x) & (? x. P2 x) & \
+\ (! x. P3 x --> P0 x) & (? x. P3 x) & \
+\ (! x. P4 x --> P0 x) & (? x. P4 x) & \
+\ (! x. P5 x --> P0 x) & (? x. P5 x) & \
+\ (! x. Q1 x --> Q0 x) & (? x. Q1 x) & \
+\ (! x. P0 x --> ((! y. Q0 y-->R x y) | \
+\ (! y. P0 y & S y x & \
+\ (? z. Q0 z&R y z) --> R x y))) & \
\ (! x y. P3 y & (P5 x|P4 x) --> S x y) & \
\ (! x y. P3 x & P2 y --> S x y) & \
\ (! x y. P2 x & P1 y --> S x y) & \
\ (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) & \
\ (! x y. P3 x & P4 y --> R x y) & \
\ (! x y. P3 x & P5 y --> ~R x y) & \
-\ (! x. (P4 x|P5 x) --> (? y.Q0 y & R x y)) \
+\ (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y)) \
\ --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
by (safe_meson_tac 1); (*119 secs*)
result();
@@ -518,14 +518,14 @@
(*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \
\ (!x y z. Q x y --> Q y z --> Q x z) --> \
-\ (!x y.Q x y --> Q y x) --> (!x y. P x y | Q x y) --> \
-\ (!x y.P x y) | (!x y.Q x y)";
+\ (!x y. Q x y --> Q y x) --> (!x y. P x y | Q x y) --> \
+\ (!x y. P x y) | (!x y. Q x y)";
by (safe_best_meson_tac 1); (*2.7 secs*)
result();
writeln"Problem 50";
(*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
+goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
by (safe_meson_tac 1);
result();
--- a/src/HOL/ex/set.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/set.ML Fri Oct 10 19:02:28 1997 +0200
@@ -21,7 +21,7 @@
(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
-val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";
+val [prem] = goal HOL.thy "?!x. f(g(x))=x ==> ?!y. g(f(y))=y";
by (EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
result();
--- a/src/HOL/mono.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/mono.ML Fri Oct 10 19:02:28 1997 +0200
@@ -91,12 +91,12 @@
qed "imp_refl";
val [PQimp] = goal HOL.thy
- "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
+ "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
by (blast_tac (!claset addIs [PQimp RS mp]) 1);
qed "ex_mono";
val [PQimp] = goal HOL.thy
- "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
+ "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
by (blast_tac (!claset addIs [PQimp RS mp]) 1);
qed "all_mono";
--- a/src/HOL/simpdata.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/simpdata.ML Fri Oct 10 19:02:28 1997 +0200
@@ -102,7 +102,7 @@
"(P | False) = P", "(False | P) = P",
"(P | P) = P", "(P | (P | Q)) = (P | Q)",
"((~P) = (~Q)) = (P=Q)",
- "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x",
+ "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
"(? x. x=t & P(x)) = P(t)",
"(! x. t=x --> P(x)) = P(t)" ];
@@ -122,21 +122,21 @@
(*Miniscoping: pushing in existential quantifiers*)
val ex_simps = map prover
- ["(EX x. P x & Q) = ((EX x.P x) & Q)",
- "(EX x. P & Q x) = (P & (EX x.Q x))",
- "(EX x. P x | Q) = ((EX x.P x) | Q)",
- "(EX x. P | Q x) = (P | (EX x.Q x))",
- "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
- "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
+ ["(EX x. P x & Q) = ((EX x. P x) & Q)",
+ "(EX x. P & Q x) = (P & (EX x. Q x))",
+ "(EX x. P x | Q) = ((EX x. P x) | Q)",
+ "(EX x. P | Q x) = (P | (EX x. Q x))",
+ "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
+ "(EX x. P --> Q x) = (P --> (EX x. Q x))"];
(*Miniscoping: pushing in universal quantifiers*)
val all_simps = map prover
- ["(ALL x. P x & Q) = ((ALL x.P x) & Q)",
- "(ALL x. P & Q x) = (P & (ALL x.Q x))",
- "(ALL x. P x | Q) = ((ALL x.P x) | Q)",
- "(ALL x. P | Q x) = (P | (ALL x.Q x))",
- "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
- "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
+ ["(ALL x. P x & Q) = ((ALL x. P x) & Q)",
+ "(ALL x. P & Q x) = (P & (ALL x. Q x))",
+ "(ALL x. P x | Q) = ((ALL x. P x) | Q)",
+ "(ALL x. P | Q x) = (P | (ALL x. Q x))",
+ "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
+ "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
(*** Simplification procedure for turning ? x. ... & x = t & ...
into ? x. x = t & ... & ...
@@ -179,7 +179,7 @@
in Some(prove_eq ceqt) end)
| rearrange _ _ _ = None;
-val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
+val pattern = read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
in
val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
@@ -242,9 +242,9 @@
cases boil down to the same thing.*)
prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
-prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))";
+prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))";
prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)";
-prove "not_ex" "(~ (? x.P(x))) = (! x.~P(x))";
+prove "not_ex" "(~ (? x. P(x))) = (! x.~P(x))";
prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)";
prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
--- a/src/HOLCF/Cfun2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Cfun2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
+qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
(fn prems =>
[
(fold_goals_tac [less_cfun_def]),
@@ -30,7 +30,7 @@
(* Type 'a ->'b is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_cfun" thy "fabs(% x.UU) << f"
+qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
(fn prems =>
[
(stac less_cfun 1),
@@ -41,10 +41,10 @@
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
-qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
+qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
(fn prems =>
[
- (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
+ (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
(rtac (minimal_cfun RS allI) 1)
]);
@@ -156,7 +156,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun_mono" thy
- "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
+ "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -190,7 +190,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont_lubcfun" thy
- "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
+ "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -209,7 +209,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun" thy
- "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
+ "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cfun3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
open Cfun3;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x.UU)"
+qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x. UU)"
(fn prems =>
[
(simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
@@ -53,7 +53,7 @@
qed_goal "contlub_cfun_fun" thy
"is_chain(FY) ==>\
-\ lub(range FY)`x = lub(range (%i.FY(i)`x))"
+\ lub(range FY)`x = lub(range (%i. FY(i)`x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -67,7 +67,7 @@
qed_goal "cont_cfun_fun" thy
"is_chain(FY) ==>\
-\ range(%i.FY(i)`x) <<| lub(range FY)`x"
+\ range(%i. FY(i)`x) <<| lub(range FY)`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -83,7 +83,7 @@
qed_goal "contlub_cfun" thy
"[|is_chain(FY);is_chain(TY)|] ==>\
-\ (lub(range FY))`(lub(range TY)) = lub(range(%i.FY(i)`(TY i)))"
+\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -117,7 +117,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont2cont_fapp" thy
- "[|cont(%x.ft x);cont(%x.tt x)|] ==> cont(%x. (ft x)`(tt x))"
+ "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -137,7 +137,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont2mono_LAM" thy
- "[| !!x.cont(c1 x); !!y.monofun(%x.c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
+ "[| !!x. cont(c1 x); !!y. monofun(%x. c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
(fn [p1,p2] =>
[
(rtac monofunI 1),
@@ -157,7 +157,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont2cont_LAM" thy
- "[| !!x.cont(c1 x); !!y.cont(%x.c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
+ "[| !!x. cont(c1 x); !!y. cont(%x. c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
(fn [p1,p2] =>
[
(rtac monocontlub2cont 1),
@@ -393,7 +393,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "iso_strict" thy
-"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
+"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
\ ==> f`UU=UU & g`UU=UU"
(fn prems =>
[
@@ -410,7 +410,7 @@
qed_goal "isorep_defined" thy
- "[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
+ "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -424,7 +424,7 @@
]);
qed_goal "isoabs_defined" thy
- "[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
+ "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -442,14 +442,14 @@
(* ------------------------------------------------------------------------ *)
qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
-\ !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a::chfin) |] \
+\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
\ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
(fn prems =>
[
(rewtac max_in_chain_def),
(strip_tac 1),
(rtac exE 1),
- (res_inst_tac [("P","is_chain(%i.g`(Y i))")] mp 1),
+ (res_inst_tac [("P","is_chain(%i. g`(Y i))")] mp 1),
(etac spec 1),
(etac ch2ch_fappR 1),
(rtac exI 1),
@@ -465,8 +465,8 @@
]);
-qed_goal "flat2flat" thy "!!f g.[|!x y::'a.x<<y --> x=UU | x=y; \
-\ !y.f`(g`y)=(y::'b); !x.g`(f`x)=(x::'a)|] ==> !x y::'b.x<<y --> x=UU | x=y"
+qed_goal "flat2flat" thy "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
+\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y"
(fn prems =>
[
(strip_tac 1),
@@ -496,7 +496,7 @@
(* ------------------------------------------------------------------------- *)
qed_goal "flat_codom" thy
-"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -534,7 +534,7 @@
(rtac refl 1)
]);
-qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
+qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x. f`(g`x))" (fn _ => [
(stac beta_cfun 1),
(Simp_tac 1),
(stac beta_cfun 1),
--- a/src/HOLCF/Cfun3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
defs
Istrictify_def "Istrictify f x == if x=UU then UU else f`x"
-strictify_def "strictify == (LAM f x.Istrictify f x)"
+strictify_def "strictify == (LAM f x. Istrictify f x)"
consts
ID :: "('a::cpo) -> 'a"
@@ -32,7 +32,7 @@
defs
- ID_def "ID ==(LAM x.x)"
- oo_def "cfcomp == (LAM f g x.f`(g`x))"
+ ID_def "ID ==(LAM x. x)"
+ oo_def "cfcomp == (LAM f g x. f`(g`x))"
end
--- a/src/HOLCF/Cont.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cont.ML Fri Oct 10 19:02:28 1997 +0200
@@ -32,7 +32,7 @@
qed_goalw "contI" thy [cont]
- "! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
+ "! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -40,7 +40,7 @@
]);
qed_goalw "contE" thy [cont]
- "cont(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+ "cont(f) ==> ! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -89,7 +89,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ub2ub_monofun" thy
- "[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)"
+ "[| monofun(f); range(Y) <| u|] ==> range(%i. f(Y(i))) <| f(u)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -213,7 +213,7 @@
]);
qed_goal "ch2ch_MF2LR" thy
-"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
+"[|monofun(MF2); !f. monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
\ is_chain(%i. MF2(F(i))(Y(i)))"
(fn prems =>
[
@@ -230,7 +230,7 @@
qed_goal "ch2ch_lubMF2R" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(F);is_chain(Y)|] ==> \
\ is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
(fn prems =>
@@ -250,7 +250,7 @@
qed_goal "ch2ch_lubMF2L" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(F);is_chain(Y)|] ==> \
\ is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
(fn prems =>
@@ -270,9 +270,9 @@
qed_goal "lub_MF2_mono" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(F)|] ==> \
-\ monofun(% x.lub(range(% j.MF2 (F j) (x))))"
+\ monofun(% x. lub(range(% j. MF2 (F j) (x))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -290,7 +290,7 @@
qed_goal "ex_lubMF2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(F); is_chain(Y)|] ==> \
\ lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
\ lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
@@ -329,7 +329,7 @@
qed_goal "diag_lubMF2_1" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -373,7 +373,7 @@
qed_goal "diag_lubMF2_2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\ !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -394,8 +394,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_CF2" thy
-"[|cont(CF2);!f.cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
+"[|cont(CF2);!f. cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -486,7 +486,7 @@
(********* Note "(%x.%y.c1 x y) = c1" ***********)
qed_goal "mono2mono_MF1L_rev" thy
- "!y.monofun(%x.c1 x y) ==> monofun(c1)"
+ "!y. monofun(%x. c1 x y) ==> monofun(c1)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -499,7 +499,7 @@
]);
qed_goal "cont2cont_CF1L_rev" thy
- "!y.cont(%x.c1 x y) ==> cont(c1)"
+ "!y. cont(%x. c1 x y) ==> cont(c1)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -524,8 +524,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
-\ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
+"[|is_chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
+\ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -540,7 +540,7 @@
]);
qed_goal "mono2mono_app" thy
-"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
+"[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
\ monofun(%x.(ft(x))(tt(x)))"
(fn prems =>
[
@@ -558,7 +558,7 @@
qed_goal "cont2contlub_app" thy
-"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
+"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -575,7 +575,7 @@
qed_goal "cont2cont_app" thy
-"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\
+"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==>\
\ cont(%x.(ft(x))(tt(x)))"
(fn prems =>
[
@@ -605,7 +605,7 @@
(* The identity function is continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_id" thy "cont(% x.x)"
+qed_goal "cont_id" thy "cont(% x. x)"
(fn prems =>
[
(rtac contI 1),
@@ -618,7 +618,7 @@
(* constant functions are continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont_const" thy [cont] "cont(%x.c)"
+qed_goalw "cont_const" thy [cont] "cont(%x. c)"
(fn prems =>
[
(strip_tac 1),
--- a/src/HOLCF/Cont.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cont.thy Fri Oct 10 19:02:28 1997 +0200
@@ -28,10 +28,10 @@
monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
contlub "contlub(f) == ! Y. is_chain(Y) -->
- f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
+ f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
cont "cont(f) == ! Y. is_chain(Y) -->
- range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+ range(% i. f(Y(i))) <<| f(lub(range(Y)))"
(* ------------------------------------------------------------------------ *)
(* the main purpose of cont.thy is to show: *)
--- a/src/HOLCF/Cprod2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Cprod2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cprod_po" thy "(op <<)=(%x y.fst x<<fst y & snd x<<snd y)"
+qed_goal "inst_cprod_po" thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
(fn prems =>
[
(fold_goals_tac [less_cprod_def]),
@@ -45,7 +45,7 @@
bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
-qed_goal "least_cprod" thy "? x::'a*'b.!y.x<<y"
+qed_goal "least_cprod" thy "? x::'a*'b.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","(UU,UU)")] exI 1),
@@ -116,7 +116,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cprod" thy
-"is_chain S ==> range S<<|(lub(range(%i.fst(S i))),lub(range(%i.snd(S i))))"
+"is_chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -147,7 +147,7 @@
*)
-qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x.range S<<| x"
+qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cprod3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -262,7 +262,7 @@
qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
"[|is_chain(S)|] ==> range(S) <<| \
-\ <(lub(range(%i.cfst`(S i)))) , lub(range(%i.csnd`(S i)))>"
+\ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cprod3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -26,9 +26,9 @@
defs
cpair_def "cpair == (LAM x y.(x,y))"
-cfst_def "cfst == (LAM p.fst(p))"
-csnd_def "csnd == (LAM p.snd(p))"
-csplit_def "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
+cfst_def "cfst == (LAM p. fst(p))"
+csnd_def "csnd == (LAM p. snd(p))"
+csplit_def "csplit == (LAM f p. f`(cfst`p)`(csnd`p))"
@@ -43,7 +43,7 @@
constdefs
CLet :: "'a -> ('a -> 'b) -> 'b"
- "CLet == LAM s f.f`s"
+ "CLet == LAM s f. f`s"
(* syntax for Let *)
@@ -59,7 +59,7 @@
translations
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)"
- "Let x = a in e" == "CLet`a`(LAM x.e)"
+ "Let x = a in e" == "CLet`a`(LAM x. e)"
(* syntax for LAM <x,y,z>.e *)
--- a/src/HOLCF/Discrete.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Discrete.ML Fri Oct 10 19:02:28 1997 +0200
@@ -10,11 +10,11 @@
Addsimps [undiscr_Discr];
goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i.f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
by(fast_tac (!claset addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
-goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr.f x)";
+goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];
--- a/src/HOLCF/Fix.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fix.ML Fri Oct 10 19:02:28 1997 +0200
@@ -43,7 +43,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "is_chain_iterate2" thy [is_chain]
- " x << F`x ==> is_chain (%i.iterate i F x)"
+ " x << F`x ==> is_chain (%i. iterate i F x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -57,7 +57,7 @@
qed_goal "is_chain_iterate" thy
- "is_chain (%i.iterate i F UU)"
+ "is_chain (%i. iterate i F UU)"
(fn prems =>
[
(rtac is_chain_iterate2 1),
@@ -452,16 +452,16 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "admI" thy [adm_def]
- "(!!Y. [| is_chain(Y); !i.P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
+ "(!!Y. [| is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
(fn prems => [fast_tac (HOL_cs addIs prems) 1]);
qed_goalw "admD" thy [adm_def]
- "!!P. [| adm(P); is_chain(Y); !i.P(Y(i)) |] ==> P(lub(range(Y)))"
+ "!!P. [| adm(P); is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
(fn prems => [fast_tac HOL_cs 1]);
qed_goalw "admw_def2" thy [admw_def]
- "admw(P) = (!F.(!n.P(iterate n F UU)) -->\
-\ P (lub(range(%i.iterate i F UU))))"
+ "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
+\ P (lub(range(%i. iterate i F UU))))"
(fn prems =>
[
(rtac refl 1)
@@ -537,7 +537,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "adm_max_in_chain" thy [adm_def]
-"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain n Y) ==> adm(P::'a=>bool)"
+"!Y. is_chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -585,7 +585,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "adm_less" thy [adm_def]
- "[|cont u;cont v|]==> adm(%x.u x << v x)"
+ "[|cont u;cont v|]==> adm(%x. u x << v x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -610,7 +610,7 @@
(fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
Addsimps [adm_conj];
-qed_goalw "adm_not_free" thy [adm_def] "adm(%x.t)"
+qed_goalw "adm_not_free" thy [adm_def] "adm(%x. t)"
(fn prems => [fast_tac HOL_cs 1]);
Addsimps [adm_not_free];
@@ -629,7 +629,7 @@
]);
qed_goal "adm_all" thy
- "!!P. !y.adm(P y) ==> adm(%x.!y.P y x)"
+ "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
(fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
bind_thm ("adm_all2", allI RS adm_all);
@@ -681,7 +681,7 @@
local
val adm_disj_lemma1 = prove_goal HOL.thy
- "!n.P(Y n)|Q(Y n) ==> (? i.!j.R i j --> Q(Y(j))) | (!i.? j.R i j & P(Y(j)))"
+ "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -689,7 +689,7 @@
]);
val adm_disj_lemma2 = prove_goal thy
- "!!Q. [| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
+ "!!Q. [| adm(Q); ? X. is_chain(X) & (!n. Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
(fn _ => [fast_tac (!claset addEs [admD] addss !simpset) 1]);
@@ -735,7 +735,7 @@
[
(cut_facts_tac prems 1),
(etac exE 1),
- (res_inst_tac [("x","%m.if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
+ (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
(rtac conjI 1),
(rtac adm_disj_lemma3 1),
(atac 1),
@@ -854,7 +854,7 @@
]);
val adm_disj = prove_goal thy
- "!!P. [| adm P; adm Q |] ==> adm(%x.P x | Q x)"
+ "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
(fn prems =>
[
(rtac admI 1),
@@ -876,10 +876,10 @@
bind_thm("adm_disj",adm_disj);
qed_goal "adm_imp" thy
- "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
+ "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
(fn prems =>
[
- (subgoal_tac "(%x.P x --> Q x) = (%x. ~P x | Q x)" 1),
+ (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
(Asm_simp_tac 1),
(etac adm_disj 1),
(atac 1),
@@ -887,9 +887,9 @@
(fast_tac HOL_cs 1)
]);
-goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x.Q x --> P x) |] \
+goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
\ ==> adm (%x. P x = Q x)";
-by(subgoal_tac "(%x.P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
+by(subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
by (Asm_simp_tac 1);
by (rtac ext 1);
by (fast_tac HOL_cs 1);
--- a/src/HOLCF/Fix.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fix.thy Fri Oct 10 19:02:28 1997 +0200
@@ -20,14 +20,14 @@
defs
-iterate_def "iterate n F c == nat_rec c (%n x.F`x) n"
-Ifix_def "Ifix F == lub(range(%i.iterate i F UU))"
+iterate_def "iterate n F c == nat_rec c (%n x. F`x) n"
+Ifix_def "Ifix F == lub(range(%i. iterate i F UU))"
fix_def "fix == (LAM f. Ifix f)"
adm_def "adm P == !Y. is_chain(Y) -->
- (!i.P(Y i)) --> P(lub(range Y))"
+ (!i. P(Y i)) --> P(lub(range Y))"
-admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
+admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
P (lub(range (%i. iterate i F UU)))"
end
--- a/src/HOLCF/Fun2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fun2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Fun2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
+qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x. f x << g x)"
(fn prems =>
[
(fold_goals_tac [less_fun_def]),
@@ -20,7 +20,7 @@
(* Type 'a::term => 'b::pcpo is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_fun" thy "(%z.UU) << x"
+qed_goal "minimal_fun" thy "(%z. UU) << x"
(fn prems =>
[
(simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1)
@@ -28,10 +28,10 @@
bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
-qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y.x<<y"
+qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y. x<<y"
(fn prems =>
[
- (res_inst_tac [("x","(%z.UU)")] exI 1),
+ (res_inst_tac [("x","(%z. UU)")] exI 1),
(rtac (minimal_fun RS allI) 1)
]);
@@ -52,7 +52,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_fun" thy
- "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i.S(i)(x))"
+ "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i. S(i)(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -87,7 +87,7 @@
qed_goal "lub_fun" Fun2.thy
"is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
-\ range(S) <<| (% x.lub(range(% i.S(i)(x))))"
+\ range(S) <<| (% x. lub(range(% i. S(i)(x))))"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Fun3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fun3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
open Fun3;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
+qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
(fn prems =>
[
(simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
--- a/src/HOLCF/IMP/Denotational.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.thy Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
constdefs
dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
- "dlift f == (LAM x.case x of Undef => UU | Def(y) => f`(Discr y))"
+ "dlift f == (LAM x. case x of Undef => UU | Def(y) => f`(Discr y))"
consts D :: "com => state discr -> state lift"
--- a/src/HOLCF/IOA/ABP/Correctness.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Fri Oct 10 19:02:28 1997 +0200
@@ -6,7 +6,7 @@
*)
-goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
+goal Abschannel.thy "(? x. x=P & Q(x)) = Q(P)";
by (Fast_tac 1);
qed"exis_elim";
@@ -209,7 +209,7 @@
(* 3 thms that do not hold generally! The lucky restriction here is
the absence of internal actions. *)
goal Correctness.thy
- "is_weak_ref_map (%id.id) sender_ioa sender_ioa";
+ "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
@@ -225,7 +225,7 @@
(* 2 copies of before *)
goal Correctness.thy
- "is_weak_ref_map (%id.id) receiver_ioa receiver_ioa";
+ "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
@@ -240,7 +240,7 @@
qed"receiver_unchanged";
goal Correctness.thy
- "is_weak_ref_map (%id.id) env_ioa env_ioa";
+ "is_weak_ref_map (%id. id) env_ioa env_ioa";
by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Oct 10 19:02:28 1997 +0200
@@ -193,7 +193,7 @@
(* --------------------------------------------------------------------- *)
goal thy "!s. (is_exec_frag (A||B) (s,xs) \
-\ --> Forall (%x.fst x:act (A||B)) xs)";
+\ --> Forall (%x. fst x:act (A||B)) xs)";
by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
(* main case *)
@@ -212,7 +212,7 @@
\ is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
\ stutter (asig_of A) (fst s,(ProjA2`xs)) & \
\ stutter (asig_of B) (snd s,(ProjB2`xs)) & \
-\ Forall (%x.fst x:act (A||B)) xs \
+\ Forall (%x. fst x:act (A||B)) xs \
\ --> is_exec_frag (A||B) (s,xs)";
by (pair_induct_tac "xs" [Forall_def,sforall_def,
@@ -242,7 +242,7 @@
\(Filter_ex (asig_of A) (ProjA ex) : executions A &\
\ Filter_ex (asig_of B) (ProjB ex) : executions B &\
\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
-\ Forall (%x.fst x:act (A||B)) (snd ex))";
+\ Forall (%x. fst x:act (A||B)) (snd ex))";
by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
Filter_ex_def,ProjA_def,starts_of_par]) 1);
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Oct 10 19:02:28 1997 +0200
@@ -45,7 +45,7 @@
Filter_ex2_def
- "Filter_ex2 sig == Filter (%x.fst x:actions sig)"
+ "Filter_ex2 sig == Filter (%x. fst x:actions sig)"
stutter_def
"stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
@@ -70,7 +70,7 @@
Int {ex. Filter_ex sigB (ProjB ex) : exB}
Int {ex. stutter sigA (ProjA ex)}
Int {ex. stutter sigB (ProjB ex)}
- Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
+ Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
asig_comp sigA sigB)"
end
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Fri Oct 10 19:02:28 1997 +0200
@@ -160,7 +160,7 @@
goalw thy [filter_act_def,Filter_ex2_def]
"filter_act`(Filter_ex2 (asig_of A)`xs)=\
-\ Filter (%a.a:act A)`(filter_act`xs)";
+\ Filter (%a. a:act A)`(filter_act`xs)";
by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
qed"lemma_2_1a";
@@ -187,7 +187,7 @@
is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\ --> Forall (%x.x:act (A||B)) (filter_act`xs)";
+\ --> Forall (%x. x:act (A||B)) (filter_act`xs)";
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
@@ -207,9 +207,9 @@
--------------------------------------------------------------------------- *)
goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
@@ -270,9 +270,9 @@
goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -281,9 +281,9 @@
goal thy "!! sch.[| \
-\ Forall (%x.x:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ Forall (%x. x:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
\ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
by (cut_facts_tac [stutterA_mkex] 1);
@@ -301,9 +301,9 @@
--------------------------------------------------------------------------- *)
goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -312,9 +312,9 @@
goal thy "!! sch.[| \
-\ Forall (%x.x:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ Forall (%x. x:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
\ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
by (cut_facts_tac [stutterB_mkex] 1);
@@ -334,11 +334,11 @@
--------------------------------------------------------------------------- *)
goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
-\ Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
+\ Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -360,8 +360,8 @@
--------------------------------------------------------------------------- *)
goal thy "!! sch ex. \
-\ Filter (%a.a:act AB)`sch = filter_act`ex \
-\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)";
+\ Filter (%a. a:act AB)`sch = filter_act`ex \
+\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
by (rtac (Zip_Map_fst_snd RS sym) 1);
qed"trick_against_eq_in_ass";
@@ -373,9 +373,9 @@
goal thy "!!sch exA exB.\
-\ [| Forall (%a.a:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ [| Forall (%a. a:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
\ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
@@ -398,11 +398,11 @@
goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
-\ Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
+\ Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
(* notice necessary change of arguments exA and exB *)
by (mkex_induct_tac "sch" "exB" "exA");
@@ -417,9 +417,9 @@
goal thy "!!sch exA exB.\
-\ [| Forall (%a.a:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ [| Forall (%a. a:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
\ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
@@ -439,9 +439,9 @@
goal thy "!s t exA exB. \
\ Forall (%x. x : act (A || B)) sch &\
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> Forall (%x.fst x : act (A ||B)) \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
+\ --> Forall (%x. fst x : act (A ||B)) \
\ (snd (mkex A B sch (s,exA) (t,exB)))";
by (mkex_induct_tac "sch" "exA" "exB");
@@ -456,8 +456,8 @@
goal thy
"sch : schedules (A||B) = \
-\ (Filter (%a.a:act A)`sch : schedules A &\
-\ Filter (%a.a:act B)`sch : schedules B &\
+\ (Filter (%a. a:act A)`sch : schedules A &\
+\ Filter (%a. a:act B)`sch : schedules B &\
\ Forall (%x. x:act (A||B)) sch)";
by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Oct 10 19:02:28 1997 +0200
@@ -67,8 +67,8 @@
let schA = fst SchedsA; sigA = snd SchedsA;
schB = fst SchedsB; sigB = snd SchedsB
in
- ( {sch. Filter (%a.a:actions sigA)`sch : schA}
- Int {sch. Filter (%a.a:actions sigB)`sch : schB}
+ ( {sch. Filter (%a. a:actions sigA)`sch : schA}
+ Int {sch. Filter (%a. a:actions sigB)`sch : schB}
Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
asig_comp sigA sigB)"
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Fri Oct 10 19:02:28 1997 +0200
@@ -24,24 +24,24 @@
\ | Def y => \
\ (if y:act A then \
\ (if y:act B then \
-\ ((Takewhile (%a.a:int A)`schA) \
-\ @@(Takewhile (%a.a:int B)`schB) \
+\ ((Takewhile (%a. a:int A)`schA) \
+\ @@(Takewhile (%a. a:int B)`schB) \
\ @@(y>>(mksch A B`xs \
-\ `(TL`(Dropwhile (%a.a:int A)`schA)) \
-\ `(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ `(TL`(Dropwhile (%a. a:int A)`schA)) \
+\ `(TL`(Dropwhile (%a. a:int B)`schB)) \
\ ))) \
\ else \
-\ ((Takewhile (%a.a:int A)`schA) \
+\ ((Takewhile (%a. a:int A)`schA) \
\ @@ (y>>(mksch A B`xs \
-\ `(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ `(TL`(Dropwhile (%a. a:int A)`schA)) \
\ `schB))) \
\ ) \
\ else \
\ (if y:act B then \
-\ ((Takewhile (%a.a:int B)`schB) \
+\ ((Takewhile (%a. a:int B)`schB) \
\ @@ (y>>(mksch A B`xs \
\ `schA \
-\ `(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ `(TL`(Dropwhile (%a. a:int B)`schB)) \
\ ))) \
\ else \
\ UU \
@@ -62,8 +62,8 @@
goal thy "!!x.[|x:act A;x~:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
-\ (Takewhile (%a.a:int A)`schA) \
-\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ (Takewhile (%a. a:int A)`schA) \
+\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
\ `schB))";
by (rtac trans 1);
by (stac mksch_unfold 1);
@@ -73,8 +73,8 @@
goal thy "!!x.[|x~:act A;x:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
-\ (Takewhile (%a.a:int B)`schB) \
-\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ (Takewhile (%a. a:int B)`schB) \
+\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB)) \
\ ))";
by (rtac trans 1);
by (stac mksch_unfold 1);
@@ -84,10 +84,10 @@
goal thy "!!x.[|x:act A;x:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
-\ (Takewhile (%a.a:int A)`schA) \
-\ @@ ((Takewhile (%a.a:int B)`schB) \
-\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
-\ `(TL`(Dropwhile (%a.a:int B)`schB)))) \
+\ (Takewhile (%a. a:int A)`schA) \
+\ @@ ((Takewhile (%a. a:int B)`schB) \
+\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
+\ `(TL`(Dropwhile (%a. a:int B)`schB)))) \
\ )";
by (rtac trans 1);
by (stac mksch_unfold 1);
@@ -208,7 +208,7 @@
Delsimps [FiniteConc];
goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ ! x y. Forall (%x.x:act A) x & Forall (%x.x:act B) y & \
+\ ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
\ Forall (%x. x:ext (A||B)) tr \
@@ -283,7 +283,7 @@
Delsimps [FilterConc];
goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
-\! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
+\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
\ Forall (%x. x:act B & x~:act A) y1 & \
@@ -312,7 +312,7 @@
Addsimps [FilterConc];
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int B)`y)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
@@ -321,7 +321,7 @@
by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
(* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int B)`y @@ a>>y1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
by (res_inst_tac [("x","y2")] exI 1);
(* elminate all obligations up to two depending on Conc_assoc *)
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -338,7 +338,7 @@
goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
-\! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\
+\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
\ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
\ Forall (%x. x:act A & x~:act B) x1 & \
@@ -367,7 +367,7 @@
Addsimps [FilterConc];
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int A)`x)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
@@ -376,7 +376,7 @@
by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
(* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int A)`x @@ a>>x1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
by (res_inst_tac [("x","x2")] exI 1);
(* elminate all obligations up to two depending on Conc_assoc *)
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -434,7 +434,7 @@
by (rotate_tac ~2 2);
by (rotate_tac ~2 3);
by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
-by (eres_inst_tac [("x","sb@@Takewhile (%a.a: int A)`a @@ Takewhile (%a.a:int B)`b@@(aaa>>nil)")] allE 2);
+by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
by (eres_inst_tac [("x","sa")] allE 2);
by (asm_full_simp_tac (!simpset addsimps [Conc_assoc])2);
@@ -481,11 +481,11 @@
goal thy
"!! A B. [| compatible A B; compatible B A;\
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
-\ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB \
-\ --> Filter (%a.a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
+\ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
+\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB \
+\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
@@ -557,12 +557,12 @@
goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
\ LastActExtsch A schA & LastActExtsch B schB \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
by (REPEAT (etac conjE 1));
@@ -613,7 +613,7 @@
(* eliminate the B-only prefix *)
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
by (etac ForallQFilterPnil 2);
by (assume_tac 2);
by (Fast_tac 2);
@@ -691,12 +691,12 @@
goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
\ LastActExtsch A schA & LastActExtsch B schB \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
by (strip_tac 1);
by (rtac seq.take_lemma 1);
@@ -730,7 +730,7 @@
(* second side: schA = nil *)
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1);
by (assume_tac 1);
by (Fast_tac 1);
@@ -747,7 +747,7 @@
(* schA = UU *)
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
by (assume_tac 1);
by (Fast_tac 1);
@@ -771,7 +771,7 @@
(* eliminate the B-only prefix *)
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
by (etac ForallQFilterPnil 2);
by (assume_tac 2);
by (Fast_tac 2);
@@ -833,7 +833,7 @@
(* assumption Forall schA *)
by (dres_inst_tac [("s","schA"),
- ("P","Forall (%x.x:act A)")] subst 1);
+ ("P","Forall (%x. x:act A)")] subst 1);
by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
@@ -933,12 +933,12 @@
goal thy "!! A B. [| compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
\ LastActExtsch A schA & LastActExtsch B schB \
-\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
+\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
by (strip_tac 1);
by (rtac seq.take_lemma 1);
@@ -972,7 +972,7 @@
(* second side: schA = nil *)
by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1);
by (assume_tac 1);
by (Fast_tac 1);
@@ -989,7 +989,7 @@
(* schA = UU *)
by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1);
by (assume_tac 1);
by (Fast_tac 1);
@@ -1013,7 +1013,7 @@
(* eliminate the A-only prefix *)
-by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
by (etac ForallQFilterPnil 2);
by (assume_tac 2);
by (Fast_tac 2);
@@ -1075,7 +1075,7 @@
(* assumption Forall schB *)
by (dres_inst_tac [("s","schB"),
- ("P","Forall (%x.x:act B)")] subst 1);
+ ("P","Forall (%x. x:act B)")] subst 1);
by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
@@ -1173,8 +1173,8 @@
"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
\ is_asig(asig_of A); is_asig(asig_of B)|] \
\ ==> tr: traces(A||B) = \
-\ (Filter (%a.a:act A)`tr : traces A &\
-\ Filter (%a.a:act B)`tr : traces B &\
+\ (Filter (%a. a:act A)`tr : traces A &\
+\ Filter (%a. a:act B)`tr : traces B &\
\ Forall (%x. x:ext(A||B)) tr)";
by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
@@ -1182,12 +1182,12 @@
(* ==> *)
(* There is a schedule of A *)
-by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
externals_of_par,ext1_ext2_is_not_act1]) 1);
(* There is a schedule of B *)
-by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
externals_of_par,ext1_ext2_is_not_act2]) 1);
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Oct 10 19:02:28 1997 +0200
@@ -25,24 +25,24 @@
| Def y =>
(if y:act A then
(if y:act B then
- ((Takewhile (%a.a:int A)`schA)
- @@ (Takewhile (%a.a:int B)`schB)
+ ((Takewhile (%a. a:int A)`schA)
+ @@ (Takewhile (%a. a:int B)`schB)
@@ (y>>(h`xs
- `(TL`(Dropwhile (%a.a:int A)`schA))
- `(TL`(Dropwhile (%a.a:int B)`schB))
+ `(TL`(Dropwhile (%a. a:int A)`schA))
+ `(TL`(Dropwhile (%a. a:int B)`schB))
)))
else
- ((Takewhile (%a.a:int A)`schA)
+ ((Takewhile (%a. a:int A)`schA)
@@ (y>>(h`xs
- `(TL`(Dropwhile (%a.a:int A)`schA))
+ `(TL`(Dropwhile (%a. a:int A)`schA))
`schB)))
)
else
(if y:act B then
- ((Takewhile (%a.a:int B)`schB)
+ ((Takewhile (%a. a:int B)`schB)
@@ (y>>(h`xs
`schA
- `(TL`(Dropwhile (%a.a:int B)`schB))
+ `(TL`(Dropwhile (%a. a:int B)`schB))
)))
else
UU
@@ -56,8 +56,8 @@
let trA = fst TracesA; sigA = snd TracesA;
trB = fst TracesB; sigB = snd TracesB
in
- ( {tr. Filter (%a.a:actions sigA)`tr : trA}
- Int {tr. Filter (%a.a:actions sigB)`tr : trB}
+ ( {tr. Filter (%a. a:actions sigA)`tr : trA}
+ Int {tr. Filter (%a. a:actions sigB)`tr : trB}
Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
asig_comp sigA sigB)"
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Oct 10 19:02:28 1997 +0200
@@ -10,8 +10,8 @@
input actions may always be added to a schedule
**********************************************************************************)
-goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
-\ ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A";
+goal thy "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
+\ ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
by (safe_tac set_cs);
by (forward_tac [inp_is_act] 1);
@@ -52,7 +52,7 @@
**********************************************************************************)
goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
-\ Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
+\ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Oct 10 19:02:28 1997 +0200
@@ -543,7 +543,7 @@
section "Last";
-goal thy "!! s.Finite s ==> s~=nil --> Last`s~=UU";
+goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
by (Seq_Finite_induct_tac 1);
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
qed"Finite_Last1";
@@ -790,11 +790,11 @@
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
qed"Takewhile_idempotent";
-goal thy "Forall P s --> Takewhile (%x.Q x | (~P x))`s = Takewhile Q`s";
+goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallPTakewhileQnP";
-goal thy "Forall P s --> Dropwhile (%x.Q x | (~P x))`s = Dropwhile Q`s";
+goal thy "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallPDropwhileQnP";
@@ -807,7 +807,7 @@
bind_thm("TakewhileConc",TakewhileConc1 RS mp);
-goal thy "!! s.Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+goal thy "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
by (Seq_Finite_induct_tac 1);
qed"DropwhileConc1";
@@ -905,7 +905,7 @@
qed"take_reduction1";
-goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 = seq_take k`y2|] \
+goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) = seq_take n`(y @@ (t>>y2))";
by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
@@ -927,7 +927,7 @@
qed"take_reduction_less1";
-goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 << seq_take k`y2|] \
+goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) << seq_take n`(y @@ (t>>y2))";
by (auto_tac (!claset addSIs [take_reduction_less1 RS spec RS mp],!simpset));
qed"take_reduction_less";
@@ -1168,17 +1168,17 @@
goal thy "!! s. Finite s ==> \
\ Forall (%x. (~P x) | (~ Q x)) s \
-\ --> Filter (%x.P x & Q x)`s = nil";
+\ --> Filter (%x. P x & Q x)`s = nil";
by (Seq_Finite_induct_tac 1);
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
qed"Filter_lemma3";
goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~(P x & Q x)"),("x1","s")]
(take_lemma_induct RS mp) 1);
-(* FIX: better support for A = %.True *)
+(* FIX: better support for A = %x. True *)
by (Fast_tac 3);
by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3]
@@ -1195,7 +1195,7 @@
goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
-by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
+by (res_inst_tac [("A1","%x. True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
by (Auto_tac());
qed"MapConc_takelemma";
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Fri Oct 10 19:02:28 1997 +0200
@@ -67,7 +67,7 @@
goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
\ nil => TT \
\ | x##xs => (flift1 \
-\ (%p.Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
+\ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
\ `x) \
\ ))";
by (rtac trans 1);
@@ -163,7 +163,7 @@
goal thy
"!! A. is_trans_of A ==> \
-\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
@@ -174,7 +174,7 @@
goal thy
"!! A.[| is_trans_of A; x:executions A |] ==> \
-\ Forall (%a.a:act A) (filter_act`(snd x))";
+\ Forall (%a. a:act A) (filter_act`(snd x))";
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
by (pair_tac "x" 1);
@@ -184,7 +184,7 @@
goalw thy [schedules_def,has_schedule_def]
"!! A.[| is_trans_of A; x:schedules A |] ==> \
-\ Forall (%a.a:act A) x";
+\ Forall (%a. a:act A) x";
by (fast_tac (!claset addSIs [exec_in_sig]) 1);
qed"scheds_in_sig";
@@ -208,7 +208,7 @@
(* second prefix notion for Finite x *)
-goal thy "! y s.is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
+goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
by (pair_induct_tac "x" [is_exec_frag_def] 1);
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Fri Oct 10 19:02:28 1997 +0200
@@ -67,7 +67,7 @@
"is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of
nil => TT
| x##xs => (flift1
- (%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p))
+ (%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p))
`x)
)))"
@@ -96,7 +96,7 @@
has_trace_def
"has_trace ioa tr ==
- (? sch:schedules ioa. tr = Filter (%a.a:ext(ioa))`sch)"
+ (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
traces_def
"traces ioa == {tr. has_trace ioa tr}"
@@ -104,7 +104,7 @@
mk_trace_def
"mk_trace ioa == LAM tr.
- Filter (%a.a:ext(ioa))`(filter_act`tr)"
+ Filter (%a. a:ext(ioa))`(filter_act`tr)"
(* ------------------- Implementation ------------------------------ *)
--- a/src/HOLCF/Lift.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift.ML Fri Oct 10 19:02:28 1997 +0200
@@ -22,7 +22,7 @@
(* flift1 is continuous in a variable that occurs only
in the Def branch *)
-goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
\ cont (%y. lift_case UU (f y))";
by (rtac cont2cont_CF1L_rev 1);
by (strip_tac 1);
@@ -34,7 +34,7 @@
(* flift1 is continuous in a variable that occurs either
in the Def branch or in the argument *)
-goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
\ cont (%y. lift_case UU (f y) (g y))";
by (rtac cont2cont_app 1);
back();
--- a/src/HOLCF/Lift2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Lift2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
+qed_goal "inst_lift_po" thy "(op <<)=(%x y. x=y|x=Undef)"
(fn prems =>
[
(fold_goals_tac [less_lift_def]),
@@ -26,7 +26,7 @@
bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
-qed_goal "least_lift" thy "? x::'a lift.!y.x<<y"
+qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Undef")] exI 1),
@@ -57,7 +57,7 @@
goal Lift2.thy
"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
-\ ==> ? j.!i.j<i-->~Y(i)=Undef";
+\ ==> ? j.!i. j<i-->~Y(i)=Undef";
by Safe_tac;
by (Step_tac 1);
by (strip_tac 1);
@@ -74,7 +74,7 @@
"(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
by (rewtac max_in_chain_def);
by (strip_tac 1);
-by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm 1);
+by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm 1);
by (res_inst_tac [("x","0")] exI 1);
by (strip_tac 1);
by (rtac trans 1);
@@ -82,7 +82,7 @@
by (rtac sym 1);
by (etac spec 1);
-by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
by (rtac (chain_mono2_po RS exE) 1);
by (Fast_tac 1);
@@ -110,7 +110,7 @@
(* Main Lemma: cpo_lift *)
goal Lift2.thy
- "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
+ "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
by (Step_tac 1);
by Safe_tac;
--- a/src/HOLCF/Lift3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -80,7 +80,7 @@
section"UU and Def";
(* ---------------------------------------------------------- *)
-goal thy "x=UU | (? y.x=Def y)";
+goal thy "x=UU | (? y. x=Def y)";
by (lift.induct_tac "x" 1);
by (Asm_simp_tac 1);
by (rtac disjI2 1);
@@ -100,7 +100,7 @@
by (ALLGOALS Asm_simp_tac);
qed "expand_lift_case";
-goal thy "(x~=UU)=(? y.x=Def y)";
+goal thy "(x~=UU)=(? y. x=Def y)";
by (rtac iffI 1);
by (rtac Lift_cases 1);
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
--- a/src/HOLCF/Pcpo.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Pcpo.ML Fri Oct 10 19:02:28 1997 +0200
@@ -13,7 +13,7 @@
(* derive the old rule minimal *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "UU_least" thy [ UU_def ] "!z.UU << z"
+qed_goalw "UU_least" thy [ UU_def ] "!z. UU << z"
(fn prems => [
(rtac (select_eq_Ex RS iffD2) 1),
(rtac least 1)]);
@@ -83,7 +83,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_equal" thy
-"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k.C1(k)=C2(k)|]\
+"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k. C1(k)=C2(k)|]\
\ ==> lub(range(C1))=lub(range(C2))"
(fn prems =>
[
@@ -206,7 +206,7 @@
]);
qed_goal "chain_UU_I" thy
- "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
+ "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -219,7 +219,7 @@
qed_goal "chain_UU_I_inverse" thy
- "!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
+ "!i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -257,7 +257,7 @@
qed_goal "chain_mono2" thy
"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
-\ ==> ? j.!i.j<i-->~Y(i)=UU"
+\ ==> ? j.!i. j<i-->~Y(i)=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -279,11 +279,11 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
- "!Y::nat=>'a::flat.is_chain Y-->(? n.max_in_chain n Y)"
+ "!Y::nat=>'a::flat. is_chain Y-->(? n. max_in_chain n Y)"
(fn _ =>
[
(strip_tac 1),
- (case_tac "!i.Y(i)=UU" 1),
+ (case_tac "!i. Y(i)=UU" 1),
(res_inst_tac [("x","0")] exI 1),
(Asm_simp_tac 1),
(Asm_full_simp_tac 1),
--- a/src/HOLCF/Pcpo.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Pcpo.thy Fri Oct 10 19:02:28 1997 +0200
@@ -17,7 +17,7 @@
(* ****************************** *)
axclass pcpo < cpo
- least "? x.!y.x<<y"
+ least "? x.!y. x<<y"
consts
UU :: "'a::pcpo"
@@ -26,16 +26,16 @@
UU :: "'a::pcpo" ("\\<bottom>")
defs
- UU_def "UU == @x.!y.x<<y"
+ UU_def "UU == @x.!y. x<<y"
(* further useful classes for HOLCF domains *)
axclass chfin<cpo
-chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+chfin "!Y. is_chain Y-->(? n. max_in_chain n Y)"
axclass flat<pcpo
-ax_flat "! x y.x << y --> (x = UU) | (x=y)"
+ax_flat "! x y. x << y --> (x = UU) | (x=y)"
end
--- a/src/HOLCF/Porder.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder.ML Fri Oct 10 19:02:28 1997 +0200
@@ -256,7 +256,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_chain_maxelem" thy
-"[|? i.Y i=c;!i.Y i<<c|] ==> lub(range Y) = c"
+"[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -274,7 +274,7 @@
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_const" thy "range(%x.c) <<| c"
+qed_goal "lub_const" thy "range(%x. c) <<| c"
(fn prems =>
[
(rtac is_lubI 1),
--- a/src/HOLCF/Porder.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder.thy Fri Oct 10 19:02:28 1997 +0200
@@ -24,7 +24,7 @@
translations
- "LUB x. t" == "lub(range(%x.t))"
+ "LUB x. t" == "lub(range(%x. t))"
syntax (symbols)
@@ -33,14 +33,14 @@
defs
(* class definitions *)
-is_ub "S <| x == ! y.y:S --> y<<x"
+is_ub "S <| x == ! y. y:S --> y<<x"
is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
(* Arbitrary chains are total orders *)
is_tord "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
(* Here we use countable chains and I prefer to code them as functions! *)
-is_chain "is_chain F == (! i.F(i) << F(Suc(i)))"
+is_chain "is_chain F == (! i. F(i) << F(Suc(i)))"
(* finite chains, needed for monotony of continouous functions *)
max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)"
--- a/src/HOLCF/Porder0.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder0.ML Fri Oct 10 19:02:28 1997 +0200
@@ -12,7 +12,7 @@
(* ------------------------------------------------------------------------ *)
(* minimal fixes least element *)
(* ------------------------------------------------------------------------ *)
-bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po. uu<<x==>uu=(@u.!y. u<<y)"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Sprod2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Sprod2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
+qed_goal "inst_sprod_po" thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
(fn prems =>
[
(fold_goals_tac [less_sprod_def]),
@@ -28,7 +28,7 @@
bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
-qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y"
+qed_goal "least_sprod" thy "? x::'a**'b.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Ispair UU UU")] exI 1),
@@ -96,7 +96,7 @@
qed_goal "lub_sprod" Sprod2.thy
"[|is_chain(S)|] ==> range(S) <<| \
-\ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
+\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -123,7 +123,7 @@
qed_goal "cpo_sprod" Sprod2.thy
- "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
+ "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Sprod3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -134,7 +134,7 @@
(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
(rtac sym 1),
(rtac lub_chain_maxelem 1),
- (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1),
+ (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1),
(rtac (not_all RS iffD1) 1),
(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
(atac 1),
@@ -315,7 +315,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "beta_cfun_sprod" thy [spair_def]
- "(LAM x y.Ispair x y)`a`b = Ispair a b"
+ "(LAM x y. Ispair x y)`a`b = Ispair a b"
(fn prems =>
[
(stac beta_cfun 1),
@@ -564,7 +564,7 @@
qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
"[|is_chain(S)|] ==> range(S) <<| \
-\ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)"
+\ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Sprod3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -24,10 +24,10 @@
"(|x, y|)" == "spair`x`y"
defs
-spair_def "spair == (LAM x y.Ispair x y)"
-sfst_def "sfst == (LAM p.Isfst p)"
-ssnd_def "ssnd == (LAM p.Issnd p)"
-ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
+spair_def "spair == (LAM x y. Ispair x y)"
+sfst_def "sfst == (LAM p. Isfst p)"
+ssnd_def "ssnd == (LAM p. Issnd p)"
+ssplit_def "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
end
--- a/src/HOLCF/Ssum0.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum0.thy Fri Oct 10 19:02:28 1997 +0200
@@ -15,7 +15,7 @@
"Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
typedef (Ssum) ('a, 'b) "++" (infixr 10) =
- "{f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
+ "{f.(? a. f=Sinl_Rep(a))|(? b. f=Sinr_Rep(b))}"
syntax (symbols)
"++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
--- a/src/HOLCF/Ssum1.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum1.thy Fri Oct 10 19:02:28 1997 +0200
@@ -12,10 +12,10 @@
defs
less_ssum_def "(op <<) == (%s1 s2.@z.
- (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
- &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
- &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))
- &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+ (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
+ &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
+ &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
+ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
end
--- a/src/HOLCF/Ssum2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -10,10 +10,10 @@
(* for compatibility with old HOLCF-Version *)
qed_goal "inst_ssum_po" thy "(op <<)=(%s1 s2.@z.\
-\ (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)\
-\ &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)\
-\ &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))\
-\ &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+\ (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)\
+\ &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)\
+\ &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))\
+\ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
(fn prems =>
[
(fold_goals_tac [less_ssum_def]),
@@ -67,7 +67,7 @@
bind_thm ("UU_ssum_def",minimal_ssum RS minimal2UU RS sym);
-qed_goal "least_ssum" thy "? x::'a++'b.!y.x<<y"
+qed_goal "least_ssum" thy "? x::'a++'b.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Isinl UU")] exI 1),
@@ -174,7 +174,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma1" thy
-"[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.Y(i)~=Isinl(x))"
+"[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -199,7 +199,7 @@
qed_goal "ssum_lemma3" thy
"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
-\ (!i.? y.Y(i)=Isinr(y))"
+\ (!i.? y. Y(i)=Isinr(y))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -231,7 +231,7 @@
]);
qed_goal "ssum_lemma4" thy
-"is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
+"is_chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -249,7 +249,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma5" thy
-"z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
+"z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -264,7 +264,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma6" thy
-"z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
+"z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -279,7 +279,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma7" thy
-"[|Isinl(x) << z; x~=UU|] ==> ? y.z=Isinl(y) & y~=UU"
+"[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -297,7 +297,7 @@
]);
qed_goal "ssum_lemma8" thy
-"[|Isinr(x) << z; x~=UU|] ==> ? y.z=Isinr(y) & y~=UU"
+"[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -317,9 +317,9 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_ssum1a" thy
-"[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
+"[|is_chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
\ range(Y) <<|\
-\ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y i))))"
+\ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -358,9 +358,9 @@
qed_goal "lub_ssum1b" thy
-"[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
+"[|is_chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
\ range(Y) <<|\
-\ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y i))))"
+\ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -413,7 +413,7 @@
*)
qed_goal "cpo_ssum" thy
- "is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
+ "is_chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Ssum3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -156,7 +156,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma9" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -174,7 +174,7 @@
qed_goal "ssum_lemma10" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -615,7 +615,7 @@
qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def]
"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\
-\ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -641,7 +641,7 @@
]);
qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def]
- "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x.Y(i)=sinl`x"
+ "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -655,7 +655,7 @@
]);
qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def]
- "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x.Y(i)=sinr`x"
+ "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -670,8 +670,8 @@
qed_goal "thelub_ssum3" Ssum3.thy
"is_chain(Y) ==>\
-\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y.UU)`(Y i))))\
-\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
+\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Ssum3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -17,11 +17,11 @@
defs
-sinl_def "sinl == (LAM x.Isinl(x))"
-sinr_def "sinr == (LAM x.Isinr(x))"
-sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
+sinl_def "sinl == (LAM x. Isinl(x))"
+sinr_def "sinr == (LAM x. Isinr(x))"
+sswhen_def "sswhen == (LAM f g s. Iwhen(f)(g)(s))"
translations
-"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
+"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x. t1)`(LAM y. t2)`s"
end
--- a/src/HOLCF/Tr.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Tr.thy Fri Oct 10 19:02:28 1997 +0200
@@ -34,9 +34,9 @@
TT_def "TT==Def True"
FF_def "FF==Def False"
neg_def "neg == flift2 Not"
- ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
- andalso_def "trand == (LAM x y.If x then y else FF fi)"
- orelse_def "tror == (LAM x y.If x then TT else y fi)"
+ ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)"
+ andalso_def "trand == (LAM x y. If x then y else FF fi)"
+ orelse_def "tror == (LAM x y. If x then TT else y fi)"
If2_def "If2 Q x y == If Q then x else y fi"
end
--- a/src/HOLCF/Up1.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up1.thy Fri Oct 10 19:02:28 1997 +0200
@@ -23,7 +23,7 @@
defs
Iup_def "Iup x == Abs_Up(Inr(x))"
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
- less_up_def "(op <<) == (%x1 x2.case Rep_Up(x1) of
+ less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of
Inl(y1) => True
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
| Inr(z2) => y2<<z2))"
--- a/src/HOLCF/Up2.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up2.ML Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
open Up2;
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_po" thy "(op <<)=(%x1 x2.case Rep_Up(x1) of \
+qed_goal "inst_up_po" thy "(op <<)=(%x1 x2. case Rep_Up(x1) of \
\ Inl(y1) => True \
\ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
\ | Inr(z2) => y2<<z2))"
@@ -31,7 +31,7 @@
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
-qed_goal "least_up" thy "? x::'a u.!y.x<<y"
+qed_goal "least_up" thy "? x::'a u.!y. x<<y"
(fn prems =>
[
(res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
@@ -99,7 +99,7 @@
(* Some kind of surjectivity lemma *)
(* ------------------------------------------------------------------------ *)
-qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -111,8 +111,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_up1a" thy
-"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
-\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
+"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
+\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -183,7 +183,7 @@
*)
qed_goal "cpo_up" thy
- "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
+ "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Up3.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up3.ML Fri Oct 10 19:02:28 1997 +0200
@@ -274,7 +274,7 @@
]);
-qed_goal "up_lemma2" thy " (? x.z = up`x) = (z~=UU)"
+qed_goal "up_lemma2" thy " (? x. z = up`x) = (z~=UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -317,7 +317,7 @@
qed_goal "thelub_up3" thy
"is_chain(Y) ==> lub(range(Y)) = UU |\
-\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))"
+\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Up3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -14,12 +14,12 @@
constdefs
up :: "'a -> ('a)u"
- "up == (LAM x.Iup(x))"
+ "up == (LAM x. Iup(x))"
fup :: "('a->'c)-> ('a)u -> 'c"
- "fup == (LAM f p.Ifup(f)(p))"
+ "fup == (LAM f p. Ifup(f)(p))"
translations
-"case l of up`x => t1" == "fup`(LAM x.t1)`l"
+"case l of up`x => t1" == "fup`(LAM x. t1)`l"
end
--- a/src/HOLCF/ex/Dlist.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Dlist.ML Fri Oct 10 19:02:28 1997 +0200
@@ -5,7 +5,7 @@
(* ------------------------------------------------------------------------- *)
bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def
- "lmap = (LAM f s.case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
+ "lmap = (LAM f s. case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
(* ------------------------------------------------------------------------- *)
(* recursive properties of lmap *)
--- a/src/HOLCF/ex/Dnat.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Dnat.ML Fri Oct 10 19:02:28 1997 +0200
@@ -47,7 +47,7 @@
val iterator_rews =
[iterator1, iterator2, iterator3];
-val dnat_flat = prove_goal Dnat.thy "!x y::dnat.x<<y --> x=UU | x=y"
+val dnat_flat = prove_goal Dnat.thy "!x y::dnat. x<<y --> x=UU | x=y"
(fn _ => [
(rtac allI 1),
(res_inst_tac [("x","x")] dnat.ind 1),
--- a/src/HOLCF/ex/Focus_ex.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.ML Fri Oct 10 19:02:28 1997 +0200
@@ -63,7 +63,7 @@
by (REPEAT (etac conjE 1));
by (etac conjI 1);
by (strip_tac 1);
-by (res_inst_tac [("x","fix`(LAM k.csnd`(f`<x,k>))")] exI 1);
+by (res_inst_tac [("x","fix`(LAM k. csnd`(f`<x,k>))")] exI 1);
by (rtac conjI 1);
by (asm_simp_tac HOLCF_ss 1);
by (rtac trans 1);
--- a/src/HOLCF/ex/Focus_ex.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy Fri Oct 10 19:02:28 1997 +0200
@@ -131,6 +131,6 @@
def_g "def_g g == (? f.
is_f f &
- g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)))"
+ g = (LAM x. cfst`(f`<x,fix`(LAM k. csnd`(f`<x,k>))>)))"
end
--- a/src/HOLCF/ex/Hoare.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Hoare.ML Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
]);
val hoare_lemma3 = prove_goal HOLCF.thy
-" (!k.b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
+" (!k. b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
(fn prems =>
[
(fast_tac HOL_cs 1)
@@ -177,8 +177,8 @@
*)
val hoare_lemma11 = prove_goal Hoare.thy
-"(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+"(? n. b1`(iterate n g x) ~= TT) ==>\
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
\ --> p`x = iterate k g x"
(fn prems =>
[
--- a/src/HOLCF/ex/Loop.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Loop.ML Fri Oct 10 19:02:28 1997 +0200
@@ -40,7 +40,7 @@
]);
val while_unfold2 = prove_goal Loop.thy
- "!x.while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
+ "!x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
(fn prems =>
[
(nat_ind_tac "k" 1),
@@ -83,7 +83,7 @@
(* --------------------------------------------------------------------------- *)
val loop_lemma1 = prove_goal Loop.thy
-"[|? y.b`y=FF; iterate k (step`b`g) x = UU|]==>iterate(Suc k) (step`b`g) x=UU"
+"[|? y. b`y=FF; iterate k (step`b`g) x = UU|]==>iterate(Suc k) (step`b`g) x=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -98,7 +98,7 @@
]);
val loop_lemma2 = prove_goal Loop.thy
-"[|? y.b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
+"[|? y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
\iterate k (step`b`g) x ~=UU"
(fn prems =>
[
@@ -111,7 +111,7 @@
val loop_lemma3 = prove_goal Loop.thy
"[|!x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
-\? y.b`y=FF; INV x|] ==>\
+\? y. b`y=FF; INV x|] ==>\
\iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)"
(fn prems =>
[
@@ -266,7 +266,7 @@
val loop_inv = prove_goal Loop.thy
"[| P(x);\
-\ !!y.P y ==> INV y;\
+\ !!y. P y ==> INV y;\
\ !!y.[| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
\ !!y.[| INV y; b`y=FF|]==> Q y;\
\ while`b`g`x ~= UU |] ==> Q (while`b`g`x)"
--- a/src/HOLCF/ex/Stream.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Stream.ML Fri Oct 10 19:02:28 1997 +0200
@@ -140,7 +140,7 @@
(rtac refl 1)
]);
-qed_goal "chain_stream_take" thy "is_chain (%i.stream_take i`s)" (fn _ => [
+qed_goal "chain_stream_take" thy "is_chain (%i. stream_take i`s)" (fn _ => [
rtac is_chainI 1,
subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
fast_tac HOL_cs 1,
@@ -189,7 +189,7 @@
*)
val stream_take_lemma3 = prove_goal thy
- "!x xs.x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
+ "!x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
(fn prems => [
(nat_ind_tac "n" 1),
(asm_simp_tac (HOL_ss addsimps stream.take_rews) 1),
--- a/src/HOLCF/ex/loeckx.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/loeckx.ML Fri Oct 10 19:02:28 1997 +0200
@@ -3,7 +3,7 @@
(* Loeckx & Sieber S.88 *)
val prems = goalw Fix.thy [Ifix_def]
-"Ifix F= lub (range (%i.%G.iterate i G UU)) F";
+"Ifix F= lub (range (%i.%G. iterate i G UU)) F";
by (stac thelub_fun 1);
by (rtac ch2ch_fun 1);
back();
@@ -48,15 +48,15 @@
val prems = goal Fix.thy "cont(Ifix)";
by (res_inst_tac
- [("t","Ifix"),("s","(%f.lub(range(%j.(LAM f. iterate j f UU)`f)))")]
+ [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
ssubst 1);
by (rtac ext 1);
by (rewtac Ifix_def );
by (subgoal_tac
- "range(% i.iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
+ "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
by (etac arg_cong 1);
by (subgoal_tac
- "(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
+ "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
by (etac arg_cong 1);
by (rtac ext 1);
by (stac beta_cfun 1);
@@ -79,7 +79,7 @@
(* the proof in little steps *)
val prems = goal Fix.thy
-"(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
+"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
by (rtac ext 1);
by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
@@ -88,7 +88,7 @@
val fix_lemma1 = result();
val prems = goal Fix.thy
-" Ifix = (%f.lub(range(%j.(LAM f.iterate j f UU)`f)))";
+" Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
by (rtac ext 1);
by (rewtac Ifix_def );
by (stac fix_lemma1 1);