equal
deleted
inserted
replaced
1 (* Title: HOL/Lambda/WeakNorm.thy |
1 (* Title: HOL/Lambda/WeakNorm.thy |
2 ID: $Id$ |
|
3 Author: Stefan Berghofer |
2 Author: Stefan Berghofer |
4 Copyright 2003 TU Muenchen |
3 Copyright 2003 TU Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header {* Weak normalization for simply-typed lambda calculus *} |
6 header {* Weak normalization for simply-typed lambda calculus *} |
428 |
427 |
429 fun dummyf _ = error "dummy"; |
428 fun dummyf _ = error "dummy"; |
430 |
429 |
431 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
430 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
432 val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1)); |
431 val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1)); |
433 val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
432 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
434 |
433 |
435 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
434 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
436 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2)); |
435 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2)); |
437 val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
436 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
438 *} |
437 *} |
439 |
438 |
440 text {* |
439 text {* |
441 The same story again for the SML code generator. |
440 The same story again for the SML code generator. |
442 *} |
441 *} |
503 *} |
502 *} |
504 |
503 |
505 ML {* |
504 ML {* |
506 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
505 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; |
507 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1)); |
506 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1)); |
508 val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
507 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); |
509 |
508 |
510 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
509 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"}; |
511 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2)); |
510 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2)); |
512 val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
511 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); |
513 *} |
512 *} |
514 |
513 |
515 end |
514 end |