no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
authorkrauss
Mon Aug 31 20:32:00 2009 +0200 (2009-08-31)
changeset 32461eee4fa79398f
parent 32460 ba0cf920a39c
child 32462 c33faa289520
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 17:32:29 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 20:32:00 2009 +0200
     1.3 @@ -97,6 +97,14 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +text {* Code generator setup (FIXME!) *}
     1.8 +
     1.9 +consts_code
    1.10 +  "wfrec"   ("\<module>wfrec?")
    1.11 +attach {*
    1.12 +fun wfrec f x = f (wfrec f) x;
    1.13 +*}
    1.14 +
    1.15  consts
    1.16  
    1.17    method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     2.1 --- a/src/HOL/Wellfounded.thy	Mon Aug 31 17:32:29 2009 +0200
     2.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
     2.3 @@ -464,14 +464,6 @@
     2.4  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
     2.5  done
     2.6  
     2.7 -subsection {* Code generator setup *}
     2.8 -
     2.9 -consts_code
    2.10 -  "wfrec"   ("\<module>wfrec?")
    2.11 -attach {*
    2.12 -fun wfrec f x = f (wfrec f) x;
    2.13 -*}
    2.14 -
    2.15  
    2.16  subsection {* @{typ nat} is well-founded *}
    2.17