# HG changeset patch
# User wenzelm
# Date 1451422982 -3600
# Node ID e90c42077767781329d59d7be318db96bac2d15b
# Parent  a35d141e6c7512660fb6924d26d68faafb55e298
more symbols;

diff -r a35d141e6c75 -r e90c42077767 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Dec 29 21:54:18 2015 +0100
+++ b/src/CCL/CCL.thy	Tue Dec 29 22:03:02 2015 +0100
@@ -27,7 +27,7 @@
 
 consts
   (*** Evaluation Judgement ***)
-  Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl "--->" 20)
+  Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl "\<longlongrightarrow>" 20)
 
   (*** Bisimulations for pre-order and equality ***)
   po          ::       "['a,'a]\<Rightarrow>o"           (infixl "[=" 50)
@@ -48,28 +48,28 @@
   (**  inference in the theory CCL.                                                **)
 
 axiomatization where
-  trueV:       "true ---> true" and
-  falseV:      "false ---> false" and
-  pairV:       "<a,b> ---> <a,b>" and
-  lamV:        "\<And>b. lam x. b(x) ---> lam x. b(x)" and
+  trueV:       "true \<longlongrightarrow> true" and
+  falseV:      "false \<longlongrightarrow> false" and
+  pairV:       "<a,b> \<longlongrightarrow> <a,b>" and
+  lamV:        "\<And>b. lam x. b(x) \<longlongrightarrow> lam x. b(x)" and
 
-  caseVtrue:   "\<lbrakk>t ---> true; d ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
-  caseVfalse:  "\<lbrakk>t ---> false; e ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
-  caseVpair:   "\<lbrakk>t ---> <a,b>; f(a,b) ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
-  caseVlam:    "\<And>b. \<lbrakk>t ---> lam x. b(x); g(b) ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c"
+  caseVtrue:   "\<lbrakk>t \<longlongrightarrow> true; d \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
+  caseVfalse:  "\<lbrakk>t \<longlongrightarrow> false; e \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
+  caseVpair:   "\<lbrakk>t \<longlongrightarrow> <a,b>; f(a,b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
+  caseVlam:    "\<And>b. \<lbrakk>t \<longlongrightarrow> lam x. b(x); g(b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c"
 
-  (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
+  (*** Properties of evaluation: note that "t \<longlongrightarrow> c" impies that c is canonical ***)
 
 axiomatization where
-  canonical:  "\<lbrakk>t ---> c; c==true \<Longrightarrow> u--->v;
-                          c==false \<Longrightarrow> u--->v;
-                    \<And>a b. c==<a,b> \<Longrightarrow> u--->v;
-                      \<And>f. c==lam x. f(x) \<Longrightarrow> u--->v\<rbrakk> \<Longrightarrow>
-             u--->v"
+  canonical:  "\<lbrakk>t \<longlongrightarrow> c; c==true \<Longrightarrow> u\<longlongrightarrow>v;
+                          c==false \<Longrightarrow> u\<longlongrightarrow>v;
+                    \<And>a b. c==<a,b> \<Longrightarrow> u\<longlongrightarrow>v;
+                      \<And>f. c==lam x. f(x) \<Longrightarrow> u\<longlongrightarrow>v\<rbrakk> \<Longrightarrow>
+             u\<longlongrightarrow>v"
 
   (* Should be derivable - but probably a bitch! *)
 axiomatization where
-  substitute: "\<lbrakk>a==a'; t(a)--->c(a)\<rbrakk> \<Longrightarrow> t(a')--->c(a')"
+  substitute: "\<lbrakk>a==a'; t(a)\<longlongrightarrow>c(a)\<rbrakk> \<Longrightarrow> t(a')\<longlongrightarrow>c(a')"
 
   (************** LOGIC ***************)
 
diff -r a35d141e6c75 -r e90c42077767 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Dec 29 21:54:18 2015 +0100
+++ b/src/CCL/Wfd.thy	Tue Dec 29 22:03:02 2015 +0100
@@ -512,15 +512,15 @@
 lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
 
 lemma applyV [eval]:
-  assumes "f ---> lam x. b(x)"
-    and "b(a) ---> c"
-  shows "f ` a ---> c"
+  assumes "f \<longlongrightarrow> lam x. b(x)"
+    and "b(a) \<longlongrightarrow> c"
+  shows "f ` a \<longlongrightarrow> c"
   unfolding apply_def by (eval assms)
 
 lemma letV:
-  assumes 1: "t ---> a"
-    and 2: "f(a) ---> c"
-  shows "let x be t in f(x) ---> c"
+  assumes 1: "t \<longlongrightarrow> a"
+    and 2: "f(a) \<longlongrightarrow> c"
+  shows "let x be t in f(x) \<longlongrightarrow> c"
   apply (unfold let_def)
   apply (rule 1 [THEN canonical])
   apply (tactic \<open>
@@ -528,7 +528,7 @@
       eresolve_tac @{context} @{thms substitute} 1))\<close>)
   done
 
