src/HOL/FunDef.thy
author wenzelm
Thu, 03 Aug 2006 15:03:11 +0200
changeset 20324 71d63a30cc96
parent 20270 3abe7dae681e
child 20523 36a59e5d0039
permissions -rw-r--r--
removed True_implies (cf. True_implies_equals); added header;
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
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     4
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     5
A package for general recursive function definitions. 
71d63a30cc96 removed True_implies (cf. True_implies_equals);
wenzelm
parents: 20270
diff changeset
     6
*)
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
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
     9
imports Accessible_Part Datatype Recdef
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    10
uses 
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    11
("Tools/function_package/sum_tools.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    12
("Tools/function_package/fundef_common.ML")
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    13
("Tools/function_package/fundef_lib.ML")
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    14
("Tools/function_package/context_tree.ML")
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    15
("Tools/function_package/fundef_prep.ML")
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    16
("Tools/function_package/fundef_proof.ML")
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    17
("Tools/function_package/termination.ML")
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    18
("Tools/function_package/mutual.ML")
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19934
diff changeset
    19
("Tools/function_package/pattern_split.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    20
("Tools/function_package/fundef_package.ML")
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    21
("Tools/function_package/fundef_datatype.ML")
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    22
("Tools/function_package/auto_term.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    23
begin
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    24
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    25
lemma fundef_ex1_existence:
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    26
assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    27
assumes ex1: "\<exists>!y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    28
shows "(x, f x)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    29
  by (simp only:f_def, rule theI', rule ex1)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    30
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    31
lemma fundef_ex1_uniqueness:
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    32
assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    33
assumes ex1: "\<exists>!y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    34
assumes elm: "(x, h x)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    35
shows "h x = f x"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    36
  by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    37
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    38
lemma fundef_ex1_iff:
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    39
assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    40
assumes ex1: "\<exists>!y. (x,y)\<in>G"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    41
shows "((x, y)\<in>G) = (f x = y)"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    42
  apply (auto simp:ex1 f_def the1_equality)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    43
  by (rule theI', rule ex1)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    44
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    45
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    46
subsection {* Projections *}
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    47
consts
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    48
  lpg::"(('a + 'b) * 'a) set"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    49
  rpg::"(('a + 'b) * 'b) set"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    50
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    51
inductive lpg
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    52
intros
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    53
  "(Inl x, x) : lpg"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    54
inductive rpg
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    55
intros
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    56
  "(Inr y, y) : rpg"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    57
definition
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    58
  "lproj x = (THE y. (x,y) : lpg)"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    59
  "rproj x = (THE y. (x,y) : rpg)"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    60
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    61
lemma lproj_inl:
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    62
  "lproj (Inl x) = x"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    63
  by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    64
lemma rproj_inr:
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    65
  "rproj (Inr x) = x"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    66
  by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    67
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    68
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    69
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    70
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    71
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
    72
use "Tools/function_package/fundef_common.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    73
use "Tools/function_package/fundef_lib.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    74
use "Tools/function_package/context_tree.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    75
use "Tools/function_package/fundef_prep.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    76
use "Tools/function_package/fundef_proof.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    77
use "Tools/function_package/termination.ML"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    78
use "Tools/function_package/mutual.ML"
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19934
diff changeset
    79
use "Tools/function_package/pattern_split.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    80
use "Tools/function_package/fundef_package.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    81
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    82
setup FundefPackage.setup
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    83
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    84
use "Tools/function_package/fundef_datatype.ML"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    85
setup FundefDatatype.setup
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    86
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    87
use "Tools/function_package/auto_term.ML"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    88
setup FundefAutoTerm.setup
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    89
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    90
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    91
lemmas [fundef_cong] = 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
    92
  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
    93
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    94
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
    95
lemma split_cong[fundef_cong]:
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
    96
  "\<lbrakk> \<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y; p = q \<rbrakk> 
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
    97
  \<Longrightarrow> split f p = split g q"
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
    98
  by (auto simp:split_def)
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
    99
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   100
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   101
end