src/HOL/Recdef.thy
author nipkow
Wed Dec 13 09:32:55 2000 +0100 (2000-12-13)
changeset 10653 55f33da63366
parent 10212 33fe2d701ddd
child 10773 0deff0197496
permissions -rw-r--r--
small mods.
     1 (*  Title:      HOL/Recdef.thy
     2     ID:         $Id$
     3     Author:     Konrad Slind
     4 
     5 TFL: recursive function definitions.
     6 *)
     7 
     8 theory Recdef = Wellfounded_Relations + Datatype
     9 files
    10   "../TFL/utils.sml"
    11   "../TFL/usyntax.sml"
    12   "../TFL/thms.sml"
    13   "../TFL/dcterm.sml"
    14   "../TFL/rules.sml"
    15   "../TFL/thry.sml"
    16   "../TFL/tfl.sml"
    17   "../TFL/post.sml"
    18   "Tools/recdef_package.ML":
    19 
    20 setup RecdefPackage.setup
    21 
    22 lemmas [recdef_simp] =
    23   inv_image_def
    24   measure_def
    25   lex_prod_def
    26   less_Suc_eq [THEN iffD2]
    27 
    28 lemmas [recdef_cong] =
    29   if_cong
    30 
    31 lemma let_cong [recdef_cong]:
    32     "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
    33   by (unfold Let_def) blast
    34 
    35 lemmas [recdef_wf] =
    36   wf_trancl
    37   wf_less_than
    38   wf_lex_prod
    39   wf_inv_image
    40   wf_measure
    41   wf_pred_nat
    42   wf_same_fst
    43   wf_empty
    44 
    45 end