univ.ML

 
 (*** Distinctness of constructors ***)
 
 (** 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);
 by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfstE, 
 			  Pair_inject, sym RS Push_neq_K0] 1

 val Push_Node_inject = result();
 
 
 (** 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();
 
 (*rewrite rules*)
 goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
 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();
 
 (*** Distinctness involving Leaf and Numb ***)
 
 (** 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();
 val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
 
 val Scons_neq_Leaf = standard (Scons_not_Leaf RS notE);
 val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
 
 (** 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();
 val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
 

 by (stac o_def 1);
 by (rtac ntrunc_Atom 1);
 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 
 	    rtac (ndepth_Push_Node RS subst) 1 THEN 
 	    assume_tac 1));

 val ntrunc_In1 = result();
 
 
 (*** 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
      ORELSE resolve_tac prems 1));
 val uprodE = result();
 
 (*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));
 val uprodE2 = result();
 

 
 goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
 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();
 
 goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));

 val In1_mono = result();
 
 
 (*** 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();
 
 goalw Univ.thy [Case_def] "Case(In0(M), c, d) = c(M)";
 by (fast_tac (set_cs addIs [select_equality] 

 
 goalw Univ.thy [ntrunc_def] "ntrunc(k, UN x.f(x)) = (UN x. ntrunc(k, f(x)))";
 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();
 
 goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
 br Scons_UN1_y 1;

 val diagE = result();
 
 (*** 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();
 
 (*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));
 by (res_inst_tac [("p","u")] PairE 1);
 by (res_inst_tac [("p","v")] PairE 1);