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