author haftmann Fri, 23 Mar 2007 12:05:43 +0100 changeset 22512 04242efdcece parent 22511 ca326e0fb5c5 child 22513 651777b8dc30
fixed typing bug in generated code
```--- a/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 10:50:03 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 12:05:43 2007 +0100
@@ -6,7 +6,9 @@

header {* Weak normalization for simply-typed lambda calculus *}

-theory WeakNorm imports Type begin
+theory WeakNorm
+imports Type
+begin

text {*
Formalization by Stefan Berghofer. Partly based on a paper proof by
@@ -554,15 +556,11 @@
*}

ML {*
-val thy = the_context ();
-fun rd s = read_cterm thy (s, TypeInfer.logicT);
-
-val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
+val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
val ct1' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct1)) dB1);

-val ct2 = rd
-  "%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)))))";
+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)))))"};
val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
@@ -584,8 +582,8 @@
structure Lambda = ROOT.Lambda;
structure Nat = ROOT.Nat;

-val nat_of_int = ROOT.Integer.nat;
-val int_of_nat = ROOT.Integer.int;
+val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
+val int_of_nat = IntInf.toInt o ROOT.Integer.int;

fun dBtype_of_typ (Type ("fun", [T, U])) =
Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
@@ -630,13 +628,12 @@
*}

ML {*
-val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
+val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct1));
val ct1' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct1)) dB1);

-val ct2 = rd
-  "%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)))))";
-val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
+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)))))"};
+val (dB2, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct2));
val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
```