-lemma fixV: "f(fix(f)) ---> c \<Longrightarrow> fix(f) ---> c"
+lemma fixV: "f(fix(f)) \<longlongrightarrow> c \<Longrightarrow> fix(f) \<longlongrightarrow> c"
   apply (unfold fix_def)
   apply (rule applyV)
    apply (rule lamV)
@@ -536,8 +536,8 @@
   done
 
 lemma letrecV:
-  "h(t,\<lambda>y. letrec g x be h(x,g) in g(y)) ---> c \<Longrightarrow>  
-                 letrec g x be h(x,g) in g(t) ---> c"
+  "h(t,\<lambda>y. letrec g x be h(x,g) in g(y)) \<longlongrightarrow> c \<Longrightarrow>  
+                 letrec g x be h(x,g) in g(t) \<longlongrightarrow> c"
   apply (unfold letrec_def)
   apply (assumption | rule fixV applyV  lamV)+
   done
@@ -545,24 +545,24 @@
 lemmas [eval] = letV letrecV fixV
 
 lemma V_rls [eval]:
-  "true ---> true"
-  "false ---> false"
-  "\<And>b c t u. \<lbrakk>b--->true; t--->c\<rbrakk> \<Longrightarrow> if b then t else u ---> c"
-  "\<And>b c t u. \<lbrakk>b--->false; u--->c\<rbrakk> \<Longrightarrow> if b then t else u ---> c"
-  "\<And>a b. <a,b> ---> <a,b>"
-  "\<And>a b c t h. \<lbrakk>t ---> <a,b>; h(a,b) ---> c\<rbrakk> \<Longrightarrow> split(t,h) ---> c"
-  "zero ---> zero"
-  "\<And>n. succ(n) ---> succ(n)"
-  "\<And>c n t u. \<lbrakk>n ---> zero; t ---> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) ---> c"
-  "\<And>c n t u x. \<lbrakk>n ---> succ(x); u(x) ---> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) ---> c"
-  "\<And>c n t u. \<lbrakk>n ---> zero; t ---> c\<rbrakk> \<Longrightarrow> nrec(n,t,u) ---> c"
-  "\<And>c n t u x. \<lbrakk>n--->succ(x); u(x,nrec(x,t,u))--->c\<rbrakk> \<Longrightarrow> nrec(n,t,u)--->c"
-  "[] ---> []"
-  "\<And>h t. h$t ---> h$t"
-  "\<And>c l t u. \<lbrakk>l ---> []; t ---> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) ---> c"
-  "\<And>c l t u x xs. \<lbrakk>l ---> x$xs; u(x,xs) ---> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) ---> c"
-  "\<And>c l t u. \<lbrakk>l ---> []; t ---> c\<rbrakk> \<Longrightarrow> lrec(l,t,u) ---> c"
-  "\<And>c l t u x xs. \<lbrakk>l--->x$xs; u(x,xs,lrec(xs,t,u))--->c\<rbrakk> \<Longrightarrow> lrec(l,t,u)--->c"
+  "true \<longlongrightarrow> true"
+  "false \<longlongrightarrow> false"
+  "\<And>b c t u. \<lbrakk>b\<longlongrightarrow>true; t\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> if b then t else u \<longlongrightarrow> c"
+  "\<And>b c t u. \<lbrakk>b\<longlongrightarrow>false; u\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> if b then t else u \<longlongrightarrow> c"
+  "\<And>a b. <a,b> \<longlongrightarrow> <a,b>"
+  "\<And>a b c t h. \<lbrakk>t \<longlongrightarrow> <a,b>; h(a,b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> split(t,h) \<longlongrightarrow> c"
+  "zero \<longlongrightarrow> zero"
+  "\<And>n. succ(n) \<longlongrightarrow> succ(n)"
+  "\<And>c n t u. \<lbrakk>n \<longlongrightarrow> zero; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) \<longlongrightarrow> c"
+  "\<And>c n t u x. \<lbrakk>n \<longlongrightarrow> succ(x); u(x) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) \<longlongrightarrow> c"
+  "\<And>c n t u. \<lbrakk>n \<longlongrightarrow> zero; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> nrec(n,t,u) \<longlongrightarrow> c"
+  "\<And>c n t u x. \<lbrakk>n\<longlongrightarrow>succ(x); u(x,nrec(x,t,u))\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> nrec(n,t,u)\<longlongrightarrow>c"
+  "[] \<longlongrightarrow> []"
+  "\<And>h t. h$t \<longlongrightarrow> h$t"
+  "\<And>c l t u. \<lbrakk>l \<longlongrightarrow> []; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) \<longlongrightarrow> c"
+  "\<And>c l t u x xs. \<lbrakk>l \<longlongrightarrow> x$xs; u(x,xs) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) \<longlongrightarrow> c"
+  "\<And>c l t u. \<lbrakk>l \<longlongrightarrow> []; t \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> lrec(l,t,u) \<longlongrightarrow> c"
+  "\<And>c l t u x xs. \<lbrakk>l\<longlongrightarrow>x$xs; u(x,xs,lrec(xs,t,u))\<longlongrightarrow>c\<rbrakk> \<Longrightarrow> lrec(l,t,u)\<longlongrightarrow>c"
   unfolding data_defs by eval+
 
 
