# 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]\prop" (infixl "--->" 20) + Eval :: "[i,i]\prop" (infixl "\" 20) (*** Bisimulations for pre-order and equality ***) po :: "['a,'a]\o" (infixl "[=" 50) @@ -48,28 +48,28 @@ (** inference in the theory CCL. **) axiomatization where - trueV: "true ---> true" and - falseV: "false ---> false" and - pairV: " ---> " and - lamV: "\b. lam x. b(x) ---> lam x. b(x)" and + trueV: "true \ true" and + falseV: "false \ false" and + pairV: " \ " and + lamV: "\b. lam x. b(x) \ lam x. b(x)" and - caseVtrue: "\t ---> true; d ---> c\ \ case(t,d,e,f,g) ---> c" and - caseVfalse: "\t ---> false; e ---> c\ \ case(t,d,e,f,g) ---> c" and - caseVpair: "\t ---> ; f(a,b) ---> c\ \ case(t,d,e,f,g) ---> c" and - caseVlam: "\b. \t ---> lam x. b(x); g(b) ---> c\ \ case(t,d,e,f,g) ---> c" + caseVtrue: "\t \ true; d \ c\ \ case(t,d,e,f,g) \ c" and + caseVfalse: "\t \ false; e \ c\ \ case(t,d,e,f,g) \ c" and + caseVpair: "\t \ ; f(a,b) \ c\ \ case(t,d,e,f,g) \ c" and + caseVlam: "\b. \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 ***) + (*** Properties of evaluation: note that "t \ c" impies that c is canonical ***) axiomatization where - canonical: "\t ---> c; c==true \ u--->v; - c==false \ u--->v; - \a b. c== \ u--->v; - \f. c==lam x. f(x) \ u--->v\ \ - u--->v" + canonical: "\t \ c; c==true \ u\v; + c==false \ u\v; + \a b. c== \ u\v; + \f. c==lam x. f(x) \ u\v\ \ + u\v" (* Should be derivable - but probably a bitch! *) axiomatization where - substitute: "\a==a'; t(a)--->c(a)\ \ t(a')--->c(a')" + substitute: "\a==a'; t(a)\c(a)\ \ t(a')\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 \ lam x. b(x)" + and "b(a) \ c" + shows "f ` a \ 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 \ a" + and 2: "f(a) \ c" + shows "let x be t in f(x) \ c" apply (unfold let_def) apply (rule 1 [THEN canonical]) apply (tactic \ @@ -528,7 +528,7 @@ eresolve_tac @{context} @{thms substitute} 1))\) done -lemma fixV: "f(fix(f)) ---> c \ fix(f) ---> c" +lemma fixV: "f(fix(f)) \ c \ fix(f) \ c" apply (unfold fix_def) apply (rule applyV) apply (rule lamV) @@ -536,8 +536,8 @@ done lemma letrecV: - "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" + "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" 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" - "\b c t u. \b--->true; t--->c\ \ if b then t else u ---> c" - "\b c t u. \b--->false; u--->c\ \ if b then t else u ---> c" - "\a b. ---> " - "\a b c t h. \t ---> ; h(a,b) ---> c\ \ split(t,h) ---> c" - "zero ---> zero" - "\n. succ(n) ---> succ(n)" - "\c n t u. \n ---> zero; t ---> c\ \ ncase(n,t,u) ---> c" - "\c n t u x. \n ---> succ(x); u(x) ---> c\ \ ncase(n,t,u) ---> c" - "\c n t u. \n ---> zero; t ---> c\ \ nrec(n,t,u) ---> c" - "\c n t u x. \n--->succ(x); u(x,nrec(x,t,u))--->c\ \ nrec(n,t,u)--->c" - "[] ---> []" - "\h t. h$t ---> h$t" - "\c l t u. \l ---> []; t ---> c\ \ lcase(l,t,u) ---> c" - "\c l t u x xs. \l ---> x$xs; u(x,xs) ---> c\ \ lcase(l,t,u) ---> c" - "\c l t u. \l ---> []; t ---> c\ \ lrec(l,t,u) ---> c" - "\c l t u x xs. \l--->x$xs; u(x,xs,lrec(xs,t,u))--->c\ \ lrec(l,t,u)--->c" + "true \ true" + "false \ false" + "\b c t u. \b\true; t\c\ \ if b then t else u \ c" + "\b c t u. \b\false; u\c\ \ if b then t else u \ c" + "\a b. \ " + "\a b c t h. \t \ ; h(a,b) \ c\ \ split(t,h) \ c" + "zero \ zero" + "\n. succ(n) \ succ(n)" + "\c n t u. \n \ zero; t \ c\ \ ncase(n,t,u) \ c" + "\c n t u x. \n \ succ(x); u(x) \ c\ \ ncase(n,t,u) \ c" + "\c n t u. \n \ zero; t \ c\ \ nrec(n,t,u) \ c" + "\c n t u x. \n\succ(x); u(x,nrec(x,t,u))\c\ \ nrec(n,t,u)\c" + "[] \ []" + "\h t. h$t \ h$t" + "\c l t u. \l \ []; t \ c\ \ lcase(l,t,u) \ c" + "\c l t u x xs. \l \ x$xs; u(x,xs) \ c\ \ lcase(l,t,u) \ c" + "\c l t u. \l \ []; t \ c\ \ lrec(l,t,u) \ c" + "\c l t u x xs. \l\x$xs; u(x,xs,lrec(xs,t,u))\c\ \ lrec(l,t,u)\c" unfolding data_defs by eval+ @@ -570,29 +570,29 @@ schematic_goal "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" + in f(succ(succ(zero))) \ ?a" by eval schematic_goal "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" + in f(succ(succ(succ(zero)))) \ ?a" by eval subsection \Less Than Or Equal\ schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) - in f() ---> ?a" + in f() \ ?a" by eval schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) - in f() ---> ?a" + in f() \ ?a" by eval schematic_goal "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) - in f() ---> ?a" + in f() \ ?a" by eval @@ -600,12 +600,12 @@ schematic_goal "letrec id l be lcase(l,[],\x xs. x$id(xs)) - in id(zero$succ(zero)$[]) ---> ?a" + in id(zero$succ(zero)$[]) \ ?a" by eval schematic_goal "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" + in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) \ ?a" by eval end