src/HOL/FunDef.thy
author krauss
Mon, 22 Jan 2007 17:29:43 +0100
changeset 22166 0a50d4db234a
parent 21512 3786eb1b69d6
child 22268 ee2619267dca
permissions -rw-r--r--
* Preliminary implementation of tail recursion * Clarified internal interfaces
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")
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20324
diff changeset
    14
("Tools/function_package/inductive_wrap.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    15
("Tools/function_package/context_tree.ML")
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    16
("Tools/function_package/fundef_core.ML")
19564
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/auto_term.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    22
begin
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    23
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    24
section {* Wellfoundedness and Accessibility: Predicate versions *}
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    25
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    26
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    27
constdefs
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    28
  wfP         :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    29
  "wfP(r) == (!P. (!x. (!y. r y x --> P(y)) --> P(x)) --> (!x. P(x)))"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    30
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    31
lemma wfP_induct: 
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    32
    "[| wfP r;           
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    33
        !!x.[| ALL y. r y x --> P(y) |] ==> P(x)  
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    34
     |]  ==>  P(a)"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    35
by (unfold wfP_def, blast)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    36
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    37
lemmas wfP_induct_rule = wfP_induct [rule_format, consumes 1, case_names less]
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    38
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    39
definition in_rel_def[simp]:
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    40
  "in_rel R x y == (x, y) \<in> R"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    41
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    42
lemma wf_in_rel:
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    43
  "wf R \<Longrightarrow> wfP (in_rel R)"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    44
  unfolding wfP_def wf_def in_rel_def .
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    45
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    46
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    47
inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    48
  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
21364
3baf57a27269 inductive2: canonical specification syntax;
wenzelm
parents: 21319
diff changeset
    49
where
3baf57a27269 inductive2: canonical specification syntax;
wenzelm
parents: 21319
diff changeset
    50
  accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    51
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    52
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    53
theorem accP_induct:
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    54
  assumes major: "accP r a"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    55
  assumes hyp: "!!x. accP r x ==> \<forall>y. r y x --> P y ==> P x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    56
  shows "P a"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    57
  apply (rule major [THEN accP.induct])
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    58
  apply (rule hyp)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    59
   apply (rule accPI)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    60
   apply fast
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    61
  apply fast
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    62
  done
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    63
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    64
theorems accP_induct_rule = accP_induct [rule_format, induct set: accP]
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    65
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    66
theorem accP_downward: "accP r b ==> r a b ==> accP r a"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    67
  apply (erule accP.cases)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    68
  apply fast
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    69
  done
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    70
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    71
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    72
lemma not_accP_down:
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    73
  assumes na: "\<not> accP R x"
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    74
  obtains z where "R z x" and "\<not>accP R z"
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    75
proof -
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    76
  assume a: "\<And>z. \<lbrakk>R z x; \<not> accP R z\<rbrakk> \<Longrightarrow> thesis"
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    77
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    78
  show thesis
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    79
  proof (cases "\<forall>z. R z x \<longrightarrow> accP R z")
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    80
    case True
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    81
    hence "\<And>z. R z x \<Longrightarrow> accP R z" by auto
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    82
    hence "accP R x"
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    83
      by (rule accPI)
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    84
    with na show thesis ..
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    85
  next
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    86
    case False then obtain z where "R z x" and "\<not>accP R z"
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    87
      by auto
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    88
    with a show thesis .
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    89
  qed
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    90
qed
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    91
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
    92
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    93
lemma accP_subset:
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    94
  assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    95
  shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    96
proof-
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    97
  fix x assume "accP R2 x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    98
  then show "accP R1 x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    99
  proof (induct x)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   100
    fix x
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   101
    assume ih: "\<And>y. R2 y x \<Longrightarrow> accP R1 y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   102
    with sub show "accP R1 x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   103
      by (blast intro:accPI)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   104
  qed
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   105
qed
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   106
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   107
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   108
lemma accP_subset_induct:
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   109
  assumes subset: "\<And>x. D x \<Longrightarrow> accP R x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   110
    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   111
    and "D x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   112
    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   113
  shows "P x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   114