@@ -570,29 +570,29 @@
 
 schematic_goal
   "letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))  
-   in f(succ(succ(zero))) ---> ?a"
+   in f(succ(succ(zero))) \<longlongrightarrow> ?a"
   by eval
 
 schematic_goal
   "letrec f n be ncase(n,succ(zero),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>z h. succ(h))))  
-   in f(succ(succ(succ(zero)))) ---> ?a"
+   in f(succ(succ(succ(zero)))) \<longlongrightarrow> ?a"
   by eval
 
 subsection \<open>Less Than Or Equal\<close>
 
 schematic_goal
   "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
-   in f(<succ(zero), succ(zero)>) ---> ?a"
+   in f(<succ(zero), succ(zero)>) \<longlongrightarrow> ?a"
   by eval
 
 schematic_goal
   "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
-   in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
+   in f(<succ(zero), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
   by eval
 
 schematic_goal
   "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
-   in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
+   in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) \<longlongrightarrow> ?a"
   by eval
 
 
@@ -600,12 +600,12 @@
 
 schematic_goal
   "letrec id l be lcase(l,[],\<lambda>x xs. x$id(xs))  
-   in id(zero$succ(zero)$[]) ---> ?a"
+   in id(zero$succ(zero)$[]) \<longlongrightarrow> ?a"
   by eval
 
 schematic_goal
   "letrec rev l be lcase(l,[],\<lambda>x xs. lrec(rev(xs),x$[],\<lambda>y ys g. y$g))  
-   in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
+   in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) \<longlongrightarrow> ?a"
   by eval
 
 end