src/HOL/FunDef.thy
author wenzelm
Thu, 26 Apr 2007 16:39:10 +0200
changeset 22816 0eba117368d9
parent 22622 25693088396b
child 22838 466599ecf610
permissions -rw-r--r--
added header; tuned presentation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20324
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     1
(*  Title:      HOL/FunDef.thy
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     2
    ID:         $Id$
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
     4
*)
20324
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     5
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
     6
header {* General recursive function definitions *}
20324
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     7
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     8
theory FunDef
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
     9
imports Accessible_Part
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    10
uses
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    11
  ("Tools/function_package/sum_tools.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    12
  ("Tools/function_package/fundef_common.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    13
  ("Tools/function_package/fundef_lib.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    14
  ("Tools/function_package/inductive_wrap.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    15
  ("Tools/function_package/context_tree.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    16
  ("Tools/function_package/fundef_core.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    17
  ("Tools/function_package/mutual.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    18
  ("Tools/function_package/pattern_split.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    19
  ("Tools/function_package/fundef_package.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    20
  ("Tools/function_package/auto_term.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    21
begin
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    22
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    23
text {* Definitions with default value. *}
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    24
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    25
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
    26
  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    27
  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    28
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    29
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    30
  by (simp add: theI' THE_default_def)
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    31
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    32
lemma THE_default1_equality:
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    33
    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    34
  by (simp add: the1_equality THE_default_def)
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    35
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    36
lemma THE_default_none:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    37
    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    38
  by (simp add:THE_default_def)
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    39
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    40
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    41
lemma fundef_ex1_existence:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    42
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    43
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    44
  shows "G x (f x)"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    45
  apply (simp only: f_def)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    46
  apply (rule THE_defaultI')
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    47
  apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    48
  done
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    49
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    50
lemma fundef_ex1_uniqueness:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    51
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    52
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    53
  assumes elm: "G x (h x)"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    54
  shows "h x = f x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    55
  apply (simp only: f_def)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    56
  apply (rule THE_default1_equality [symmetric])
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    57
   apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    58
  apply (rule elm)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    59
  done
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    60
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    61
lemma fundef_ex1_iff:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    62
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    63
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    64
  shows "(G x y) = (f x = y)"
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    65
  apply (auto simp:ex1 f_def THE_default1_equality)
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    66
  apply (rule THE_defaultI')
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    67
  apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    68
  done
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    69
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    70
lemma fundef_default_value:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    71
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    72
  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    73
  assumes "\<not> D x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    74
  shows "f x = d x"
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    75
proof -
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    76
  have "\<not>(\<exists>y. G x y)"
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    77
  proof
21512
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    78
    assume "\<exists>y. G x y"
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    79
    hence "D x" using graph ..
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    80
    with `\<not> D x` show False ..
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    81
  qed
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    82
  hence "\<not>(\<exists>!y. G x y)" by blast
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    83
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    84
  thus ?thesis
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    85
    unfolding f_def
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    86
    by (rule THE_default_none)
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    87
qed
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    88
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    89
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    90
use "Tools/function_package/sum_tools.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    91
use "Tools/function_package/fundef_common.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    92
use "Tools/function_package/fundef_lib.ML"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20324
diff changeset
    93
use "Tools/function_package/inductive_wrap.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    94
use "Tools/function_package/context_tree.ML"
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    95
use "Tools/function_package/fundef_core.ML"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    96
use "Tools/function_package/mutual.ML"
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19934
diff changeset
    97
use "Tools/function_package/pattern_split.ML"
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21312
diff changeset
    98
use "Tools/function_package/auto_term.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    99
use "Tools/function_package/fundef_package.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   100
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   101
setup FundefPackage.setup
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   102
22622
25693088396b Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents: 22325
diff changeset
   103
lemma let_cong:
25693088396b Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents: 22325
diff changeset
   104
    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   105
  unfolding Let_def by blast
22622
25693088396b Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents: 22325
diff changeset
   106
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   107
lemmas [fundef_cong] =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   108
  let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   109
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   110
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   111
lemma split_cong [fundef_cong]:
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   112
  "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk>
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   113
    \<Longrightarrow> split f p = split g q"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   114
  by (auto simp: split_def)
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   115
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   116
lemma comp_cong [fundef_cong]:
22324
c95319d14332 added congruence rule for function composition
krauss
parents: 22268
diff changeset
   117
  "f (g x) = f' (g' x')
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   118
    ==>  (f o g) x = (f' o g') x'"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   119
  unfolding o_apply .
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   120
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   121
end