--- a/HOL.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/HOL.ML Wed Mar 02 12:26:55 1994 +0100
@@ -337,6 +337,7 @@
fun sstac ths = EVERY' (map stac ths);
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
+
end;
open HOL_Lemmas;
--- a/List.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/List.ML Wed Mar 02 12:26:55 1994 +0100
@@ -52,7 +52,7 @@
(*Induction for the type 'a list *)
val prems = goalw List.thy [Nil_def,Cons_def]
"[| P(Nil); \
-\ !!x xs. P(xs) ==> P(Cons(x,xs)) |] ==> P(l)";
+\ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)";
by (rtac (Rep_List_inverse RS subst) 1); (*types force good instantiation*)
by (rtac (Rep_List RS List_induct) 1);
by (REPEAT (ares_tac prems 1
@@ -104,7 +104,7 @@
val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
val NIL_neq_CONS = sym RS CONS_neq_NIL;
-goalw List.thy [Nil_def,Cons_def] "Cons(x,xs) ~= Nil";
+goalw List.thy [Nil_def,Cons_def] "x # xs ~= Nil";
by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
val Cons_not_Nil = result();
@@ -128,7 +128,7 @@
addSDs [inj_onto_Abs_List RS inj_ontoD,
inj_Rep_List RS injD, Leaf_inject];
-goalw List.thy [Cons_def] "(Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)";
+goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
by (fast_tac List_cs 1);
val Cons_Cons_eq = result();
val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
@@ -157,13 +157,13 @@
by (ALLGOALS (asm_simp_tac list_free_ss));
val not_CONS_self = result();
-goal List.thy "!x. l ~= Cons(x,l)";
+goal List.thy "!x. l ~= x#l";
by (list_ind_tac "l" 1);
by (ALLGOALS (asm_simp_tac list_free_ss));
val not_Cons_self = result();
-goal List.thy "(xs ~= []) = (? y ys. xs = Cons(y,ys))";
+goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
by(list_ind_tac "xs" 1);
by(simp_tac list_free_ss 1);
by(asm_simp_tac list_free_ss 1);
@@ -240,7 +240,7 @@
(fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
val list_rec_Cons = prove_goalw List.thy [list_rec_def, Cons_def]
- "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"
+ "list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))"
(fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
end;
@@ -269,7 +269,7 @@
val Rep_map_Nil = result();
goalw List.thy [Rep_map_def]
- "Rep_map(f, Cons(x,xs)) = CONS(f(x), Rep_map(f,xs))";
+ "Rep_map(f, x#xs) = CONS(f(x), Rep_map(f,xs))";
by (rtac list_rec_Cons 1);
val Rep_map_Cons = result();
@@ -284,7 +284,7 @@
val prems = goalw List.thy [Abs_map_def]
"[| M: Sexp; N: Sexp |] ==> \
-\ Abs_map(g, CONS(M,N)) = Cons(g(M), Abs_map(g,N))";
+\ Abs_map(g, CONS(M,N)) = g(M) # Abs_map(g,N)";
by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
val Abs_map_CONS = result();
@@ -296,7 +296,7 @@
val def_list_rec_Nil = result();
val [rew] = goal List.thy
- "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(Cons(x,xs)) = h(x,xs,f(xs))";
+ "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(x#xs) = h(x,xs,f(xs))";
by (rewtac rew);
by (rtac list_rec_Cons 1);
val def_list_rec_Cons = result();
@@ -393,7 +393,7 @@
goal List.thy
"P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
-\ (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
+\ (!y ys. xs=y#ys --> P(f(y,ys))))";
by(list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac list_ss));
by(fast_tac HOL_cs 1);
--- a/List.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/List.thy Wed Mar 02 12:26:55 1994 +0100
@@ -28,7 +28,7 @@
NIL :: "'a node set"
CONS :: "['a node set, 'a node set] => 'a node set"
Nil :: "'a list"
- Cons :: "['a, 'a list] => 'a list"
+ "#" :: "['a, 'a list] => 'a list" (infixr 65)
List_case :: "['a node set, 'b, ['a node set, 'a node set]=>'b] => 'b"
List_rec :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
@@ -40,7 +40,7 @@
mem :: "['a, 'a list] => bool" (infixl 55)
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
- "@" :: "['a list, 'a list] => 'a list" (infixr 65)
+ "@" :: "['a list, 'a list] => 'a list" (infixl 65)
list_case :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
filter :: "['a => bool, 'a list] => 'a list"
@@ -54,11 +54,11 @@
"@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
translations
- "[x, xs]" == "Cons(x, [xs])"
- "[x]" == "Cons(x, [])"
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
"[]" == "Nil"
- "case xs of Nil => a | Cons(y,ys) => b" == "list_case(xs,a,%y ys.b)"
+ "case xs of Nil => a | y#ys => b" == "list_case(xs,a,%y ys.b)"
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"
@@ -77,12 +77,12 @@
(* Defining the Concrete Constructors *)
NIL_def "NIL == In0(Numb(0))"
- CONS_def "CONS(M, N) == In1(M . N)"
+ CONS_def "CONS(M, N) == In1(M $ N)"
(* Defining the Abstract Constructors *)
Nil_def "Nil == Abs_List(NIL)"
- Cons_def "Cons(x, xs) == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
+ Cons_def "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
List_case_def "List_case(M, c, d) == Case(M, %x.c, %u. Split(u, %x y.d(x, y)))"
@@ -101,7 +101,7 @@
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. Cons(g(N), r))"
+ "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, @x.True, %x xs r.x)"
@@ -111,10 +111,10 @@
mem_def "x mem xs == \
\ list_rec(xs, False, %y ys r. if(y=x, True, r))"
list_all_def "list_all(P, xs) == list_rec(xs, True, %x l r. P(x) & r)"
- map_def "map(f, xs) == list_rec(xs, [], %x l r. Cons(f(x),r))"
- append_def "xs@ys == list_rec(xs, ys, %x l r. Cons(x,r))"
+ map_def "map(f, xs) == list_rec(xs, [], %x l r. f(x)#r)"
+ append_def "xs@ys == list_rec(xs, ys, %x l r. x#r)"
filter_def "filter(P,xs) == \
-\ list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
+\ list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
end
--- a/Sexp.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Sexp.ML Wed Mar 02 12:26:55 1994 +0100
@@ -20,7 +20,7 @@
val major::prems = goal Sexp.thy
"[| ii: Sexp; !!a. P(Leaf(a)); !!k. P(Numb(k)); \
-\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i.j) \
+\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \
\ |] ==> P(ii)";
by (rtac (major RS (Sexp_def RS def_induct)) 1);
by (rtac Sexp_fun_mono 1);
@@ -41,7 +41,7 @@
addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
val Sexp_case_Numb = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M.N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
by (fast_tac (HOL_cs addIs [select_equality]
addSDs [Scons_inject]
addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
@@ -61,7 +61,7 @@
val Sexp_NumbI = result();
val prems = goal Sexp.thy
- "[| M: Sexp; N: Sexp |] ==> M.N : Sexp";
+ "[| M: Sexp; N: Sexp |] ==> M$N : Sexp";
by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
val Sexp_SconsI = result();
@@ -79,7 +79,7 @@
by (fast_tac (set_cs addIs [SexpI]) 1);
val range_Leaf_subset_Sexp = result();
-val [major] = goal Sexp.thy "M.N : Sexp ==> M: Sexp & N: Sexp";
+val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp";
by (rtac (major RS setup_induction) 1);
by (etac Sexp_induct 1);
by (ALLGOALS
@@ -101,12 +101,12 @@
pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <M, M.N> : pred_Sexp";
+ "[| M: Sexp; N: Sexp |] ==> <M, M$N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI1 = result();
val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <N, M.N> : pred_Sexp";
+ "[| M: Sexp; N: Sexp |] ==> <N, M$N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI2 = result();
@@ -126,8 +126,8 @@
val major::prems = goalw Sexp.thy [pred_Sexp_def]
"[| p : pred_Sexp; \
-\ !!M N. [| p = <M, M.N>; M: Sexp; N: Sexp |] ==> R; \
-\ !!M N. [| p = <N, M.N>; M: Sexp; N: Sexp |] ==> R \
+\ !!M N. [| p = <M, M$N>; M: Sexp; N: Sexp |] ==> R; \
+\ !!M N. [| p = <N, M$N>; M: Sexp; N: Sexp |] ==> R \
\ |] ==> R";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
@@ -159,7 +159,7 @@
val Sexp_rec_Numb = result();
goal Sexp.thy "!!M. [| M: Sexp; N: Sexp |] ==> \
-\ Sexp_rec(M.N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
+\ Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
by (rtac (Sexp_rec_unfold RS trans) 1);
by (asm_simp_tac(HOL_ss addsimps
[Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
--- a/Sexp.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Sexp.thy Wed Mar 02 12:26:55 1994 +0100
@@ -24,10 +24,10 @@
Sexp_case_def
"Sexp_case(M,c,d,e) == @ z. (? x. M=Leaf(x) & z=c(x)) \
\ | (? k. M=Numb(k) & z=d(k)) \
-\ | (? N1 N2. M = N1 . N2 & z=e(N1,N2))"
+\ | (? N1 N2. M = N1 $ N2 & z=e(N1,N2))"
pred_Sexp_def
- "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M.N>, <N, M.N>}"
+ "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}"
Sexp_rec_def
"Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M, \
--- a/Subst/AList.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/AList.ML Wed Mar 02 12:26:55 1994 +0100
@@ -19,15 +19,15 @@
(fn _ => [simp_tac alist_ss 1])
in map mk_thm
["alist_rec(Nil,c,d) = c",
- "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
+ "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
"assoc(v,d,Nil) = d",
- "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;
+ "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
(*********)
val prems = goal AList.thy
"[| P(Nil); \
-\ !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |] ==> P(l)";
+\ !!x y xs. P(xs) ==> P(<x,y>#xs) |] ==> P(l)";
by (list_ind_tac "l" 1);
by (resolve_tac prems 1);
by (rtac PairE 1);
@@ -43,7 +43,7 @@
(*
val prems = goal AList.thy
- "[| P(Nil); !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
+ "[| P(Nil); !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
by (alist_ind_tac "a" 1);
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
val alist_induct2 = result();
--- a/Subst/ROOT.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/ROOT.ML Wed Mar 02 12:26:55 1994 +0100
@@ -19,12 +19,13 @@
unifier - specification of unification and conditions for
correctness and termination
-To load, go to the parent directory and type use"Substitutions/ROOT.ML";
+To load, go to the parent directory and type use"Subst/ROOT.ML";
*)
HOL_build_completed; (*Cause examples to fail if HOL did*)
writeln"Root file for Substitutions and Unification";
+loadpath := ["Subst"];
use_thy "Subst/Setplus";
use_thy "Subst/AList";
--- a/Subst/Subst.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Subst.ML Wed Mar 02 12:26:55 1994 +0100
@@ -19,9 +19,9 @@
["Const(c) <| al = Const(c)",
"Comb(t,u) <| al = Comb(t <| al, u <| al)",
"Nil <> bl = bl",
- "Cons(<a,b>,al) <> bl = Cons(<a,b <| bl>, al <> bl)",
+ "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
"sdom(Nil) = {}",
- "sdom(Cons(<a,b>,al)) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
+ "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
];
(* This rewrite isn't always desired *)
val Var_subst = mk_thm "Var(x) <| al = assoc(x,Var(x),al)";
@@ -41,10 +41,10 @@
by (ALLGOALS (asm_simp_tac subst_ss));
val subst_mono = result() RS mp;
-goal Subst.thy "~ (Var(v) <: t) --> t <| Cons(<v,t <| s>,s) = t <| s";
+goal Subst.thy "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
by (imp_excluded_middle_tac "t = Var(v)" 1);
by (res_inst_tac [("P",
- "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| Cons(<v,t<|s>,s)=x<|s")]
+ "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
uterm_induct 2);
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
by (fast_tac HOL_cs 1);
@@ -58,13 +58,13 @@
by (ALLGOALS (fast_tac HOL_cs));
val agreement = result();
-goal Subst.thy "~ v: vars_of(t) --> t <| Cons(<v,u>,s) = t <| s";
+goal Subst.thy "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
by(simp_tac(subst_ss addsimps [agreement,Var_subst]
setloop (split_tac [expand_if])) 1);
val repl_invariance = result() RS mp;
val asms = goal Subst.thy
- "v : vars_of(t) --> w : vars_of(t <| Cons(<v,Var(w)>,s))";
+ "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
by (uterm_ind_tac "t" 1);
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
val Var_in_subst = result() RS mp;
@@ -112,7 +112,7 @@
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
val comp_assoc = result();
-goal Subst.thy "Cons(<w,Var(w) <| s>,s) =s= s";
+goal Subst.thy "<w,Var(w) <| s>#s =s= s";
by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
by (uterm_ind_tac "t" 1);
by (REPEAT (etac rev_mp 3));
--- a/Subst/Subst.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Subst.thy Wed Mar 02 12:26:55 1994 +0100
@@ -26,7 +26,7 @@
\ %x.Const(x), \
\ %u v q r.Comb(q,r))"
- comp_def "al <> bl == alist_rec(al,bl,%x y xs g.Cons(<x,y <| bl>,g))"
+ comp_def "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
sdom_def
"sdom(al) == alist_rec(al, {}, \
--- a/Subst/UTerm.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/UTerm.thy Wed Mar 02 12:26:55 1994 +0100
@@ -37,7 +37,7 @@
(*defining the concrete constructors*)
VAR_def "VAR(v) == In0(v)"
CONST_def "CONST(v) == In1(In0(v))"
- COMB_def "COMB(t,u) == In1(In1(t . u))"
+ COMB_def "COMB(t,u) == In1(In1(t $ u))"
(*defining the abstract constructors*)
Var_def "Var(v) == Abs_UTerm(VAR(Leaf(v)))"
Const_def "Const(c) == Abs_UTerm(CONST(Leaf(c)))"
--- a/Subst/Unifier.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Unifier.ML Wed Mar 02 12:26:55 1994 +0100
@@ -25,7 +25,7 @@
goal Unifier.thy
"~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
-\ Unifier(Cons(<v,r>,s),t,u)";
+\ Unifier(<v,r>#s,t,u)";
by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
val Cons_Unifier = result() RS mp RS mp RS mp;
@@ -49,7 +49,7 @@
val MGU_iff = result();
val [prem] = goal Unifier.thy
- "~ Var(v) <: t ==> MGUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
by (REPEAT_SOME (step_tac set_cs));
by (etac subst 1);
@@ -85,7 +85,7 @@
by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
val Idem_Nil = result();
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(Cons(<v,t>,Nil))";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
setloop (split_tac [expand_if])) 1);
by (fast_tac set_cs 1);
@@ -114,8 +114,8 @@
val prems = goal Unifier.thy
"x : sdom(s) --> ~x : srange(s) --> \
-\ ~vars_of(Var(x) <| s<>Cons(<x,Var(x)>,s)) = \
-\ vars_of(Var(x) <| Cons(<x,Var(x)>,s))";
+\ ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\ vars_of(Var(x) <| <x,Var(x)>#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI2] 1));
by(res_inst_tac [("x","x")] exI 1);
@@ -141,8 +141,8 @@
val prems = goal Unifier.thy
"~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\ ~vars_of(Var(w) <| s<>Cons(<x,Var(w)>,s)) = \
-\ vars_of(Var(w) <| Cons(<x,Var(w)>,s))";
+\ ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\ vars_of(Var(w) <| <x,Var(w)>#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI1] 1));
by(res_inst_tac [("x","w")] exI 1);
@@ -167,10 +167,10 @@
(* *)
(* fun unify Const(m) Const(n) = if m=n then Nil else Fail *)
(* | unify Const(m) _ = Fail *)
-(* | unify Var(v) t = if Var(v)<:t then Fail else Cons(<v,t>,Nil)*)
+(* | unify Var(v) t = if Var(v)<:t then Fail else <v,t>#Nil *)
(* | unify Comb(t,u) Const(n) = Fail *)
(* | unify Comb(t,u) Var(v) = if Var(v) <: Comb(t,u) then Fail *)
-(* else Cons(<v,Comb(t,u>,Nil) *)
+(* else <v,Comb(t,u>#Nil *)
(* | unify Comb(t,u) Comb(v,w) = let s = unify t v *)
(* in if s=Fail then Fail *)
(* else unify (u<|s) (w<|s); *)
@@ -191,7 +191,7 @@
val Unify2 = result() RS mp;
val [prem] = goalw Unifier.thy [MGIUnifier_def]
- "~Var(v) <: t ==> MGIUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
val Unify3 = result();
--- a/Subst/alist.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/alist.ML Wed Mar 02 12:26:55 1994 +0100
@@ -19,15 +19,15 @@
(fn _ => [simp_tac alist_ss 1])
in map mk_thm
["alist_rec(Nil,c,d) = c",
- "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
+ "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
"assoc(v,d,Nil) = d",
- "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;
+ "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
(*********)
val prems = goal AList.thy
"[| P(Nil); \
-\ !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |] ==> P(l)";
+\ !!x y xs. P(xs) ==> P(<x,y>#xs) |] ==> P(l)";
by (list_ind_tac "l" 1);
by (resolve_tac prems 1);
by (rtac PairE 1);
@@ -43,7 +43,7 @@
(*
val prems = goal AList.thy
- "[| P(Nil); !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
+ "[| P(Nil); !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
by (alist_ind_tac "a" 1);
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
val alist_induct2 = result();
--- a/Subst/subst.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/subst.ML Wed Mar 02 12:26:55 1994 +0100
@@ -19,9 +19,9 @@
["Const(c) <| al = Const(c)",
"Comb(t,u) <| al = Comb(t <| al, u <| al)",
"Nil <> bl = bl",
- "Cons(<a,b>,al) <> bl = Cons(<a,b <| bl>, al <> bl)",
+ "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
"sdom(Nil) = {}",
- "sdom(Cons(<a,b>,al)) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
+ "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
];
(* This rewrite isn't always desired *)
val Var_subst = mk_thm "Var(x) <| al = assoc(x,Var(x),al)";
@@ -41,10 +41,10 @@
by (ALLGOALS (asm_simp_tac subst_ss));
val subst_mono = result() RS mp;
-goal Subst.thy "~ (Var(v) <: t) --> t <| Cons(<v,t <| s>,s) = t <| s";
+goal Subst.thy "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
by (imp_excluded_middle_tac "t = Var(v)" 1);
by (res_inst_tac [("P",
- "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| Cons(<v,t<|s>,s)=x<|s")]
+ "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
uterm_induct 2);
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
by (fast_tac HOL_cs 1);
@@ -58,13 +58,13 @@
by (ALLGOALS (fast_tac HOL_cs));
val agreement = result();
-goal Subst.thy "~ v: vars_of(t) --> t <| Cons(<v,u>,s) = t <| s";
+goal Subst.thy "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
by(simp_tac(subst_ss addsimps [agreement,Var_subst]
setloop (split_tac [expand_if])) 1);
val repl_invariance = result() RS mp;
val asms = goal Subst.thy
- "v : vars_of(t) --> w : vars_of(t <| Cons(<v,Var(w)>,s))";
+ "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
by (uterm_ind_tac "t" 1);
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
val Var_in_subst = result() RS mp;
@@ -112,7 +112,7 @@
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
val comp_assoc = result();
-goal Subst.thy "Cons(<w,Var(w) <| s>,s) =s= s";
+goal Subst.thy "<w,Var(w) <| s>#s =s= s";
by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
by (uterm_ind_tac "t" 1);
by (REPEAT (etac rev_mp 3));
--- a/Subst/subst.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/subst.thy Wed Mar 02 12:26:55 1994 +0100
@@ -26,7 +26,7 @@
\ %x.Const(x), \
\ %u v q r.Comb(q,r))"
- comp_def "al <> bl == alist_rec(al,bl,%x y xs g.Cons(<x,y <| bl>,g))"
+ comp_def "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
sdom_def
"sdom(al) == alist_rec(al, {}, \
--- a/Subst/unifier.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/unifier.ML Wed Mar 02 12:26:55 1994 +0100
@@ -25,7 +25,7 @@
goal Unifier.thy
"~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
-\ Unifier(Cons(<v,r>,s),t,u)";
+\ Unifier(<v,r>#s,t,u)";
by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
val Cons_Unifier = result() RS mp RS mp RS mp;
@@ -49,7 +49,7 @@
val MGU_iff = result();
val [prem] = goal Unifier.thy
- "~ Var(v) <: t ==> MGUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
by (REPEAT_SOME (step_tac set_cs));
by (etac subst 1);
@@ -85,7 +85,7 @@
by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
val Idem_Nil = result();
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(Cons(<v,t>,Nil))";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
setloop (split_tac [expand_if])) 1);
by (fast_tac set_cs 1);
@@ -114,8 +114,8 @@
val prems = goal Unifier.thy
"x : sdom(s) --> ~x : srange(s) --> \
-\ ~vars_of(Var(x) <| s<>Cons(<x,Var(x)>,s)) = \
-\ vars_of(Var(x) <| Cons(<x,Var(x)>,s))";
+\ ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\ vars_of(Var(x) <| <x,Var(x)>#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI2] 1));
by(res_inst_tac [("x","x")] exI 1);
@@ -141,8 +141,8 @@
val prems = goal Unifier.thy
"~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\ ~vars_of(Var(w) <| s<>Cons(<x,Var(w)>,s)) = \
-\ vars_of(Var(w) <| Cons(<x,Var(w)>,s))";
+\ ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\ vars_of(Var(w) <| <x,Var(w)>#s)";
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
by (REPEAT (resolve_tac [impI,disjI1] 1));
by(res_inst_tac [("x","w")] exI 1);
@@ -167,10 +167,10 @@
(* *)
(* fun unify Const(m) Const(n) = if m=n then Nil else Fail *)
(* | unify Const(m) _ = Fail *)
-(* | unify Var(v) t = if Var(v)<:t then Fail else Cons(<v,t>,Nil)*)
+(* | unify Var(v) t = if Var(v)<:t then Fail else <v,t>#Nil *)
(* | unify Comb(t,u) Const(n) = Fail *)
(* | unify Comb(t,u) Var(v) = if Var(v) <: Comb(t,u) then Fail *)
-(* else Cons(<v,Comb(t,u>,Nil) *)
+(* else <v,Comb(t,u>#Nil *)
(* | unify Comb(t,u) Comb(v,w) = let s = unify t v *)
(* in if s=Fail then Fail *)
(* else unify (u<|s) (w<|s); *)
@@ -191,7 +191,7 @@
val Unify2 = result() RS mp;
val [prem] = goalw Unifier.thy [MGIUnifier_def]
- "~Var(v) <: t ==> MGIUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
val Unify3 = result();
--- a/Subst/uterm.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/uterm.thy Wed Mar 02 12:26:55 1994 +0100
@@ -37,7 +37,7 @@
(*defining the concrete constructors*)
VAR_def "VAR(v) == In0(v)"
CONST_def "CONST(v) == In1(In0(v))"
- COMB_def "COMB(t,u) == In1(In1(t . u))"
+ COMB_def "COMB(t,u) == In1(In1(t $ u))"
(*defining the abstract constructors*)
Var_def "Var(v) == Abs_UTerm(VAR(Leaf(v)))"
Const_def "Const(c) == Abs_UTerm(CONST(Leaf(c)))"
--- a/Univ.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/Univ.ML Wed Mar 02 12:26:55 1994 +0100
@@ -123,7 +123,7 @@
(** Scons vs Atom **)
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
@@ -182,30 +182,30 @@
(** Injectiveness of Scons **)
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> M<=M'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
by (cut_facts_tac [major] 1);
by (fast_tac (set_cs addSDs [Suc_inject]
addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
val Scons_inject_lemma1 = result();
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> N<=N'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
by (cut_facts_tac [major] 1);
by (fast_tac (set_cs addSDs [Suc_inject]
addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
val Scons_inject_lemma2 = result();
-val [major] = goal Univ.thy "M.N = M'.N' ==> M=M'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
val Scons_inject1 = result();
-val [major] = goal Univ.thy "M.N = M'.N' ==> N=N'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
val Scons_inject2 = result();
val [major,minor] = goal Univ.thy
- "[| M.N = M'.N'; [| M=M'; N=N' |] ==> P \
+ "[| M$N = M'$N'; [| M=M'; N=N' |] ==> P \
\ |] ==> P";
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
val Scons_inject = result();
@@ -215,7 +215,7 @@
by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
val Atom_Atom_eq = result();
-goal Univ.thy "(M.N = M'.N') = (M=M' & N=N')";
+goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
val Scons_Scons_eq = result();
@@ -223,7 +223,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
+goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
+goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
@@ -312,7 +312,7 @@
val ntrunc_Numb = result();
goalw Univ.thy [Scons_def,ntrunc_def]
- "ntrunc(Suc(k), M.N) = ntrunc(k,M) . ntrunc(k,N)";
+ "ntrunc(Suc(k), M$N) = ntrunc(k,M) $ ntrunc(k,N)";
by (safe_tac (set_cs addSIs [equalityI,imageI]));
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
by (REPEAT (rtac Suc_less_SucD 1 THEN
@@ -347,14 +347,14 @@
(*** Cartesian Product ***)
-goalw Univ.thy [uprod_def] "!!M N. [| M:A; N:B |] ==> (M.N) : A<*>B";
+goalw Univ.thy [uprod_def] "!!M N. [| M:A; N:B |] ==> (M$N) : A<*>B";
by (REPEAT (ares_tac [singletonI,UN_I] 1));
val uprodI = result();
(*The general elimination rule*)
val major::prems = goalw Univ.thy [uprod_def]
"[| c : A<*>B; \
-\ !!x y. [| x:A; y:B; c=x.y |] ==> P \
+\ !!x y. [| x:A; y:B; c=x$y |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
@@ -363,7 +363,7 @@
(*Elimination of a pair -- introduces no eigenvariables*)
val prems = goal Univ.thy
- "[| (M.N) : A<*>B; [| M:A; N:B |] ==> P \
+ "[| (M$N) : A<*>B; [| M:A; N:B |] ==> P \
\ |] ==> P";
by (rtac uprodE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
@@ -448,7 +448,7 @@
by (fast_tac set_cs 1);
val usum_mono = result();
-goalw Univ.thy [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M.N <= M'.N'";
+goalw Univ.thy [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M$N <= M'$N'";
by (fast_tac set_cs 1);
val Scons_mono = result();
@@ -463,7 +463,7 @@
(*** Split and Case ***)
-goalw Univ.thy [Split_def] "Split(M.N, c) = c(M,N)";
+goalw Univ.thy [Split_def] "Split(M$N, c) = c(M,N)";
by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
val Split = result();
@@ -483,11 +483,11 @@
by (fast_tac (set_cs addIs [equalityI]) 1);
val ntrunc_UN1 = result();
-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 (fast_tac (set_cs addIs [equalityI]) 1);
val Scons_UN1_x = result();
-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 (fast_tac (set_cs addIs [equalityI]) 1);
val Scons_UN1_y = result();
@@ -518,12 +518,12 @@
(*** Equality for Cartesian Product ***)
goal Univ.thy
- "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x.y,x'.y'>})) = {<M.N, M'.N'>}";
+ "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x$y,x'$y'>})) = {<M$N, M'$N'>}";
by (simp_tac univ_ss 1);
val dprod_lemma = result();
goalw Univ.thy [dprod_def]
- "!!r s. [| <M,M'>:r; <N,N'>:s |] ==> <M.N, M'.N'> : r<**>s";
+ "!!r s. [| <M,M'>:r; <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
by (REPEAT (ares_tac [UN_I] 1));
by (rtac (singletonI RS (dprod_lemma RS equalityD2 RS subsetD)) 1);
val dprodI = result();
@@ -531,7 +531,7 @@
(*The general elimination rule*)
val major::prems = goalw Univ.thy [dprod_def]
"[| c : r<**>s; \
-\ !!x y x' y'. [| <x,x'> : r; <y,y'> : s; c = <x.y,x'.y'> |] ==> P \
+\ !!x y x' y'. [| <x,x'> : r; <y,y'> : s; c = <x$y,x'$y'> |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1));
--- a/Univ.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Univ.thy Wed Mar 02 12:26:55 1994 +0100
@@ -29,7 +29,7 @@
Atom :: "('a+nat) => 'a node set"
Leaf :: "'a => 'a node set"
Numb :: "nat => 'a node set"
- "." :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
+ "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
In0,In1 :: "'a node set => 'a node set"
ntrunc :: "[nat, 'a node set] => 'a node set"
@@ -67,26 +67,26 @@
(*S-expression constructors*)
Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})"
- Scons_def "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+ Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
(*Leaf nodes, with arbitrary or nat labels*)
Leaf_def "Leaf == Atom o Inl"
Numb_def "Numb == Atom o Inr"
(*Injections of the "disjoint sum"*)
- In0_def "In0(M) == Numb(0) . M"
- In1_def "In1(M) == Numb(Suc(0)) . M"
+ In0_def "In0(M) == Numb(0) $ M"
+ In1_def "In1(M) == Numb(Suc(0)) $ M"
(*the set of nodes with depth less than k*)
ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
(*products and sums for the "universe"*)
- uprod_def "A<*>B == UN x:A. UN y:B. { (x.y) }"
+ uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }"
usum_def "A<+>B == In0``A Un In1``B"
(*the corresponding eliminators*)
- Split_def "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)"
+ Split_def "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \
\ | (? y . M = In1(y) & u = d(y))"
@@ -97,7 +97,7 @@
diag_def "diag(A) == UN x:A. {<x,x>}"
dprod_def "r<**>s == UN u:r. UN v:s. \
-\ split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))"
+\ split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
\ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"
--- a/ex/InSort.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/InSort.thy Wed Mar 02 12:26:55 1994 +0100
@@ -14,9 +14,9 @@
rules
ins_Nil "ins(f,x,[]) = [x]"
- ins_Cons "ins(f,x,Cons(y,ys)) = \
-\ if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+ ins_Cons "ins(f,x,y#ys) = \
+\ if(f(x,y), x#y#ys, y# ins(f,x,ys))"
insort_Nil "insort(f,[]) = []"
- insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+ insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
end
--- a/ex/PL.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/PL.ML Wed Mar 02 12:26:55 1994 +0100
@@ -158,7 +158,7 @@
by (simp_tac pl_ss 1);
val hyps_false = result();
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
+goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, (#v)->false)}";
by (simp_tac pl_ss 1);
val hyps_var = result();
@@ -250,7 +250,7 @@
(*For the case hyps(p,t)-insert(#v,Y) |- p;
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-goal PL.thy "!p.hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})";
+goal PL.thy "!p.hyps(p, t-{v}) <= insert((#v)->false, hyps(p,t)-{#v})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -260,8 +260,8 @@
val hyps_Diff = result() RS spec;
(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
- we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
-goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})";
+ we also have hyps(p,t)-{(#v)->false} <= hyps(p, insert(v,t)) *)
+goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -282,7 +282,7 @@
(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
+goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, (#v)->false})";
by (rtac pl_ind 1);
by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
--- a/ex/PL.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/PL.thy Wed Mar 02 12:26:55 1994 +0100
@@ -46,7 +46,7 @@
eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
var_inject "(#v = #w) ==> v = w"
imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R"
--- a/ex/Qsort.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Qsort.thy Wed Mar 02 12:26:55 1994 +0100
@@ -13,8 +13,8 @@
rules
qsort_Nil "qsort(le,[]) = []"
-qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
-\ Cons(x, qsort(le,[y:xs . le(x,y)]))"
+qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\ (x# qsort(le,[y:xs . le(x,y)]))"
(* computational induction.
The dependence of p on x but not xs is intentional.
@@ -22,6 +22,6 @@
qsort_ind
"[| P([]); \
\ !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
-\ P(Cons(x,xs)) |] \
+\ P(x#xs) |] \
\ ==> P(xs)"
end
--- a/ex/Simult.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Simult.thy Wed Mar 02 12:26:55 1994 +0100
@@ -50,7 +50,7 @@
"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
(*the concrete constants*)
- TCONS_def "TCONS(M,N) == In0(M . N)"
+ TCONS_def "TCONS(M,N) == In0(M $ N)"
FNIL_def "FNIL == In1(NIL)"
FCONS_def "FCONS(M,N) == In1(CONS(M,N))"
(*the abstract constants*)
--- a/ex/Sorting.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Sorting.thy Wed Mar 02 12:26:55 1994 +0100
@@ -18,13 +18,13 @@
sorted1_Nil "sorted1(f,[])"
sorted1_One "sorted1(f,[x])"
-sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
total_def "total(r) == (!x y. r(x,y) | r(y,x))"
transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))"
--- a/ex/Term.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Term.ML Wed Mar 02 12:26:55 1994 +0100
@@ -40,7 +40,7 @@
val [major,minor] = goal Term.thy
"[| M: Term(A); \
\ !!x zs. [| x: A; zs: List(Term(A)); zs: List({x.R(x)}) \
-\ |] ==> R(x.zs) \
+\ |] ==> R(x$zs) \
\ |] ==> R(M)";
by (rtac (major RS (Term_def RS def_induct)) 1);
by (rtac Term_fun_mono 1);
@@ -51,9 +51,9 @@
(*Induction on Term(A) followed by induction on List *)
val major::prems = goal Term.thy
"[| M: Term(A); \
-\ !!x. [| x: A |] ==> R(x.NIL); \
-\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x.zs) \
-\ |] ==> R(x . CONS(z,zs)) \
+\ !!x. [| x: A |] ==> R(x$NIL); \
+\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x$zs) \
+\ |] ==> R(x $ CONS(z,zs)) \
\ |] ==> R(M)";
by (rtac (major RS Term_induct) 1);
by (etac List_induct 1);
@@ -97,7 +97,7 @@
(*Induction for the abstract type 'a term*)
val prems = goal Term.thy
"[| !!x. R(App(x,Nil)); \
-\ !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts))) \
+\ !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts)) \
\ |] ==> R(t)";
by (rtac term_induct 1); (*types force good instantiation*)
by (etac rev_mp 1);
@@ -117,7 +117,7 @@
val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
(*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M.N : Term(A)";
+val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M$N : Term(A)";
by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
val APP_I = result();
@@ -143,7 +143,7 @@
val [prem1,prem2,A_subset_Sexp] = goal Term.thy
"[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \
-\ Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
+\ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
by (rtac (Term_rec_unfold RS trans) 1);
by (rtac (Split RS trans) 1);
by (simp_tac (HOL_ss addsimps
--- a/ex/Term.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Term.thy Wed Mar 02 12:26:55 1994 +0100
@@ -32,7 +32,7 @@
Rep_TList_def "Rep_TList == Rep_map(Rep_Term)"
Abs_TList_def "Abs_TList == Abs_map(Abs_Term)"
(*defining the abstract constants*)
- App_def "App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
+ App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
(*list recursion*)
Term_rec_def
"Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \
--- a/ex/insort.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/insort.thy Wed Mar 02 12:26:55 1994 +0100
@@ -14,9 +14,9 @@
rules
ins_Nil "ins(f,x,[]) = [x]"
- ins_Cons "ins(f,x,Cons(y,ys)) = \
-\ if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+ ins_Cons "ins(f,x,y#ys) = \
+\ if(f(x,y), x#y#ys, y# ins(f,x,ys))"
insort_Nil "insort(f,[]) = []"
- insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+ insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
end
--- a/ex/pl.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/pl.ML Wed Mar 02 12:26:55 1994 +0100
@@ -158,7 +158,7 @@
by (simp_tac pl_ss 1);
val hyps_false = result();
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
+goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, (#v)->false)}";
by (simp_tac pl_ss 1);
val hyps_var = result();
@@ -250,7 +250,7 @@
(*For the case hyps(p,t)-insert(#v,Y) |- p;
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-goal PL.thy "!p.hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})";
+goal PL.thy "!p.hyps(p, t-{v}) <= insert((#v)->false, hyps(p,t)-{#v})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -260,8 +260,8 @@
val hyps_Diff = result() RS spec;
(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
- we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
-goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})";
+ we also have hyps(p,t)-{(#v)->false} <= hyps(p, insert(v,t)) *)
+goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -282,7 +282,7 @@
(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
+goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, (#v)->false})";
by (rtac pl_ind 1);
by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
--- a/ex/pl.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/pl.thy Wed Mar 02 12:26:55 1994 +0100
@@ -46,7 +46,7 @@
eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
var_inject "(#v = #w) ==> v = w"
imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R"
--- a/ex/qsort.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/qsort.thy Wed Mar 02 12:26:55 1994 +0100
@@ -13,8 +13,8 @@
rules
qsort_Nil "qsort(le,[]) = []"
-qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
-\ Cons(x, qsort(le,[y:xs . le(x,y)]))"
+qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\ (x# qsort(le,[y:xs . le(x,y)]))"
(* computational induction.
The dependence of p on x but not xs is intentional.
@@ -22,6 +22,6 @@
qsort_ind
"[| P([]); \
\ !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
-\ P(Cons(x,xs)) |] \
+\ P(x#xs) |] \
\ ==> P(xs)"
end
--- a/ex/simult.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/simult.thy Wed Mar 02 12:26:55 1994 +0100
@@ -50,7 +50,7 @@
"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
(*the concrete constants*)
- TCONS_def "TCONS(M,N) == In0(M . N)"
+ TCONS_def "TCONS(M,N) == In0(M $ N)"
FNIL_def "FNIL == In1(NIL)"
FCONS_def "FCONS(M,N) == In1(CONS(M,N))"
(*the abstract constants*)
--- a/ex/sorting.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/sorting.thy Wed Mar 02 12:26:55 1994 +0100
@@ -18,13 +18,13 @@
sorted1_Nil "sorted1(f,[])"
sorted1_One "sorted1(f,[x])"
-sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
total_def "total(r) == (!x y. r(x,y) | r(y,x))"
transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))"
--- a/ex/term.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/term.ML Wed Mar 02 12:26:55 1994 +0100
@@ -40,7 +40,7 @@
val [major,minor] = goal Term.thy
"[| M: Term(A); \
\ !!x zs. [| x: A; zs: List(Term(A)); zs: List({x.R(x)}) \
-\ |] ==> R(x.zs) \
+\ |] ==> R(x$zs) \
\ |] ==> R(M)";
by (rtac (major RS (Term_def RS def_induct)) 1);
by (rtac Term_fun_mono 1);
@@ -51,9 +51,9 @@
(*Induction on Term(A) followed by induction on List *)
val major::prems = goal Term.thy
"[| M: Term(A); \
-\ !!x. [| x: A |] ==> R(x.NIL); \
-\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x.zs) \
-\ |] ==> R(x . CONS(z,zs)) \
+\ !!x. [| x: A |] ==> R(x$NIL); \
+\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x$zs) \
+\ |] ==> R(x $ CONS(z,zs)) \
\ |] ==> R(M)";
by (rtac (major RS Term_induct) 1);
by (etac List_induct 1);
@@ -97,7 +97,7 @@
(*Induction for the abstract type 'a term*)
val prems = goal Term.thy
"[| !!x. R(App(x,Nil)); \
-\ !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts))) \
+\ !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts)) \
\ |] ==> R(t)";
by (rtac term_induct 1); (*types force good instantiation*)
by (etac rev_mp 1);
@@ -117,7 +117,7 @@
val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
(*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M.N : Term(A)";
+val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M$N : Term(A)";
by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
val APP_I = result();
@@ -143,7 +143,7 @@
val [prem1,prem2,A_subset_Sexp] = goal Term.thy
"[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \
-\ Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
+\ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
by (rtac (Term_rec_unfold RS trans) 1);
by (rtac (Split RS trans) 1);
by (simp_tac (HOL_ss addsimps
--- a/ex/term.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/term.thy Wed Mar 02 12:26:55 1994 +0100
@@ -32,7 +32,7 @@
Rep_TList_def "Rep_TList == Rep_map(Rep_Term)"
Abs_TList_def "Abs_TList == Abs_map(Abs_Term)"
(*defining the abstract constants*)
- App_def "App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
+ App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
(*list recursion*)
Term_rec_def
"Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \
--- a/hol.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/hol.ML Wed Mar 02 12:26:55 1994 +0100
@@ -337,6 +337,7 @@
fun sstac ths = EVERY' (map stac ths);
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
+
end;
open HOL_Lemmas;
--- a/sexp.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/sexp.ML Wed Mar 02 12:26:55 1994 +0100
@@ -20,7 +20,7 @@
val major::prems = goal Sexp.thy
"[| ii: Sexp; !!a. P(Leaf(a)); !!k. P(Numb(k)); \
-\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i.j) \
+\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \
\ |] ==> P(ii)";
by (rtac (major RS (Sexp_def RS def_induct)) 1);
by (rtac Sexp_fun_mono 1);
@@ -41,7 +41,7 @@
addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
val Sexp_case_Numb = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M.N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
by (fast_tac (HOL_cs addIs [select_equality]
addSDs [Scons_inject]
addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
@@ -61,7 +61,7 @@
val Sexp_NumbI = result();
val prems = goal Sexp.thy
- "[| M: Sexp; N: Sexp |] ==> M.N : Sexp";
+ "[| M: Sexp; N: Sexp |] ==> M$N : Sexp";
by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
val Sexp_SconsI = result();
@@ -79,7 +79,7 @@
by (fast_tac (set_cs addIs [SexpI]) 1);
val range_Leaf_subset_Sexp = result();
-val [major] = goal Sexp.thy "M.N : Sexp ==> M: Sexp & N: Sexp";
+val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp";
by (rtac (major RS setup_induction) 1);
by (etac Sexp_induct 1);
by (ALLGOALS
@@ -101,12 +101,12 @@
pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <M, M.N> : pred_Sexp";
+ "[| M: Sexp; N: Sexp |] ==> <M, M$N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI1 = result();
val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <N, M.N> : pred_Sexp";
+ "[| M: Sexp; N: Sexp |] ==> <N, M$N> : pred_Sexp";
by (fast_tac (set_cs addIs prems) 1);
val pred_SexpI2 = result();
@@ -126,8 +126,8 @@
val major::prems = goalw Sexp.thy [pred_Sexp_def]
"[| p : pred_Sexp; \
-\ !!M N. [| p = <M, M.N>; M: Sexp; N: Sexp |] ==> R; \
-\ !!M N. [| p = <N, M.N>; M: Sexp; N: Sexp |] ==> R \
+\ !!M N. [| p = <M, M$N>; M: Sexp; N: Sexp |] ==> R; \
+\ !!M N. [| p = <N, M$N>; M: Sexp; N: Sexp |] ==> R \
\ |] ==> R";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
@@ -159,7 +159,7 @@
val Sexp_rec_Numb = result();
goal Sexp.thy "!!M. [| M: Sexp; N: Sexp |] ==> \
-\ Sexp_rec(M.N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
+\ Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
by (rtac (Sexp_rec_unfold RS trans) 1);
by (asm_simp_tac(HOL_ss addsimps
[Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
--- a/sexp.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/sexp.thy Wed Mar 02 12:26:55 1994 +0100
@@ -24,10 +24,10 @@
Sexp_case_def
"Sexp_case(M,c,d,e) == @ z. (? x. M=Leaf(x) & z=c(x)) \
\ | (? k. M=Numb(k) & z=d(k)) \
-\ | (? N1 N2. M = N1 . N2 & z=e(N1,N2))"
+\ | (? N1 N2. M = N1 $ N2 & z=e(N1,N2))"
pred_Sexp_def
- "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M.N>, <N, M.N>}"
+ "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}"
Sexp_rec_def
"Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M, \
--- a/univ.ML Thu Feb 24 14:45:57 1994 +0100
+++ b/univ.ML Wed Mar 02 12:26:55 1994 +0100
@@ -123,7 +123,7 @@
(** Scons vs Atom **)
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
@@ -182,30 +182,30 @@
(** Injectiveness of Scons **)
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> M<=M'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
by (cut_facts_tac [major] 1);
by (fast_tac (set_cs addSDs [Suc_inject]
addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
val Scons_inject_lemma1 = result();
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> N<=N'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
by (cut_facts_tac [major] 1);
by (fast_tac (set_cs addSDs [Suc_inject]
addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
val Scons_inject_lemma2 = result();
-val [major] = goal Univ.thy "M.N = M'.N' ==> M=M'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
val Scons_inject1 = result();
-val [major] = goal Univ.thy "M.N = M'.N' ==> N=N'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
val Scons_inject2 = result();
val [major,minor] = goal Univ.thy
- "[| M.N = M'.N'; [| M=M'; N=N' |] ==> P \
+ "[| M$N = M'$N'; [| M=M'; N=N' |] ==> P \
\ |] ==> P";
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
val Scons_inject = result();
@@ -215,7 +215,7 @@
by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
val Atom_Atom_eq = result();
-goal Univ.thy "(M.N = M'.N') = (M=M' & N=N')";
+goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
val Scons_Scons_eq = result();
@@ -223,7 +223,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
+goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
+goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
@@ -312,7 +312,7 @@
val ntrunc_Numb = result();
goalw Univ.thy [Scons_def,ntrunc_def]
- "ntrunc(Suc(k), M.N) = ntrunc(k,M) . ntrunc(k,N)";
+ "ntrunc(Suc(k), M$N) = ntrunc(k,M) $ ntrunc(k,N)";
by (safe_tac (set_cs addSIs [equalityI,imageI]));
by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
by (REPEAT (rtac Suc_less_SucD 1 THEN
@@ -347,14 +347,14 @@
(*** Cartesian Product ***)
-goalw Univ.thy [uprod_def] "!!M N. [| M:A; N:B |] ==> (M.N) : A<*>B";
+goalw Univ.thy [uprod_def] "!!M N. [| M:A; N:B |] ==> (M$N) : A<*>B";
by (REPEAT (ares_tac [singletonI,UN_I] 1));
val uprodI = result();
(*The general elimination rule*)
val major::prems = goalw Univ.thy [uprod_def]
"[| c : A<*>B; \
-\ !!x y. [| x:A; y:B; c=x.y |] ==> P \
+\ !!x y. [| x:A; y:B; c=x$y |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
@@ -363,7 +363,7 @@
(*Elimination of a pair -- introduces no eigenvariables*)
val prems = goal Univ.thy
- "[| (M.N) : A<*>B; [| M:A; N:B |] ==> P \
+ "[| (M$N) : A<*>B; [| M:A; N:B |] ==> P \
\ |] ==> P";
by (rtac uprodE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
@@ -448,7 +448,7 @@
by (fast_tac set_cs 1);
val usum_mono = result();
-goalw Univ.thy [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M.N <= M'.N'";
+goalw Univ.thy [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M$N <= M'$N'";
by (fast_tac set_cs 1);
val Scons_mono = result();
@@ -463,7 +463,7 @@
(*** Split and Case ***)
-goalw Univ.thy [Split_def] "Split(M.N, c) = c(M,N)";
+goalw Univ.thy [Split_def] "Split(M$N, c) = c(M,N)";
by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
val Split = result();
@@ -483,11 +483,11 @@
by (fast_tac (set_cs addIs [equalityI]) 1);
val ntrunc_UN1 = result();
-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 (fast_tac (set_cs addIs [equalityI]) 1);
val Scons_UN1_x = result();
-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 (fast_tac (set_cs addIs [equalityI]) 1);
val Scons_UN1_y = result();
@@ -518,12 +518,12 @@
(*** Equality for Cartesian Product ***)
goal Univ.thy
- "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x.y,x'.y'>})) = {<M.N, M'.N'>}";
+ "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x$y,x'$y'>})) = {<M$N, M'$N'>}";
by (simp_tac univ_ss 1);
val dprod_lemma = result();
goalw Univ.thy [dprod_def]
- "!!r s. [| <M,M'>:r; <N,N'>:s |] ==> <M.N, M'.N'> : r<**>s";
+ "!!r s. [| <M,M'>:r; <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
by (REPEAT (ares_tac [UN_I] 1));
by (rtac (singletonI RS (dprod_lemma RS equalityD2 RS subsetD)) 1);
val dprodI = result();
@@ -531,7 +531,7 @@
(*The general elimination rule*)
val major::prems = goalw Univ.thy [dprod_def]
"[| c : r<**>s; \
-\ !!x y x' y'. [| <x,x'> : r; <y,y'> : s; c = <x.y,x'.y'> |] ==> P \
+\ !!x y x' y'. [| <x,x'> : r; <y,y'> : s; c = <x$y,x'$y'> |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1));
--- a/univ.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/univ.thy Wed Mar 02 12:26:55 1994 +0100
@@ -29,7 +29,7 @@
Atom :: "('a+nat) => 'a node set"
Leaf :: "'a => 'a node set"
Numb :: "nat => 'a node set"
- "." :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
+ "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
In0,In1 :: "'a node set => 'a node set"
ntrunc :: "[nat, 'a node set] => 'a node set"
@@ -67,26 +67,26 @@
(*S-expression constructors*)
Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})"
- Scons_def "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+ Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
(*Leaf nodes, with arbitrary or nat labels*)
Leaf_def "Leaf == Atom o Inl"
Numb_def "Numb == Atom o Inr"
(*Injections of the "disjoint sum"*)
- In0_def "In0(M) == Numb(0) . M"
- In1_def "In1(M) == Numb(Suc(0)) . M"
+ In0_def "In0(M) == Numb(0) $ M"
+ In1_def "In1(M) == Numb(Suc(0)) $ M"
(*the set of nodes with depth less than k*)
ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
(*products and sums for the "universe"*)
- uprod_def "A<*>B == UN x:A. UN y:B. { (x.y) }"
+ uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }"
usum_def "A<+>B == In0``A Un In1``B"
(*the corresponding eliminators*)
- Split_def "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)"
+ Split_def "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \
\ | (? y . M = In1(y) & u = d(y))"
@@ -97,7 +97,7 @@
diag_def "diag(A) == UN x:A. {<x,x>}"
dprod_def "r<**>s == UN u:r. UN v:s. \
-\ split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))"
+\ split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
\ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"