--- a/src/CCL/CCL.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/CCL.ML Fri Oct 10 17:10:12 1997 +0200
@@ -22,7 +22,7 @@
qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
-goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
+goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
by (fast_tac (set_cs addIs [po_abstractn]) 1);
bind_thm("abstractn", standard (allI RS (result() RS mp)));
@@ -68,7 +68,7 @@
val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
["<a,b> = <a',b'> <-> (a=a' & b=b')",
- "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
+ "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
@@ -140,13 +140,13 @@
by (resolve_tac (prems RL [major RS ssubst]) 1);
qed "XHlemma1";
-goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> & P(t,t')} <-> Q)";
+goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <-> Q)";
by (fast_tac ccl_cs 1);
bind_thm("XHlemma2", result() RS mp);
(*** Pre-Order ***)
-goalw CCL.thy [POgen_def,SIM_def] "mono(%X.POgen(X))";
+goalw CCL.thy [POgen_def,SIM_def] "mono(%X. POgen(X))";
by (rtac monoI 1);
by (safe_tac ccl_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -156,15 +156,15 @@
goalw CCL.thy [POgen_def,SIM_def]
"<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
+\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
+\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
by (rtac (iff_refl RS XHlemma2) 1);
qed "POgenXH";
goal CCL.thy
"t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
+\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
+\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
br (rewrite_rule [POgen_def,SIM_def]
(POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
@@ -189,7 +189,7 @@
by (fast_tac ccl_cs 1);
qed "po_pair";
-goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
+goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
by (rtac (poXH RS iff_trans) 1);
by (simp_tac ccl_ss 1);
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
@@ -200,13 +200,13 @@
val ccl_porews = [po_bot,po_pair,po_lam];
val [p1,p2,p3,p4,p5] = goal CCL.thy
- "[| t [= t'; a [= a'; b [= b'; !!x y.c(x,y) [= c'(x,y); \
-\ !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
+ "[| t [= t'; a [= a'; b [= b'; !!x y. c(x,y) [= c'(x,y); \
+\ !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
by (rtac (p1 RS po_cong RS po_trans) 1);
by (rtac (p2 RS po_cong RS po_trans) 1);
by (rtac (p3 RS po_cong RS po_trans) 1);
by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
-by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")]
+by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")]
(p5 RS po_abstractn RS po_cong RS po_trans) 1);
by (rtac po_refl 1);
qed "case_pocong";
@@ -217,7 +217,7 @@
qed "apply_pocong";
-val prems = goal CCL.thy "~ lam x.b(x) [= bot";
+val prems = goal CCL.thy "~ lam x. b(x) [= bot";
by (rtac notI 1);
by (dtac bot_poleast 1);
by (etac (distinctness RS notE) 1);
@@ -230,14 +230,14 @@
by (resolve_tac prems 1);
qed "po_lemma";
-goal CCL.thy "~ <a,b> [= lam x.f(x)";
+goal CCL.thy "~ <a,b> [= lam x. f(x)";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
qed "npo_pair_lam";
-goal CCL.thy "~ lam x.f(x) [= <a,b>";
+goal CCL.thy "~ lam x. f(x) [= <a,b>";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
@@ -252,9 +252,9 @@
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
["~ true [= false", "~ false [= true",
"~ true [= <a,b>", "~ <a,b> [= true",
- "~ true [= lam x.f(x)","~ lam x.f(x) [= true",
+ "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
"~ false [= <a,b>", "~ <a,b> [= false",
- "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
+ "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
(* Coinduction for [= *)
@@ -267,7 +267,7 @@
(*************** EQUALITY *******************)
-goalw CCL.thy [EQgen_def,SIM_def] "mono(%X.EQgen(X))";
+goalw CCL.thy [EQgen_def,SIM_def] "mono(%X. EQgen(X))";
by (rtac monoI 1);
by (safe_tac set_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -278,19 +278,19 @@
goalw CCL.thy [EQgen_def,SIM_def]
"<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | \
\ (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
+\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
+\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
by (rtac (iff_refl RS XHlemma2) 1);
qed "EQgenXH";
goal CCL.thy
"t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a=a' & b=b') | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
+\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a=a' & b=b') | \
+\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
by (subgoal_tac
"<t,t'> : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \
-\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | \
-\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
+\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | \
+\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
by (etac rev_mp 1);
by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
br (rewrite_rule [EQgen_def,SIM_def]
@@ -304,7 +304,7 @@
qed "eq_coinduct";
val prems = goal CCL.thy
- "[| <t,u> : R; R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
+ "[| <t,u> : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
by (REPEAT (ares_tac (EQgen_mono::prems) 1));
qed "eq_coinduct3";
@@ -314,18 +314,18 @@
(*** Untyped Case Analysis and Other Facts ***)
-goalw CCL.thy [apply_def] "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
+goalw CCL.thy [apply_def] "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
by (safe_tac ccl_cs);
by (simp_tac ccl_ss 1);
bind_thm("cond_eta", result() RS mp);
-goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
+goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
by (fast_tac set_cs 1);
qed "exhaustion";
val prems = goal CCL.thy
- "[| P(bot); P(true); P(false); !!x y.P(<x,y>); !!b.P(lam x.b(x)) |] ==> P(t)";
+ "[| P(bot); P(true); P(false); !!x y. P(<x,y>); !!b. P(lam x. b(x)) |] ==> P(t)";
by (cut_facts_tac [exhaustion] 1);
by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
qed "term_case";
--- a/src/CCL/CCL.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/CCL.thy Fri Oct 10 17:10:12 1997 +0200
@@ -56,18 +56,18 @@
trueV "true ---> true"
falseV "false ---> false"
pairV "<a,b> ---> <a,b>"
- lamV "lam x.b(x) ---> lam x.b(x)"
+ lamV "lam x. b(x) ---> lam x. b(x)"
caseVtrue "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c"
caseVfalse "[| t ---> false; e ---> c |] ==> case(t,d,e,f,g) ---> c"
caseVpair "[| t ---> <a,b>; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
- caseVlam "[| t ---> lam x.b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
+ caseVlam "[| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
(*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
canonical "[| t ---> c; c==true ==> u--->v;
c==false ==> u--->v;
- !!a b.c==<a,b> ==> u--->v;
- !!f.c==lam x.f(x) ==> u--->v |] ==>
+ !!a b. c==<a,b> ==> u--->v;
+ !!f. c==lam x. f(x) ==> u--->v |] ==>
u--->v"
(* Should be derivable - but probably a bitch! *)
@@ -77,9 +77,9 @@
(*** Definitions used in the following rules ***)
- apply_def "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))"
- bot_def "bot == (lam x.x`x)`(lam x.x`x)"
- fix_def "fix(f) == (lam x.f(x`x))`(lam x.f(x`x))"
+ apply_def "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
+ bot_def "bot == (lam x. x`x)`(lam x. x`x)"
+ fix_def "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
(* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
(* as a bisimulation. They can both be expressed as (bi)simulations up to *)
@@ -87,8 +87,8 @@
SIM_def
"SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) |
- (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
- (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
+ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
+ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
POgen_def "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
EQgen_def "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
@@ -105,7 +105,7 @@
po_cong "a [= b ==> f(a) [= f(b)"
(* Extend definition of [= to program fragments of higher type *)
- po_abstractn "(!!x. f(x) [= g(x)) ==> (%x.f(x)) [= (%x.g(x))"
+ po_abstractn "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))"
(** Equality - equivalence axioms inherited from FOL.thy **)
(** - congruence of "=" is axiomatised implicitly **)
@@ -122,11 +122,11 @@
caseBtrue "case(true,d,e,f,g) = d"
caseBfalse "case(false,d,e,f,g) = e"
caseBpair "case(<a,b>,d,e,f,g) = f(a,b)"
- caseBlam "case(lam x.b(x),d,e,f,g) = g(b)"
+ caseBlam "case(lam x. b(x),d,e,f,g) = g(b)"
caseBbot "case(bot,d,e,f,g) = bot" (* strictness *)
(** The theory is non-trivial **)
- distinctness "~ lam x.b(x) = bot"
+ distinctness "~ lam x. b(x) = bot"
(*** Definitions of Termination and Divergence ***)
--- a/src/CCL/Fix.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Fix.ML Fri Oct 10 17:10:12 1997 +0200
@@ -11,7 +11,7 @@
(*** Fixed Point Induction ***)
val [base,step,incl] = goalw Fix.thy [INCL_def]
- "[| P(bot); !!x.P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))";
+ "[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))";
by (rtac (incl RS spec RS mp) 1);
by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
by (ALLGOALS (simp_tac term_ss));
@@ -26,18 +26,18 @@
qed "inclXH";
val prems = goal Fix.thy
- "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
+ "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))";
by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
qed "inclI";
val incl::prems = goal Fix.thy
- "[| INCL(P); !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
+ "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)]
@ prems)) 1);
qed "inclD";
val incl::prems = goal Fix.thy
- "[| INCL(P); (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
+ "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
qed "inclE";
@@ -55,19 +55,19 @@
by (rtac po_cong 1 THEN rtac po_bot 1);
qed "npo_INCL";
-val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
+val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
qed "conj_INCL";
-val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
+val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
qed "all_INCL";
-val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
+val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
qed "ball_INCL";
-goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
+goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))";
by (simp_tac (term_ss addsimps [eq_iff]) 1);
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
qed "eq_INCL";
@@ -80,7 +80,7 @@
by (rtac (fixB RS sym) 1);
qed "fix_idgenfp";
-goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
+goalw Fix.thy [idgen_def] "idgen(lam x. x) = lam x. x";
by (simp_tac term_ss 1);
by (rtac (term_case RS allI) 1);
by (ALLGOALS (simp_tac term_ss));
@@ -109,14 +109,14 @@
"idgen(d) = d ==> d ` true = true",
"idgen(d) = d ==> d ` false = false",
"idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>",
- "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"]
+ "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"]
end;
(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points
of idgen and hence are they same *)
val [p1,p2,p3] = goal CCL.thy
- "[| ALL x.t ` x [= u ` x; EX f.t=lam x.f(x); EX f.u=lam x.f(x) |] ==> t [= u";
+ "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u";
by (stac (p2 RS cond_eta) 1);
by (stac (p3 RS cond_eta) 1);
by (rtac (p1 RS (po_lam RS iffD2)) 1);
@@ -129,8 +129,8 @@
val [prem] = goal Fix.thy
"idgen(d) = d ==> \
-\ {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <= \
-\ POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)})";
+\ {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <= \
+\ POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "t" 1);
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
@@ -146,7 +146,7 @@
val [prem] = goal Fix.thy
"idgen(d) = d ==> \
-\ {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
+\ {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "a" 1);
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
@@ -154,14 +154,14 @@
qed "lemma2";
val [prem] = goal Fix.thy
- "idgen(d) = d ==> lam x.x [= d";
+ "idgen(d) = d ==> lam x. x [= d";
by (rtac (allI RS po_eta) 1);
by (rtac (lemma2 RSN(2,po_coinduct)) 1);
by (simp_tac term_ss 1);
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
qed "id_least_idgen";
-goal Fix.thy "fix(idgen) = lam x.x";
+goal Fix.thy "fix(idgen) = lam x. x";
by (fast_tac (term_cs addIs [eq_iff RS iffD2,
id_idgenfp RS fix_least_idgen,
fix_idgenfp RS id_least_idgen]) 1);
@@ -169,7 +169,7 @@
(********)
-val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
+val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t";
by (rtac (prem RS sym RS subst) 1);
by (rtac applyB 1);
qed "id_apply";
@@ -177,7 +177,7 @@
val prems = goal Fix.thy
"[| P(bot); P(true); P(false); \
\ !!x y.[| P(x); P(y) |] ==> P(<x,y>); \
-\ !!u.(!!x.P(u(x))) ==> P(lam x.u(x)); INCL(P) |] ==> \
+\ !!u.(!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> \
\ P(t)";
by (rtac (reachability RS id_apply RS subst) 1);
by (res_inst_tac [("x","t")] spec 1);
--- a/src/CCL/Fix.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Fix.thy Fri Oct 10 17:10:12 1997 +0200
@@ -17,10 +17,10 @@
rules
idgen_def
- "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))"
+ "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
- INCL_def "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))"
- po_INCL "INCL(%x.a(x) [= b(x))"
- INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))"
+ INCL_def "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
+ po_INCL "INCL(%x. a(x) [= b(x))"
+ INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
end
--- a/src/CCL/Gfp.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Gfp.ML Fri Oct 10 17:10:12 1997 +0200
@@ -71,13 +71,13 @@
- instead of the condition A <= f(A)
consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***)
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
+val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un A 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
- "[| A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> \
-\ lfp(%x.f(x) Un A Un gfp(f)) <= f(lfp(%x.f(x) Un A Un gfp(f)))";
+ "[| A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> \
+\ lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A 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);
@@ -90,7 +90,7 @@
qed "coinduct3_lemma";
val ainA::prems = goal Gfp.thy
- "[| a:A; A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
+ "[| a:A; A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
by (rtac coinduct 1);
by (rtac (prems MRS coinduct3_lemma) 2);
by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
@@ -118,7 +118,7 @@
qed "def_coinduct2";
val rew::prems = goal Gfp.thy
- "[| h==gfp(f); a:A; A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
+ "[| h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
qed "def_coinduct3";
--- a/src/CCL/Hered.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Hered.ML Fri Oct 10 17:10:12 1997 +0200
@@ -12,20 +12,20 @@
(*** Hereditary Termination ***)
-goalw Hered.thy [HTTgen_def] "mono(%X.HTTgen(X))";
+goalw Hered.thy [HTTgen_def] "mono(%X. HTTgen(X))";
by (rtac monoI 1);
by (fast_tac set_cs 1);
qed "HTTgen_mono";
goalw Hered.thy [HTTgen_def]
- "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
-\ (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
+ "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
+\ (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
by (fast_tac set_cs 1);
qed "HTTgenXH";
goal Hered.thy
- "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
-\ (EX f.t=lam x.f(x) & (ALL x.f(x) : HTT))";
+ "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
+\ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
br (rewrite_rule [HTTgen_def]
(HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
by (fast_tac set_cs 1);
@@ -50,7 +50,7 @@
by (fast_tac term_cs 1);
qed "HTT_pair";
-goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
+goal Hered.thy "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
by (rtac (HTTXH RS iff_trans) 1);
by (simp_tac term_ss 1);
by (safe_tac term_cs);
@@ -97,7 +97,7 @@
["true : HTTgen(R)",
"false : HTTgen(R)",
"[| a : R; b : R |] ==> <a,b> : HTTgen(R)",
- "[| !!x. b(x) : R |] ==> lam x.b(x) : HTTgen(R)",
+ "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
"one : HTTgen(R)",
"a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
\ inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
@@ -127,7 +127,7 @@
qed "PlusF";
val prems = goal Hered.thy
- "[| A <= HTT; !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
+ "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
qed "SigmaF";
@@ -178,7 +178,7 @@
(*** but it seems as easy (and more general) to do this directly by coinduction ***)
(*
val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> u [= t";
-by (po_coinduct_tac "{p. EX a b.p=<a,b> & b : HTT & b [= a}" 1);
+by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1);
by (fast_tac (ccl_cs addIs prems) 1);
by (safe_tac ccl_cs);
by (dtac (poXH RS iffD1) 1);
--- a/src/CCL/Hered.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Hered.thy Fri Oct 10 17:10:12 1997 +0200
@@ -23,8 +23,8 @@
(*** Definitions of Hereditary Termination ***)
HTTgen_def
- "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) |
- (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}"
+ "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) |
+ (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"
HTT_def "HTT == gfp(HTTgen)"
end
--- a/src/CCL/Lfp.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Lfp.ML Fri Oct 10 17:10:12 1997 +0200
@@ -45,7 +45,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);
@@ -64,7 +64,7 @@
val rew::prems = goal Lfp.thy
"[| A == lfp(f); a:A; mono(f); \
-\ !!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/CCL/Set.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Set.ML Fri Oct 10 17:10:12 1997 +0200
@@ -13,12 +13,12 @@
open Set;
-val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
+val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}";
by (rtac (mem_Collect_iff RS iffD2) 1);
by (rtac prem 1);
qed "CollectI";
-val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
+val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)";
by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1);
qed "CollectD";
@@ -56,7 +56,7 @@
qed "bexI";
qed_goal "bexCI" Set.thy
- "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A.P(x)"
+ "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
@@ -93,7 +93,7 @@
(*** Rules for 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";
@@ -163,7 +163,7 @@
by (REPEAT (resolve_tac (refl::prems) 1));
qed "setup_induction";
-goal Set.thy "{x.x:A} = A";
+goal Set.thy "{x. x:A} = A";
by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1));
qed "trivial_set";
@@ -234,7 +234,7 @@
(*** Empty sets ***)
-goalw Set.thy [empty_def] "{x.False} = {}";
+goalw Set.thy [empty_def] "{x. False} = {}";
by (rtac refl 1);
qed "empty_eq";
@@ -244,7 +244,7 @@
val emptyE = make_elim emptyD;
-val [prem] = goal Set.thy "~ A={} ==> (EX x.x:A)";
+val [prem] = goal Set.thy "~ A={} ==> (EX x. x:A)";
by (rtac (prem RS swap) 1);
by (rtac equalityI 1);
by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
--- a/src/CCL/Set.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Set.thy Fri Oct 10 17:10:12 1997 +0200
@@ -50,17 +50,17 @@
rules
- mem_Collect_iff "(a : {x.P(x)}) <-> P(a)"
- set_extension "A=B <-> (ALL x.x:A <-> x:B)"
+ mem_Collect_iff "(a : {x. P(x)}) <-> P(a)"
+ set_extension "A=B <-> (ALL x. x:A <-> x:B)"
Ball_def "Ball(A, P) == ALL x. x:A --> P(x)"
Bex_def "Bex(A, P) == EX x. x:A & P(x)"
mono_def "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))"
subset_def "A <= B == ALL x:A. x:B"
- singleton_def "{a} == {x.x=a}"
- empty_def "{} == {x.False}"
- Un_def "A Un B == {x.x:A | x:B}"
- Int_def "A Int B == {x.x:A & x:B}"
+ singleton_def "{a} == {x. x=a}"
+ empty_def "{} == {x. False}"
+ Un_def "A Un B == {x. x:A | x:B}"
+ Int_def "A Int B == {x. x:A & x:B}"
Compl_def "Compl(A) == {x. ~x:A}"
INTER_def "INTER(A, B) == {y. ALL x:A. y: B(x)}"
UNION_def "UNION(A, B) == {y. EX x:A. y: B(x)}"
--- a/src/CCL/Term.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Term.ML Fri Oct 10 17:10:12 1997 +0200
@@ -35,7 +35,7 @@
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
qed "letBbbot";
-goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
+goalw Term.thy [apply_def] "(lam x. b(x)) ` a = b(a)";
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
qed "applyB";
@@ -48,7 +48,7 @@
qed "fixB";
goalw Term.thy [letrec_def]
- "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
+ "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))";
by (resolve_tac [fixB RS ssubst] 1 THEN
resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
qed "letrecB";
@@ -98,10 +98,10 @@
val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
"letrec g x y be h(x,y,g) in g(p,q) = \
-\ h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))";
+\ h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))";
val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def])
"letrec g x y z be h(x,y,z,g) in g(p,q,r) = \
-\ h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))";
+\ h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))";
val napplyBzero = mk_beta_rl "f^zero`a = a";
val napplyBsucc = mk_beta_rl "f^succ(n)`a = f(f^n`a)";
--- a/src/CCL/Term.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Term.thy Fri Oct 10 17:10:12 1997 +0200
@@ -54,36 +54,36 @@
rules
one_def "one == true"
- if_def "if b then t else u == case(b,t,u,% x y.bot,%v.bot)"
+ if_def "if b then t else u == case(b,t,u,% x y. bot,%v. bot)"
inl_def "inl(a) == <true,a>"
inr_def "inr(b) == <false,b>"
- when_def "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
- split_def "split(t,f) == case(t,bot,bot,f,%u.bot)"
- fst_def "fst(t) == split(t,%x y.x)"
- snd_def "snd(t) == split(t,%x y.y)"
- thd_def "thd(t) == split(t,%x p.split(p,%y z.z))"
+ when_def "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
+ split_def "split(t,f) == case(t,bot,bot,f,%u. bot)"
+ fst_def "fst(t) == split(t,%x y. x)"
+ snd_def "snd(t) == split(t,%x y. y)"
+ thd_def "thd(t) == split(t,%x p. split(p,%y z. z))"
zero_def "zero == inl(one)"
succ_def "succ(n) == inr(n)"
- ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
- nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
+ ncase_def "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
+ nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
nil_def "[] == inl(one)"
cons_def "h$t == inr(<h,t>)"
- lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
- lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
+ lcase_def "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
+ lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
- let_def "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"
+ let_def "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))"
letrec_def
- "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
+ "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
letrec2_def "letrec g x y be h(x,y,g) in f(g)==
- letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>)))
- in f(%x y.g'(<x,y>))"
+ letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
+ in f(%x y. g'(<x,y>))"
letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) ==
- letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>))))
- in f(%x y z.g'(<x,<y,z>>))"
+ letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>))))
+ in f(%x y z. g'(<x,<y,z>>))"
- napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
+ napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
end
--- a/src/CCL/Type.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Type.ML Fri Oct 10 17:10:12 1997 +0200
@@ -15,7 +15,7 @@
val simp_data_defs = [one_def,inl_def,inr_def];
val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
-goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
+goal Set.thy "A <= B <-> (ALL x. x:A --> x:B)";
by (fast_tac set_cs 1);
qed "subsetXH";
@@ -25,18 +25,18 @@
val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
val EmptyXH = XH_tac "a : {} <-> False";
-val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
+val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))";
val UnitXH = XH_tac "a : Unit <-> a=one";
val BoolXH = XH_tac "a : Bool <-> a=true | a=false";
-val PlusXH = XH_tac "a : A+B <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
-val PiXH = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
-val SgXH = XH_tac "a : SUM x:A.B(x) <-> (EX x:A.EX y:B(x).a=<x,y>)";
+val PlusXH = XH_tac "a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))";
+val PiXH = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))";
+val SgXH = XH_tac "a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=<x,y>)";
val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
-val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
-val TexXH = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
+val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))";
+val TexXH = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))";
val case_rls = XH_to_Es XHs;
@@ -49,7 +49,7 @@
val oneT = canT_tac "one : Unit";
val trueT = canT_tac "true : Bool";
val falseT = canT_tac "false : Bool";
-val lamT = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
+val lamT = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)";
val pairT = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
val inlT = canT_tac "a:A ==> inl(a) : A+B";
val inrT = canT_tac "b:B ==> inr(b) : A+B";
@@ -108,16 +108,16 @@
(*** Monotonicity ***)
-goal Type.thy "mono (%X.X)";
+goal Type.thy "mono (%X. X)";
by (REPEAT (ares_tac [monoI] 1));
qed "idM";
-goal Type.thy "mono(%X.A)";
+goal Type.thy "mono(%X. A)";
by (REPEAT (ares_tac [monoI,subset_refl] 1));
qed "constM";
val major::prems = goal Type.thy
- "mono(%X.A(X)) ==> mono(%X.[A(X)])";
+ "mono(%X. A(X)) ==> mono(%X.[A(X)])";
by (rtac (subsetI RS monoI) 1);
by (dtac (LiftXH RS iffD1) 1);
by (etac disjE 1);
@@ -128,8 +128,8 @@
qed "LiftM";
val prems = goal Type.thy
- "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
-\ mono(%X.Sigma(A(X),B(X)))";
+ "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \
+\ mono(%X. Sigma(A(X),B(X)))";
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -137,7 +137,7 @@
qed "SgM";
val prems = goal Type.thy
- "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
+ "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))";
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -145,7 +145,7 @@
qed "PiM";
val prems = goal Type.thy
- "[| mono(%X.A(X)); mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
+ "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))";
by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -156,18 +156,18 @@
(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
-goal Type.thy "mono(%X.Unit+X)";
+goal Type.thy "mono(%X. Unit+X)";
by (REPEAT (ares_tac [PlusM,constM,idM] 1));
qed "NatM";
bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
-goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
+goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
qed "ListM";
bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
-goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
+goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
qed "IListsM";
bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
@@ -182,10 +182,10 @@
val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
-val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
-val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
-val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
-val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
+val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))";
+val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))";
+val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))";
+val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)";
val iXHs = [NatXH,ListXH];
val icase_rls = XH_to_Es iXHs;
@@ -283,15 +283,15 @@
qed "lfp_subset_gfp";
val prems = goal Type.thy
- "[| a:A; !!x X.[| x:A; ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
+ "[| a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
\ t(a) : gfp(B)";
by (rtac coinduct 1);
-by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
+by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1);
by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
qed "gfpI";
val rew::prem::prems = goal Type.thy
- "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
+ "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
\ t(a) : C";
by (rewtac rew);
by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
--- a/src/CCL/Type.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Type.thy Fri Oct 10 17:10:12 1997 +0200
@@ -46,23 +46,23 @@
rules
- Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
- Unit_def "Unit == {x.x=one}"
- Bool_def "Bool == {x.x=true | x=false}"
- Plus_def "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
- Pi_def "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
- Sigma_def "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
- Nat_def "Nat == lfp(% X.Unit + X)"
- List_def "List(A) == lfp(% X.Unit + A*X)"
+ Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}"
+ Unit_def "Unit == {x. x=one}"
+ Bool_def "Bool == {x. x=true | x=false}"
+ Plus_def "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
+ Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
+ Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
+ Nat_def "Nat == lfp(% X. Unit + X)"
+ List_def "List(A) == lfp(% X. Unit + A*X)"
- Lists_def "Lists(A) == gfp(% X.Unit + A*X)"
+ Lists_def "Lists(A) == gfp(% X. Unit + A*X)"
ILists_def "ILists(A) == gfp(% X.{} + A*X)"
- Tall_def "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
- Tex_def "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
+ Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
+ Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
Lift_def "[A] == A Un {bot}"
- SPLIT_def "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
+ SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
end
--- a/src/CCL/Wfd.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Wfd.ML Fri Oct 10 17:10:12 1997 +0200
@@ -25,7 +25,7 @@
val [p1,p2,p3] = goal Wfd.thy
"[| !!x y.<x,y> : R ==> Q(x); \
\ ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
-\ !!x.Q(x) ==> x:P |] ==> a:P";
+\ !!x. Q(x) ==> x:P |] ==> a:P";
by (rtac (p2 RS spec RS mp) 1);
by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
qed "wfd_strengthen_lemma";
@@ -64,7 +64,7 @@
(*** Lexicographic Ordering ***)
goalw Wfd.thy [lex_def]
- "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
+ "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
by (fast_tac ccl_cs 1);
qed "lexXH";
@@ -98,7 +98,7 @@
"[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
by (rewtac Wfd_def);
by (safe_tac ccl_cs);
-by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
+by (wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1);
by (fast_tac (term_cs addSEs [lex_pair]) 1);
by (subgoal_tac "ALL a b.<a,b>:P" 1);
by (fast_tac ccl_cs 1);
@@ -130,7 +130,7 @@
"Wfd(r) ==> Wfd(wmap(f,r))";
by (rewtac Wfd_def);
by (safe_tac ccl_cs);
-by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
+by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1);
by (fast_tac ccl_cs 1);
by (rtac (wf RS wfd_induct RS allI) 1);
by (safe_tac ccl_cs);
@@ -175,11 +175,11 @@
by (rtac Empty_wf 1);
qed "wf_wf";
-goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
+goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
by (fast_tac set_cs 1);
qed "NatPRXH";
-goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
+goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
by (fast_tac set_cs 1);
qed "ListPRXH";
@@ -188,7 +188,7 @@
goalw Wfd.thy [Wfd_def] "Wfd(NatPR)";
by (safe_tac set_cs);
-by (wfd_strengthen_tac "%x.x:Nat" 1);
+by (wfd_strengthen_tac "%x. x:Nat" 1);
by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
by (etac Nat_ind 1);
by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
@@ -196,7 +196,7 @@
goalw Wfd.thy [Wfd_def] "Wfd(ListPR(A))";
by (safe_tac set_cs);
-by (wfd_strengthen_tac "%x.x:List(A)" 1);
+by (wfd_strengthen_tac "%x. x:List(A)" 1);
by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
by (etac List_ind 1);
by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
--- a/src/CCL/Wfd.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Wfd.thy Fri Oct 10 17:10:12 1997 +0200
@@ -21,14 +21,14 @@
rules
Wfd_def
- "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"
+ "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
- wf_def "wf(R) == {x.x:R & Wfd(R)}"
+ wf_def "wf(R) == {x. x:R & Wfd(R)}"
wmap_def "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"
lex_def
- "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
+ "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
- NatPR_def "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
- ListPR_def "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
+ NatPR_def "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
+ ListPR_def "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
end
--- a/src/CCL/coinduction.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/coinduction.ML Fri Oct 10 17:10:12 1997 +0200
@@ -48,7 +48,7 @@
["<true,true> : POgen(R)",
"<false,false> : POgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
- "[|!!x. <b(x),b'(x)> : R |] ==><lam x.b(x),lam x.b'(x)> : POgen(R)",
+ "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)",
"<one,one> : POgen(R)",
"<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> \
\ <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
@@ -78,7 +78,7 @@
["<true,true> : EQgen(R)",
"<false,false> : EQgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
- "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
+ "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)",
"<one,one> : EQgen(R)",
"<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
\ <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
--- a/src/CCL/equalities.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/equalities.ML Fri Oct 10 17:10:12 1997 +0200
@@ -64,11 +64,11 @@
(** Simple properties of Compl -- complement of a set **)
-goal Set.thy "A Int Compl(A) = {x.False}";
+goal Set.thy "A Int Compl(A) = {x. False}";
by (fast_tac eq_cs 1);
qed "Compl_disjoint";
-goal Set.thy "A Un Compl(A) = {x.True}";
+goal Set.thy "A Un Compl(A) = {x. True}";
by (fast_tac eq_cs 1);
qed "Compl_partition";
@@ -106,7 +106,7 @@
qed "Union_Un_distrib";
val prems = goal Set.thy
- "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
+ "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
qed "Union_disjoint";
--- a/src/CCL/eval.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/eval.ML Fri Oct 10 17:10:12 1997 +0200
@@ -14,7 +14,7 @@
fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
val prems = goalw thy [apply_def]
- "[| f ---> lam x.b(x); b(a) ---> c |] ==> f ` a ---> c";
+ "[| f ---> lam x. b(x); b(a) ---> c |] ==> f ` a ---> c";
by (ceval_tac prems);
qed "applyV";
@@ -35,7 +35,7 @@
qed "fixV";
val prems = goalw thy [letrec_def]
- "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
+ "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \
\ letrec g x be h(x,g) in g(t) ---> c";
by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
qed "letrecV";
@@ -69,19 +69,19 @@
(* Factorial *)
val prems = goal thy
- "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
+ "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
\ in f(succ(succ(zero))) ---> ?a";
by (ceval_tac []);
val prems = goal thy
- "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
+ "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
\ in f(succ(succ(succ(zero)))) ---> ?a";
by (ceval_tac []);
(* Less Than Or Equal *)
fun isle x y = prove_goal thy
- ("letrec f p be split(p,%m n.ncase(m,true,%x.ncase(n,false,%y.f(<x,y>)))) \
+ ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) \
\ in f(<"^x^","^y^">) ---> ?a")
(fn prems => [ceval_tac []]);
@@ -93,12 +93,12 @@
(* Reverse *)
val prems = goal thy
- "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
+ "letrec id l be lcase(l,[],%x xs. x$id(xs)) \
\ in id(zero$succ(zero)$[]) ---> ?a";
by (ceval_tac []);
val prems = goal thy
- "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
-\ in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
+ "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \
+\ in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a";
by (ceval_tac []);
--- a/src/CCL/ex/Flag.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Flag.thy Fri Oct 10 17:10:12 1997 +0200
@@ -24,11 +24,11 @@
white_def "white == inr(inl(one))"
blue_def "blue == inr(inr(one))"
- ccase_def "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
+ ccase_def "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
- flag_def "flag == lam l.letrec
+ flag_def "flag == lam l. letrec
flagx l be lcase(l,<[],<[],[]>>,
- %h t. split(flagx(t),%lr p.split(p,%lw lb.
+ %h t. split(flagx(t),%lr p. split(p,%lw lb.
ccase(h, <red$lr,<lw,lb>>,
<lr,<white$lw,lb>>,
<lr,<lw,blue$lb>>))))
--- a/src/CCL/ex/List.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.ML Fri Oct 10 17:10:12 1997 +0200
@@ -14,7 +14,7 @@
(****)
val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
- ["(f o g) = (%a.f(g(a)))",
+ ["(f o g) = (%a. f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
"map(f,x$xs) = f(x)$map(f,xs)",
@@ -44,7 +44,7 @@
(***)
val prems = goalw List.thy [map_def]
- "[| !!x.x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)";
+ "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)";
by (typechk_tac prems 1);
qed "mapT";
--- a/src/CCL/ex/List.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.thy Fri Oct 10 17:10:12 1997 +0200
@@ -22,15 +22,15 @@
rules
- map_def "map(f,l) == lrec(l,[],%x xs g.f(x)$g)"
- comp_def "f o g == (%x.f(g(x)))"
- append_def "l @ m == lrec(l,m,%x xs g.x$g)"
- mem_def "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
- filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
- flat_def "flat(l) == lrec(l,[],%h t g.h @ g)"
+ map_def "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+ comp_def "f o g == (%x. f(g(x)))"
+ append_def "l @ m == lrec(l,m,%x xs g. x$g)"
+ mem_def "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+ filter_def "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
+ flat_def "flat(l) == lrec(l,[],%h t g. h @ g)"
- insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
- isort_def "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
+ insert_def "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+ isort_def "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
partition_def
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
@@ -38,7 +38,7 @@
in part(l,[],[])"
qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
let p be partition(f`h,t)
- in split(p,%x y.qsortx(x) @ h$qsortx(y)))
+ in split(p,%x y. qsortx(x) @ h$qsortx(y)))
in qsortx(l)"
end
--- a/src/CCL/ex/Nat.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Nat.thy Fri Oct 10 17:10:12 1997 +0200
@@ -19,11 +19,11 @@
not_def "not(b) == if b then false else true"
- add_def "a #+ b == nrec(a,b,%x g.succ(g))"
- mult_def "a #* b == nrec(a,zero,%x g.b #+ g)"
- sub_def "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy)))
+ add_def "a #+ b == nrec(a,b,%x g. succ(g))"
+ mult_def "a #* b == nrec(a,zero,%x g. b #+ g)"
+ sub_def "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
in sub(a,b)"
- le_def "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy)))
+ le_def "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
in le(a,b)"
lt_def "a #< b == not(b #<= a)"
@@ -31,7 +31,7 @@
in div(a,b)"
ack_def
"ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
- ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))
+ ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
in ack(a,b)"
end
--- a/src/CCL/ex/Stream.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Stream.ML Fri Oct 10 17:10:12 1997 +0200
@@ -16,7 +16,7 @@
val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1);
+ "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
by (etac (XH_to_E ListsXH) 1);
@@ -27,9 +27,9 @@
(*** Mapping the identity function leaves a list unchanged ***)
-val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l";
+val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}" 1);
+ "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(%x. x,l) & y=l)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
by (etac (XH_to_E ListsXH) 1);
@@ -41,7 +41,7 @@
val prems = goal Stream.thy
"[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)";
-by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
+by (eq_coinduct3_tac "{p. EX x y. p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
\ x=map(f,l@m) & y=map(f,l) @ map(f,m))}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
@@ -57,7 +57,7 @@
val prems = goal Stream.thy
"[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
+ "{p. EX x y. p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
\ x=k @ l @ m & y=(k @ l) @ m)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
@@ -71,7 +71,7 @@
val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
+ "{p. EX x y. p=<x,y> & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac set_cs);
by (etac (XH_to_E IListsXH) 1);
@@ -103,7 +103,7 @@
goal Stream.thy "iter1(f,a) = iter2(f,a)";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
+ "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
1);
by (fast_tac (type_cs addSIs [napplyBzero RS sym,
napplyBzero RS sym RS arg_cong]) 1);
--- a/src/CCL/genrec.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/genrec.ML Fri Oct 10 17:10:12 1997 +0200
@@ -30,7 +30,7 @@
val prems = goalw Wfd.thy [letrec2_def]
"[| a : A; b : B; \
\ !!p q g.[| p:A; q:B; \
-\ ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
+\ ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
\ h(p,q,g) : D(p,q) |] ==> \
\ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
by (rtac (SPLITB RS subst) 1);
@@ -42,14 +42,14 @@
eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
qed "letrec2T";
-goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
+goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)";
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
qed "lemma";
val prems = goalw Wfd.thy [letrec3_def]
"[| a : A; b : B; c : C; \
\ !!p q r g.[| p:A; q:B; r:C; \
-\ ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
+\ ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
\ g(x,y,z) : D(x,y,z) |] ==>\
\ h(p,q,r,g) : D(p,q,r) |] ==> \
\ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
@@ -75,14 +75,14 @@
qed "rcallT";
val major::prems = goal Wfd.thy
- "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+ "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \
\ g(a,b) : E";
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
qed "rcall2T";
val major::prems = goal Wfd.thy
- "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
+ "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
\ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
\ g(a,b,c) : E";
@@ -116,7 +116,7 @@
qed "hyprcallT";
val prems = goal Wfd.thy
- "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+ "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \
\ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \
\ P";
@@ -128,7 +128,7 @@
val prems = goal Wfd.thy
"[| g(a,b,c) = d; \
-\ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+\ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
\ P";
@@ -149,13 +149,13 @@
qed "rmIH1";
val prems = goal Wfd.thy
- "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
+ "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
qed "rmIH2";
val prems = goal Wfd.thy
- "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+ "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
--- a/src/CCL/subset.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/subset.ML Fri Oct 10 17:10:12 1997 +0200
@@ -115,7 +115,7 @@
"(a : Compl(B)) <-> (~a:B)",
"(a : {b}) <-> (a=b)",
"(a : {}) <-> False",
- "(a : {x.P(x)}) <-> P(a)" ]);
+ "(a : {x. P(x)}) <-> P(a)" ]);
val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
--- a/src/CCL/typecheck.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/typecheck.ML Fri Oct 10 17:10:12 1997 +0200
@@ -35,9 +35,9 @@
fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
in map solve
["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
- "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
- "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
- "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
+ "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}",
+ "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}",
+ "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}",
"h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
] end;
@@ -54,12 +54,12 @@
qed "applyT2";
val prems = goal Type.thy
- "[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}";
+ "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}";
by (fast_tac (type_cs addSIs prems) 1);
qed "rcall_lemma1";
val prems = goal Type.thy
- "[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
+ "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}";
by (cut_facts_tac prems 1);
by (fast_tac (type_cs addSIs prems) 1);
qed "rcall_lemma2";
--- a/src/CTT/Arith.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Arith.ML Fri Oct 10 17:10:12 1997 +0200
@@ -385,7 +385,7 @@
[ (rew_tac(absdiff_typing::prems)) ]);
qed_goalw "modC_succ" Arith.thy [mod_def]
-"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
+"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
(fn prems=>
[ (rew_tac(absdiff_typing::prems)) ]);
@@ -429,7 +429,7 @@
(*for case analysis on whether a number is 0 or a successor*)
qed_goal "iszero_decidable" Arith.thy
- "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
+ "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
(fn prems=>
[ (NE_tac "a" 1),
--- a/src/CTT/Arith.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Arith.thy Fri Oct 10 17:10:12 1997 +0200
@@ -15,10 +15,10 @@
"#*",div,mod :: "[i,i]=>i" (infixr 70)
rules
- add_def "a#+b == rec(a, b, %u v.succ(v))"
- diff_def "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))"
+ add_def "a#+b == rec(a, b, %u v. succ(v))"
+ diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
absdiff_def "a|-|b == (a-b) #+ (b-a)"
mult_def "a#*b == rec(a, 0, %u v. b #+ v)"
- mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))"
- div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y.v))"
+ mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+ div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
end
--- a/src/CTT/Bool.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Bool.thy Fri Oct 10 17:10:12 1997 +0200
@@ -15,5 +15,5 @@
Bool_def "Bool == T+T"
true_def "true == inl(tt)"
false_def "false == inr(tt)"
- cond_def "cond(a,b,c) == when(a, %u.b, %u.c)"
+ cond_def "cond(a,b,c) == when(a, %u. b, %u. c)"
end
--- a/src/CTT/CTT.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/CTT.ML Fri Oct 10 17:10:12 1997 +0200
@@ -109,7 +109,7 @@
(*Simplify the parameter of a unary type operator.*)
qed_goal "subst_eqtyparg" CTT.thy
- "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
+ "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"
(fn prems=>
[ (rtac subst_typeL 1),
(rtac refl_type 2),
--- a/src/CTT/CTT.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/CTT.thy Fri Oct 10 17:10:12 1997 +0200
@@ -113,21 +113,21 @@
NE
"[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
- ==> rec(p, a, %u v.b(u,v)) : C(p)"
+ ==> rec(p, a, %u v. b(u,v)) : C(p)"
NEL
"[| p = q : N; a = c : C(0);
!!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |]
- ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
+ ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)"
NC0
"[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
- ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
+ ==> rec(0, a, %u v. b(u,v)) = a : C(0)"
NC_succ
"[| p: N; a: C(0);
!!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>
- rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
+ rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))"
(*The fourth Peano axiom. See page 91 of Martin-Lof's book*)
zero_ne_succ
@@ -136,54 +136,54 @@
(*The Product of a family of types*)
- ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
+ ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
ProdFL
"[| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
- PROD x:A.B(x) = PROD x:C.D(x)"
+ PROD x:A. B(x) = PROD x:C. D(x)"
ProdI
- "[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
+ "[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)"
ProdIL
"[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==>
- lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
+ lam x. b(x) = lam x. c(x) : PROD x:A. B(x)"
- ProdE "[| p : PROD x:A.B(x); a : A |] ==> p`a : B(a)"
- ProdEL "[| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a)"
+ ProdE "[| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)"
+ ProdEL "[| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)"
ProdC
"[| a : A; !!x. x:A ==> b(x) : B(x)|] ==>
- (lam x.b(x)) ` a = b(a) : B(a)"
+ (lam x. b(x)) ` a = b(a) : B(a)"
ProdC2
- "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
+ "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)"
(*The Sum of a family of types*)
- SumF "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type"
+ SumF "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
SumFL
- "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A.B(x) = SUM x:C.D(x)"
+ "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)"
- SumI "[| a : A; b : B(a) |] ==> <a,b> : SUM x:A.B(x)"
- SumIL "[| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
+ SumI "[| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
+ SumIL "[| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
SumE
- "[| p: SUM x:A.B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
- ==> split(p, %x y.c(x,y)) : C(p)"
+ "[| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
+ ==> split(p, %x y. c(x,y)) : C(p)"
SumEL
- "[| p=q : SUM x:A.B(x);
+ "[| p=q : SUM x:A. B(x);
!!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|]
- ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
+ ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)"
SumC
"[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
- ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
+ ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)"
- fst_def "fst(a) == split(a, %x y.x)"
- snd_def "snd(a) == split(a, %x y.y)"
+ fst_def "fst(a) == split(a, %x y. x)"
+ snd_def "snd(a) == split(a, %x y. y)"
(*The sum of two types*)
@@ -200,22 +200,22 @@
PlusE
"[| p: A+B; !!x. x:A ==> c(x): C(inl(x));
!!y. y:B ==> d(y): C(inr(y)) |]
- ==> when(p, %x.c(x), %y.d(y)) : C(p)"
+ ==> when(p, %x. c(x), %y. d(y)) : C(p)"
PlusEL
"[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x));
!!y. y: B ==> d(y) = f(y) : C(inr(y)) |]
- ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
+ ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)"
PlusC_inl
"[| a: A; !!x. x:A ==> c(x): C(inl(x));
!!y. y:B ==> d(y): C(inr(y)) |]
- ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
+ ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))"
PlusC_inr
"[| b: B; !!x. x:A ==> c(x): C(inl(x));
!!y. y:B ==> d(y): C(inr(y)) |]
- ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
+ ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))"
(*The type Eq*)
--- a/src/CTT/ex/elim.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/elim.ML Fri Oct 10 17:10:12 1997 +0200
@@ -148,7 +148,7 @@
writeln"Axiom of choice. Proof without fst, snd. Harder still!";
val prems = goal CTT.thy
- "[| A type; !!x.x:A ==> B(x) type; \
+ "[| A type; !!x. x:A ==> B(x) type; \
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
--- a/src/CTT/ex/equal.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/equal.ML Fri Oct 10 17:10:12 1997 +0200
@@ -24,7 +24,7 @@
(*in the "rec" formulation of addition, 0+n=n *)
val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z.succ(y)) = p : N";
+goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
by (rtac EqE 1);
by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
by (rew_tac prems);
@@ -33,7 +33,7 @@
(*the harder version, n+0=n: recursive, uses induction hypothesis*)
val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z.succ(z)) = p : N";
+goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
by (rtac EqE 1);
by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
by (hyp_rew_tac prems);
@@ -43,8 +43,8 @@
(*Associativity of addition*)
val prems =
goal CTT.thy
- "[| a:N; b:N; c:N |] ==> rec(rec(a, b, %x y.succ(y)), c, %x y.succ(y)) = \
-\ rec(a, rec(b, c, %x y.succ(y)), %x y.succ(y)) : N";
+ "[| a:N; b:N; c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
+\ rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
by (NE_tac "a" 1);
by (hyp_rew_tac prems);
result();
@@ -53,7 +53,7 @@
(*Martin-Lof (1984) page 62: pairing is surjective*)
val prems =
goal CTT.thy
- "p : Sum(A,B) ==> <split(p,%x y.x), split(p,%x y.y)> = p : Sum(A,B)";
+ "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
by (rtac EqE 1);
by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
by (DEPTH_SOLVE_1 (rew_tac prems)); (*!!!!!!!*)
@@ -62,7 +62,7 @@
val prems =
goal CTT.thy "[| a : A; b : B |] ==> \
-\ (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B.A";
+\ (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
by (rew_tac prems);
result();
@@ -71,7 +71,7 @@
val prems =
goal CTT.thy
"(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) = \
-\ lam x. x : PROD x:(SUM y:N.N). (SUM y:N.N)";
+\ lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)";
by (resolve_tac reduction_rls 1);
by (resolve_tac intrL_rls 3);
by (rtac EqE 4);
--- a/src/CTT/ex/typechk.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/typechk.ML Fri Oct 10 17:10:12 1997 +0200
@@ -45,17 +45,17 @@
result();
writeln"typechecking an application of fst";
-goal CTT.thy "(lam u. split(u, %v w.v)) ` <0, succ(0)> : ?A";
+goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
by (typechk_tac[]);
result();
writeln"typechecking the predecessor function";
-goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
+goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
by (typechk_tac[]);
result();
writeln"typechecking the addition function";
-goal CTT.thy "lam n. lam m. rec(n, m, %x y.succ(y)) : ?A";
+goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
by (typechk_tac[]);
result();
@@ -74,7 +74,7 @@
result();
writeln"typechecking fst (as a function object) ";
-goal CTT.thy "lam i. split(i, %j k.j) : ?A";
+goal CTT.thy "lam i. split(i, %j k. j) : ?A";
by (typechk_tac[]);
by N_tac;
result();
--- a/src/LCF/LCF.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/LCF.ML Fri Oct 10 17:10:12 1997 +0200
@@ -65,7 +65,7 @@
REPEAT(rstac(conjI::prems)1)]);
val ext = prove_goal thy
- "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
+ "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
prem RS eq_imp_less1,
prem RS eq_imp_less2]1)]);
@@ -79,7 +79,7 @@
val ap_term = refl RS cong;
val ap_thm = refl RSN (2,cong);
-val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"
+val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU"
(fn _ => [rtac less_anti_sym 1, rtac minimal 2,
rtac less_ext 1, rtac allI 1, rtac minimal 1]);
@@ -89,7 +89,7 @@
(fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
-val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)"
+val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
(fn prems => [rtac allI 1, rtac mp 1,
res_inst_tac[("p","b")]tr_cases 2,
fast_tac (FOL_cs addIs prems) 1]);
--- a/src/LCF/LCF.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/LCF.thy Fri Oct 10 17:10:12 1997 +0200
@@ -99,12 +99,12 @@
Note that "easiness" of types is not taken into account
because it cannot be expressed schematically; flatness could be. *)
- adm_less "adm(%x.t(x) << u(x))"
+ adm_less "adm(%x. t(x) << u(x))"
adm_not_less "adm(%x.~ t(x) << u)"
- adm_not_free "adm(%x.A)"
- adm_subst "adm(P) ==> adm(%x.P(t(x)))"
- adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
- adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
- adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
- adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
+ adm_not_free "adm(%x. A)"
+ adm_subst "adm(P) ==> adm(%x. P(t(x)))"
+ adm_conj "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
+ adm_disj "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
+ adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
+ adm_all "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
end
--- a/src/LCF/fix.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/fix.ML Fri Oct 10 17:10:12 1997 +0200
@@ -22,7 +22,7 @@
structure Fix:FIX =
struct
-val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
+val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))"
(fn _ => [rewtac eq_def,
REPEAT(rstac[adm_conj,adm_less]1)]);
@@ -41,7 +41,7 @@
val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
(fn _ => [tac]) RS spec;
-val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)"
+val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)"
(fn _ => [rtac tr_induct 1,
REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
@@ -80,7 +80,7 @@
val FIX2 = FIX_pair_conj RS conjunct2;
val induct2 = prove_goal LCF.thy
- "[| adm(%p.P(FST(p),SND(p))); P(UU::'a,UU::'b);\
+ "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\
\ ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
(fn prems => [EVERY1
[res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),