src/CCL/Wfd.thy
 changeset 36319 8feb2c4bef1a parent 33317 b4534348b8fd child 38500 d5477ee35820
```--- a/src/CCL/Wfd.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CCL/Wfd.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -573,29 +573,29 @@

subsection {* Factorial *}

-lemma
+schematic_lemma
"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 eval

-lemma
+schematic_lemma
"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 eval

subsection {* Less Than Or Equal *}

-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(zero), succ(zero)>) ---> ?a"
by eval

-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval

-lemma
+schematic_lemma
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
@@ -603,12 +603,12 @@

subsection {* Reverse *}

-lemma
+schematic_lemma
"letrec id l be lcase(l,[],%x xs. x\$id(xs))
in id(zero\$succ(zero)\$[]) ---> ?a"
by eval

-lemma
+schematic_lemma
"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 eval```