src/HOL/Recdef.thy
changeset 10773 0deff0197496
parent 10653 55f33da63366
child 11165 3b69feb7d053
     1.1 --- a/src/HOL/Recdef.thy	Wed Jan 03 21:23:13 2001 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Wed Jan 03 21:23:50 2001 +0100
     1.3 @@ -1,22 +1,58 @@
     1.4  (*  Title:      HOL/Recdef.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Konrad Slind
     1.7 +    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     1.8  
     1.9  TFL: recursive function definitions.
    1.10  *)
    1.11  
    1.12  theory Recdef = Wellfounded_Relations + Datatype
    1.13  files
    1.14 -  "../TFL/utils.sml"
    1.15 -  "../TFL/usyntax.sml"
    1.16 -  "../TFL/thms.sml"
    1.17 -  "../TFL/dcterm.sml"
    1.18 -  "../TFL/rules.sml"
    1.19 -  "../TFL/thry.sml"
    1.20 -  "../TFL/tfl.sml"
    1.21 -  "../TFL/post.sml"
    1.22 -  "Tools/recdef_package.ML":
    1.23 +  ("../TFL/utils.ML")
    1.24 +  ("../TFL/usyntax.ML")
    1.25 +  ("../TFL/dcterm.ML")
    1.26 +  ("../TFL/thms.ML")
    1.27 +  ("../TFL/rules.ML")
    1.28 +  ("../TFL/thry.ML")
    1.29 +  ("../TFL/tfl.ML")
    1.30 +  ("../TFL/post.ML")
    1.31 +  ("Tools/recdef_package.ML"):
    1.32 +
    1.33 +lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.34 +  by (blast intro: someI)
    1.35 +
    1.36 +lemma tfl_eq_True: "(x = True) --> x"
    1.37 +  by blast
    1.38 +
    1.39 +lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
    1.40 +  by blast
    1.41 +
    1.42 +lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
    1.43 +  by blast
    1.44  
    1.45 +lemma tfl_P_imp_P_iff_True: "P ==> P = True"
    1.46 +  by blast
    1.47 +
    1.48 +lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
    1.49 +  by blast
    1.50 +
    1.51 +lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
    1.52 +  by simp
    1.53 +
    1.54 +lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
    1.55 +  by blast
    1.56 +
    1.57 +lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.58 +  by blast
    1.59 +
    1.60 +use "../TFL/utils.ML"
    1.61 +use "../TFL/usyntax.ML"
    1.62 +use "../TFL/dcterm.ML"
    1.63 +use "../TFL/thms.ML"
    1.64 +use "../TFL/rules.ML"
    1.65 +use "../TFL/thry.ML"
    1.66 +use "../TFL/tfl.ML"
    1.67 +use "../TFL/post.ML"
    1.68 +use "Tools/recdef_package.ML"
    1.69  setup RecdefPackage.setup
    1.70  
    1.71  lemmas [recdef_simp] =