proof -
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   115
  from subset and `D x` 
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   116
  have "accP R x" .
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   117
  then show "P x" using `D x`
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   118
  proof (induct x)
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   119
    fix x
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   120
    assume "D x"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   121
      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   122
    with dcl and istep show "P x" by blast
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   123
  qed
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   124
qed
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   125
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   126
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   127
section {* Definitions with default value *}
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   128
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   129
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
   130
  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
   131
  "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
   132
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   133
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   134
  by (simp add:theI' THE_default_def)
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   135
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   136
lemma THE_default1_equality: 
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   137
  "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   138
  by (simp add:the1_equality THE_default_def)
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   139
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   140
lemma THE_default_none:
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   141
  "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   142
by (simp add:THE_default_def)
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   143
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   144
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   145
lemma fundef_ex1_existence:
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   146
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   147
assumes ex1: "\<exists>!y. G x y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   148
shows "G x (f x)"
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   149
  by (simp only:f_def, rule THE_defaultI', rule ex1)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   150
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   151
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   152
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   153
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   154
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   155
lemma fundef_ex1_uniqueness:
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   156
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   157
assumes ex1: "\<exists>!y. G x y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   158
assumes elm: "G x (h x)"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   159
shows "h x = f x"
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   160
  by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   161
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   162
lemma fundef_ex1_iff:
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   163
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   164
assumes ex1: "\<exists>!y. G x y"
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   165
shows "(G x y) = (f x = y)"
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   166
  apply (auto simp:ex1 f_def THE_default1_equality)
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
   167
  by (rule THE_defaultI', rule ex1)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   168
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   169
lemma fundef_default_value:
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   170
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
21512
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
   171
assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
   172
assumes "\<not> D x"
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   173
shows "f x = d x"
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   174
proof -
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   175
  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
   176
  proof
21512
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
   177
    assume "\<exists>y. G x y"
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
   178
    hence "D x" using graph ..
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
   179
    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
   180
  qed
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   181
  hence "\<not>(\<exists>!y. G x y)" by blast
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   182
  
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   183
  thus ?thesis
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   184
    unfolding f_def
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   185
    by (rule THE_default_none)
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   186
qed
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   187
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   188
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
   189
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
   190
section {* Projections *}
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   191
consts
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   192
  lpg::"(('a + 'b) * 'a) set"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   193
  rpg::"(('a + 'b) * 'b) set"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   194
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   195
inductive lpg
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   196
intros
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   197
  "(Inl x, x) : lpg"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   198
inductive rpg
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   199
intros
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   200
  "(Inr y, y) : rpg"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
   201
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
   202
definition "lproj x = (THE y. (x,y) : lpg)"
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
   203
definition "rproj x = (THE y. (x,y) : rpg)"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   204
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   205
lemma lproj_inl:
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   206
  "lproj (Inl x) = x"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   207
  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
   208
lemma rproj_inr:
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   209
  "rproj (Inr x) = x"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   210
  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
   211
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   212
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
   213
use "Tools/function_package/fundef_common.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   214
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
   215
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
   216
use "Tools/function_package/context_tree.ML"
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
   217
use "Tools/function_package/fundef_core.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   218
use "Tools/function_package/termination.ML"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   219
use "Tools/function_package/mutual.ML"
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19934
diff changeset
   220
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
   221
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
   222
use "Tools/function_package/fundef_package.ML"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   223
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   224
setup FundefPackage.setup
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   225
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   226
lemmas [fundef_cong] = 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   227
  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
   228
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   229
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   230
lemma split_cong[fundef_cong]:
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   231
  "\<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
   232
  \<Longrightarrow> split f p = split g q"
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   233
  by (auto simp:split_def)
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   234
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   235
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   236
end