src/HOL/FunDef.thy
author krauss
Thu, 19 Jun 2008 11:46:14 +0200
changeset 27271 ba2a00d35df1
parent 26875 e18574413bc4
child 29125 d41182a8135c
permissions -rw-r--r--
generalized induct_scheme method to prove conditional induction schemes.
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
26748
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
     9
imports Wellfounded
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    10
uses
23203
a5026e73cfcf "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents: 22919
diff changeset
    11
  ("Tools/function_package/fundef_lib.ML")
22816
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/inductive_wrap.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    14
  ("Tools/function_package/context_tree.ML")
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    15
  ("Tools/function_package/fundef_core.ML")
25556
8d3b7c27049b load sum_tree.ML
krauss
parents: 24699
diff changeset
    16
  ("Tools/function_package/sum_tree.ML")
22816
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")
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
    21
  ("Tools/function_package/measure_functions.ML")
26748
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
    22
  ("Tools/function_package/lexicographic_order.ML")
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
    23
  ("Tools/function_package/fundef_datatype.ML")
27271
ba2a00d35df1 generalized induct_scheme method to prove conditional induction schemes.
krauss
parents: 26875
diff changeset
    24
  ("Tools/function_package/induction_scheme.ML")
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    25
begin
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    26
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    27
text {* Definitions with default value. *}
20536
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
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21364
diff changeset
    30
  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
    31
  "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
    32
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    33
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    34
  by (simp add: theI' THE_default_def)
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    35
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    36
lemma THE_default1_equality:
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    37
    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    38
  by (simp add: the1_equality 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
lemma THE_default_none:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    41
    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    42
  by (simp add:THE_default_def)
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    43
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    44
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    45
lemma fundef_ex1_existence:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    46
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    47
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    48
  shows "G x (f x)"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    49
  apply (simp only: f_def)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    50
  apply (rule THE_defaultI')
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    51
  apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    52
  done
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    53
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    54
lemma fundef_ex1_uniqueness:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    55
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    56
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    57
  assumes elm: "G x (h x)"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    58
  shows "h x = f x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    59
  apply (simp only: f_def)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    60
  apply (rule THE_default1_equality [symmetric])
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    61
   apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    62
  apply (rule elm)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    63
  done
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    64
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    65
lemma fundef_ex1_iff:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    66
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    67
  assumes ex1: "\<exists>!y. G x y"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    68
  shows "(G x y) = (f x = y)"
20536
f088edff8af8 Function package: Outside their domain functions now return "arbitrary".
krauss
parents: 20523
diff changeset
    69
  apply (auto simp:ex1 f_def THE_default1_equality)
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    70
  apply (rule THE_defaultI')
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    71
  apply (rule ex1)
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    72
  done
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    73
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    74
lemma fundef_default_value:
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    75
  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    76
  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    77
  assumes "\<not> D x"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    78
  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
    79
proof -
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    80
  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
    81
  proof
21512
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    82
    assume "\<exists>y. G x y"
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    83
    hence "D x" using graph ..
3786eb1b69d6 Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents: 21404
diff changeset
    84
    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
    85
  qed
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20654
diff changeset
    86
  hence "\<not>(\<exists>!y. G x y)" by blast
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
    87
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    88
  thus ?thesis
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    89
    unfolding f_def
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    90
    by (rule THE_default_none)
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    91
qed
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20536
diff changeset
    92
23739
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    93
definition in_rel_def[simp]:
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    94
  "in_rel R x y == (x, y) \<in> R"
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    95
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    96
lemma wf_in_rel:
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    97
  "wf R \<Longrightarrow> wfP (in_rel R)"
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    98
  by (simp add: wfP_def)
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
    99
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   100
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   101
where is_measure_trivial: "is_measure f"
23739
c5ead5df7f35 Inserted definition of in_rel again (since member2 was removed).
berghofe
parents: 23494
diff changeset
   102
23203
a5026e73cfcf "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents: 22919
diff changeset
   103
use "Tools/function_package/fundef_lib.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   104
use "Tools/function_package/fundef_common.ML"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20324
diff changeset
   105
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
   106
use "Tools/function_package/context_tree.ML"
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21512
diff changeset
   107
use "Tools/function_package/fundef_core.ML"
25556
8d3b7c27049b load sum_tree.ML
krauss
parents: 24699
diff changeset
   108
use "Tools/function_package/sum_tree.ML"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   109
use "Tools/function_package/mutual.ML"
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19934
diff changeset
   110
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
   111
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
   112
use "Tools/function_package/fundef_package.ML"
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   113
use "Tools/function_package/measure_functions.ML"
26748
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
   114
use "Tools/function_package/lexicographic_order.ML"
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
   115
use "Tools/function_package/fundef_datatype.ML"
27271
ba2a00d35df1 generalized induct_scheme method to prove conditional induction schemes.
krauss
parents: 26875
diff changeset
   116
use "Tools/function_package/induction_scheme.ML"
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   117
25567
5720345ea689 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents: 25556
diff changeset
   118
setup {* 
5720345ea689 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents: 25556
diff changeset
   119
  FundefPackage.setup 
5720345ea689 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents: 25556
diff changeset
   120
  #> InductionScheme.setup
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   121
  #> MeasureFunctions.setup
26748
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
   122
  #> LexicographicOrder.setup 
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 25567
diff changeset
   123
  #> FundefDatatype.setup
25567
5720345ea689 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents: 25556
diff changeset
   124
*}
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19564
diff changeset
   125
22838
haftmann
parents: 22816
diff changeset
   126
lemma let_cong [fundef_cong]:
haftmann
parents: 22816
diff changeset
   127
  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   128
  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
   129
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   130
lemmas [fundef_cong] =
22838
haftmann
parents: 22816
diff changeset
   131
  if_cong image_cong INT_cong UN_cong
haftmann
parents: 22816
diff changeset
   132
  bex_cong ball_cong imp_cong
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   133
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   134
lemma split_cong [fundef_cong]:
22838
haftmann
parents: 22816
diff changeset
   135
  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   136
    \<Longrightarrow> split f p = split g q"
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   137
  by (auto simp: split_def)
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   138
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   139
lemma comp_cong [fundef_cong]:
22838
haftmann
parents: 22816
diff changeset
   140
  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
22816
0eba117368d9 added header;
wenzelm
parents: 22622
diff changeset
   141
  unfolding o_apply .
19934
8190655ea2d4 Added split_cong rule
krauss
parents: 19770
diff changeset
   142
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   143
subsection {* Setup for termination proofs *}
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   144
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   145
text {* Rules for generating measure functions *}
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   146
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   147
lemma [measure_function]: "is_measure size"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   148
by (rule is_measure_trivial)
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   149
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   150
lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   151
by (rule is_measure_trivial)
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   152
lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   153
by (rule is_measure_trivial)
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   154
26749
397a1aeede7d * New attribute "termination_simp": Simp rules for termination proofs
krauss
parents: 26748
diff changeset
   155
lemma termination_basic_simps[termination_simp]:
397a1aeede7d * New attribute "termination_simp": Simp rules for termination proofs
krauss
parents: 26748
diff changeset
   156
  "x < (y::nat) \<Longrightarrow> x < y + z" 
397a1aeede7d * New attribute "termination_simp": Simp rules for termination proofs
krauss
parents: 26748
diff changeset
   157
  "x < z \<Longrightarrow> x < y + z"
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   158
  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   159
  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   160
  "x < y \<Longrightarrow> x \<le> (y::nat)"
26749
397a1aeede7d * New attribute "termination_simp": Simp rules for termination proofs
krauss
parents: 26748
diff changeset
   161
by arith+
397a1aeede7d * New attribute "termination_simp": Simp rules for termination proofs
krauss
parents: 26748
diff changeset
   162
26875
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   163
declare le_imp_less_Suc[termination_simp]
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   164
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   165
lemma prod_size_simp[termination_simp]:
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   166
  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   167
by (induct p) auto
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   168
e18574413bc4 Measure functions can now be declared via special rules, allowing for a
krauss
parents: 26749
diff changeset
   169
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   170
end