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