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