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.
wenzelm@7701
     1
(*  Title:      HOL/Recdef.thy
wenzelm@7701
     2
    ID:         $Id$
wenzelm@7701
     3
    Author:     Konrad Slind
wenzelm@5123
     4
wenzelm@7701
     5
TFL: recursive function definitions.
wenzelm@7701
     6
*)
wenzelm@7701
     7
nipkow@10212
     8
theory Recdef = Wellfounded_Relations + Datatype
wenzelm@7701
     9
files
wenzelm@7701
    10
  "../TFL/utils.sml"
wenzelm@7701
    11
  "../TFL/usyntax.sml"
wenzelm@7701
    12
  "../TFL/thms.sml"
wenzelm@7701
    13
  "../TFL/dcterm.sml"
wenzelm@7701
    14
  "../TFL/rules.sml"
wenzelm@7701
    15
  "../TFL/thry.sml"
wenzelm@7701
    16
  "../TFL/tfl.sml"
wenzelm@7701
    17
  "../TFL/post.sml"
wenzelm@8303
    18
  "Tools/recdef_package.ML":
wenzelm@6438
    19
wenzelm@6438
    20
setup RecdefPackage.setup
wenzelm@6438
    21
wenzelm@9855
    22
lemmas [recdef_simp] =
wenzelm@9855
    23
  inv_image_def
wenzelm@9855
    24
  measure_def
wenzelm@9855
    25
  lex_prod_def
wenzelm@9855
    26
  less_Suc_eq [THEN iffD2]
wenzelm@9855
    27
wenzelm@9855
    28
lemmas [recdef_cong] =
wenzelm@9855
    29
  if_cong
wenzelm@9855
    30
wenzelm@9855
    31
lemma let_cong [recdef_cong]:
wenzelm@9855
    32
    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
wenzelm@9855
    33
  by (unfold Let_def) blast
wenzelm@9855
    34
wenzelm@9855
    35
lemmas [recdef_wf] =
wenzelm@9855
    36
  wf_trancl
wenzelm@9855
    37
  wf_less_than
wenzelm@9855
    38
  wf_lex_prod
wenzelm@9855
    39
  wf_inv_image
wenzelm@9855
    40
  wf_measure
wenzelm@9855
    41
  wf_pred_nat
nipkow@10653
    42
  wf_same_fst
wenzelm@9855
    43
  wf_empty
wenzelm@9855
    44
wenzelm@6438
    45
end