improved recdef setup;
authorwenzelm
Tue Sep 05 18:48:04 2000 +0200 (2000-09-05)
changeset 9855709a295731e2
parent 9854 a1383b55ac05
child 9856 c34d3c94298c
improved recdef setup;
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Recdef.thy	Tue Sep 05 18:47:46 2000 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Tue Sep 05 18:48:04 2000 +0200
     1.3 @@ -7,30 +7,38 @@
     1.4  
     1.5  theory Recdef = WF_Rel + Datatype
     1.6  files
     1.7 -  (*establish a base of common and/or helpful functions*)
     1.8 -  "../TFL/utils.sig"
     1.9 -
    1.10 -  "../TFL/usyntax.sig"
    1.11 -  "../TFL/rules.sig"
    1.12 -  "../TFL/thry.sig"
    1.13 -  "../TFL/thms.sig"
    1.14 -  "../TFL/tfl.sig"
    1.15    "../TFL/utils.sml"
    1.16 -
    1.17 -  (*supply implementations*)
    1.18    "../TFL/usyntax.sml"
    1.19    "../TFL/thms.sml"
    1.20    "../TFL/dcterm.sml"
    1.21    "../TFL/rules.sml"
    1.22    "../TFL/thry.sml"
    1.23 -
    1.24 -  (*link system and specialize for Isabelle*)
    1.25    "../TFL/tfl.sml"
    1.26    "../TFL/post.sml"
    1.27 -
    1.28 -  (*theory extender wrapper module*)
    1.29    "Tools/recdef_package.ML":
    1.30  
    1.31  setup RecdefPackage.setup
    1.32  
    1.33 +lemmas [recdef_simp] =
    1.34 +  inv_image_def
    1.35 +  measure_def
    1.36 +  lex_prod_def
    1.37 +  less_Suc_eq [THEN iffD2]
    1.38 +
    1.39 +lemmas [recdef_cong] =
    1.40 +  if_cong
    1.41 +
    1.42 +lemma let_cong [recdef_cong]:
    1.43 +    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
    1.44 +  by (unfold Let_def) blast
    1.45 +
    1.46 +lemmas [recdef_wf] =
    1.47 +  wf_trancl
    1.48 +  wf_less_than
    1.49 +  wf_lex_prod
    1.50 +  wf_inv_image
    1.51 +  wf_measure
    1.52 +  wf_pred_nat
    1.53 +  wf_empty
    1.54 +
    1.55  end