src/HOL/FunDef.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22622 25693088396b
child 22816 0eba117368d9
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:      HOL/FunDef.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions. 
     6 *)
     7 
     8 theory FunDef
     9 imports Accessible_Part 
    10 uses 
    11 ("Tools/function_package/sum_tools.ML")
    12 ("Tools/function_package/fundef_common.ML")
    13 ("Tools/function_package/fundef_lib.ML")
    14 ("Tools/function_package/inductive_wrap.ML")
    15 ("Tools/function_package/context_tree.ML")
    16 ("Tools/function_package/fundef_core.ML")
    17 ("Tools/function_package/mutual.ML")
    18 ("Tools/function_package/pattern_split.ML")
    19 ("Tools/function_package/fundef_package.ML")
    20 ("Tools/function_package/auto_term.ML")
    21 begin
    22 
    23 section {* Definitions with default value *}
    24 
    25 definition
    26   THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    27   "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
    28 
    29 lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
    30   by (simp add:theI' THE_default_def)
    31 
    32 lemma THE_default1_equality: 
    33   "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
    34   by (simp add:the1_equality THE_default_def)
    35 
    36 lemma THE_default_none:
    37   "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
    38 by (simp add:THE_default_def)
    39 
    40 
    41 lemma fundef_ex1_existence:
    42 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    43 assumes ex1: "\<exists>!y. G x y"
    44 shows "G x (f x)"
    45   by (simp only:f_def, rule THE_defaultI', rule ex1)
    46 
    47 
    48 
    49 
    50 
    51 lemma fundef_ex1_uniqueness:
    52 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    53 assumes ex1: "\<exists>!y. G x y"
    54 assumes elm: "G x (h x)"
    55 shows "h x = f x"
    56   by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
    57 
    58 lemma fundef_ex1_iff:
    59 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    60 assumes ex1: "\<exists>!y. G x y"
    61 shows "(G x y) = (f x = y)"
    62   apply (auto simp:ex1 f_def THE_default1_equality)
    63   by (rule THE_defaultI', rule ex1)
    64 
    65 lemma fundef_default_value:
    66 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    67 assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
    68 assumes "\<not> D x"
    69 shows "f x = d x"
    70 proof -
    71   have "\<not>(\<exists>y. G x y)"
    72   proof
    73     assume "\<exists>y. G x y"
    74     hence "D x" using graph ..
    75     with `\<not> D x` show False ..
    76   qed
    77   hence "\<not>(\<exists>!y. G x y)" by blast
    78   
    79   thus ?thesis
    80     unfolding f_def
    81     by (rule THE_default_none)
    82 qed
    83 
    84 
    85 
    86 use "Tools/function_package/sum_tools.ML"
    87 use "Tools/function_package/fundef_common.ML"
    88 use "Tools/function_package/fundef_lib.ML"
    89 use "Tools/function_package/inductive_wrap.ML"
    90 use "Tools/function_package/context_tree.ML"
    91 use "Tools/function_package/fundef_core.ML"
    92 use "Tools/function_package/mutual.ML"
    93 use "Tools/function_package/pattern_split.ML"
    94 use "Tools/function_package/auto_term.ML"
    95 use "Tools/function_package/fundef_package.ML"
    96 
    97 setup FundefPackage.setup
    98 
    99 lemma let_cong:
   100     "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
   101   by (unfold Let_def) blast
   102 
   103 lemmas [fundef_cong] = 
   104   let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
   105 
   106 
   107 lemma split_cong[fundef_cong]:
   108   "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> 
   109   \<Longrightarrow> split f p = split g q"
   110   by (auto simp:split_def)
   111 
   112 lemma comp_cong[fundef_cong]:
   113   "f (g x) = f' (g' x')
   114   ==>  (f o g) x = (f' o g') x'"
   115 unfolding o_apply .
   116 
   117 end