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