src/CCL/Wfd.thy
changeset 36319 8feb2c4bef1a
parent 33317 b4534348b8fd
child 38500 d5477ee35820
     1.1 --- a/src/CCL/Wfd.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -573,29 +573,29 @@
     1.4  
     1.5  subsection {* Factorial *}
     1.6  
     1.7 -lemma
     1.8 +schematic_lemma
     1.9    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    1.10     in f(succ(succ(zero))) ---> ?a"
    1.11    by eval
    1.12  
    1.13 -lemma
    1.14 +schematic_lemma
    1.15    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
    1.16     in f(succ(succ(succ(zero)))) ---> ?a"
    1.17    by eval
    1.18  
    1.19  subsection {* Less Than Or Equal *}
    1.20  
    1.21 -lemma
    1.22 +schematic_lemma
    1.23    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    1.24     in f(<succ(zero), succ(zero)>) ---> ?a"
    1.25    by eval
    1.26  
    1.27 -lemma
    1.28 +schematic_lemma
    1.29    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    1.30     in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
    1.31    by eval
    1.32  
    1.33 -lemma
    1.34 +schematic_lemma
    1.35    "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
    1.36     in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
    1.37    by eval
    1.38 @@ -603,12 +603,12 @@
    1.39  
    1.40  subsection {* Reverse *}
    1.41  
    1.42 -lemma
    1.43 +schematic_lemma
    1.44    "letrec id l be lcase(l,[],%x xs. x$id(xs))  
    1.45     in id(zero$succ(zero)$[]) ---> ?a"
    1.46    by eval
    1.47  
    1.48 -lemma
    1.49 +schematic_lemma
    1.50    "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))  
    1.51     in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
    1.52    by eval