author | paulson <lp15@cam.ac.uk> |
Mon, 30 May 2022 12:46:11 +0100 | |
changeset 75494 | eded3fe9e600 |
parent 72184 | 881bd98bddee |
child 75669 | 43f5dfb7fa35 |
permissions | -rw-r--r-- |
55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54407
diff
changeset
|
1 |
(* Title: HOL/Fun_Def.thy |
20324 | 2 |
Author: Alexander Krauss, TU Muenchen |
22816 | 3 |
*) |
20324 | 4 |
|
60758 | 5 |
section \<open>Function Definitions and Termination Proofs\<close> |
20324 | 6 |
|
55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54407
diff
changeset
|
7 |
theory Fun_Def |
63654 | 8 |
imports Basic_BNF_LFPs Partial_Function SAT |
9 |
keywords |
|
69913 | 10 |
"function" "termination" :: thy_goal_defn and |
11 |
"fun" "fun_cases" :: thy_defn |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
12 |
begin |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
13 |
|
60758 | 14 |
subsection \<open>Definitions with default value\<close> |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
15 |
|
63654 | 16 |
definition THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" |
17 |
where "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)" |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
18 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
19 |
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)" |
22816 | 20 |
by (simp add: theI' THE_default_def) |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
21 |
|
63654 | 22 |
lemma THE_default1_equality: "\<exists>!x. P x \<Longrightarrow> P a \<Longrightarrow> THE_default d P = a" |
22816 | 23 |
by (simp add: the1_equality THE_default_def) |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
24 |
|
63654 | 25 |
lemma THE_default_none: "\<not> (\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
26 |
by (simp add: THE_default_def) |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
27 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
28 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
29 |
lemma fundef_ex1_existence: |
63654 | 30 |
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
22816 | 31 |
assumes ex1: "\<exists>!y. G x y" |
32 |
shows "G x (f x)" |
|
33 |
apply (simp only: f_def) |
|
34 |
apply (rule THE_defaultI') |
|
35 |
apply (rule ex1) |
|
36 |
done |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
37 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
lemma fundef_ex1_uniqueness: |
63654 | 39 |
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
22816 | 40 |
assumes ex1: "\<exists>!y. G x y" |
41 |
assumes elm: "G x (h x)" |
|
42 |
shows "h x = f x" |
|
43 |
apply (simp only: f_def) |
|
44 |
apply (rule THE_default1_equality [symmetric]) |
|
45 |
apply (rule ex1) |
|
46 |
apply (rule elm) |
|
47 |
done |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
48 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
49 |
lemma fundef_ex1_iff: |
63654 | 50 |
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
22816 | 51 |
assumes ex1: "\<exists>!y. G x y" |
52 |
shows "(G x y) = (f x = y)" |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
53 |
apply (auto simp:ex1 f_def THE_default1_equality) |
22816 | 54 |
apply (rule THE_defaultI') |
55 |
apply (rule ex1) |
|
56 |
done |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
57 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
58 |
lemma fundef_default_value: |
63654 | 59 |
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
22816 | 60 |
assumes graph: "\<And>x y. G x y \<Longrightarrow> D x" |
61 |
assumes "\<not> D x" |
|
62 |
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
|
63 |
proof - |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
64 |
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
|
65 |
proof |
21512
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
66 |
assume "\<exists>y. G x y" |
63654 | 67 |
then have "D x" using graph .. |
60758 | 68 |
with \<open>\<not> D x\<close> show False .. |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
69 |
qed |
63654 | 70 |
then have "\<not>(\<exists>!y. G x y)" by blast |
71 |
then show ?thesis |
|
72 |
unfolding f_def by (rule THE_default_none) |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
73 |
qed |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
74 |
|
63654 | 75 |
definition in_rel_def[simp]: "in_rel R x y \<equiv> (x, y) \<in> R" |
23739
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
76 |
|
63654 | 77 |
lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)" |
23739
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
78 |
by (simp add: wfP_def) |
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
79 |
|
69605 | 80 |
ML_file \<open>Tools/Function/function_core.ML\<close> |
81 |
ML_file \<open>Tools/Function/mutual.ML\<close> |
|
82 |
ML_file \<open>Tools/Function/pattern_split.ML\<close> |
|
83 |
ML_file \<open>Tools/Function/relation.ML\<close> |
|
84 |
ML_file \<open>Tools/Function/function_elims.ML\<close> |
|
47701 | 85 |
|
60758 | 86 |
method_setup relation = \<open> |
47701 | 87 |
Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t)) |
60758 | 88 |
\<close> "prove termination using a user-specified wellfounded relation" |
47701 | 89 |
|
69605 | 90 |
ML_file \<open>Tools/Function/function.ML\<close> |
91 |
ML_file \<open>Tools/Function/pat_completeness.ML\<close> |
|
47432 | 92 |
|
60758 | 93 |
method_setup pat_completeness = \<open> |
47432 | 94 |
Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) |
60758 | 95 |
\<close> "prove completeness of (co)datatype patterns" |
47432 | 96 |
|
69605 | 97 |
ML_file \<open>Tools/Function/fun.ML\<close> |
98 |
ML_file \<open>Tools/Function/induction_schema.ML\<close> |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
99 |
|
60758 | 100 |
method_setup induction_schema = \<open> |
70520 | 101 |
Scan.succeed (CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) |
60758 | 102 |
\<close> "prove an induction principle" |
47432 | 103 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
104 |
|
60758 | 105 |
subsection \<open>Measure functions\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
106 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
107 |
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool" |
63654 | 108 |
where is_measure_trivial: "is_measure f" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
109 |
|
57959 | 110 |
named_theorems measure_function "rules that guide the heuristic generation of measure functions" |
69605 | 111 |
ML_file \<open>Tools/Function/measure_functions.ML\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
112 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
113 |
lemma measure_size[measure_function]: "is_measure size" |
63654 | 114 |
by (rule is_measure_trivial) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
115 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
116 |
lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))" |
63654 | 117 |
by (rule is_measure_trivial) |
118 |
||
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
119 |
lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))" |
63654 | 120 |
by (rule is_measure_trivial) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
121 |
|
69605 | 122 |
ML_file \<open>Tools/Function/lexicographic_order.ML\<close> |
47432 | 123 |
|
60758 | 124 |
method_setup lexicographic_order = \<open> |
47432 | 125 |
Method.sections clasimp_modifiers >> |
126 |
(K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false)) |
|
60758 | 127 |
\<close> "termination prover for lexicographic orderings" |
47432 | 128 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
129 |
|
60758 | 130 |
subsection \<open>Congruence rules\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
131 |
|
63654 | 132 |
lemma let_cong [fundef_cong]: "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g" |
22816 | 133 |
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
|
134 |
|
22816 | 135 |
lemmas [fundef_cong] = |
67487
b4e65cd6974a
drop redundant fundef_cong rule
Lars Hupel <lars.hupel@mytum.de>
parents:
67443
diff
changeset
|
136 |
if_cong image_cong |
55466 | 137 |
bex_cong ball_cong imp_cong map_option_cong Option.bind_cong |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
138 |
|
22816 | 139 |
lemma split_cong [fundef_cong]: |
63654 | 140 |
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q \<Longrightarrow> case_prod f p = case_prod g q" |
22816 | 141 |
by (auto simp: split_def) |
19934 | 142 |
|
63654 | 143 |
lemma comp_cong [fundef_cong]: "f (g x) = f' (g' x') \<Longrightarrow> (f \<circ> g) x = (f' \<circ> g') x'" |
144 |
by (simp only: o_apply) |
|
19934 | 145 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
146 |
|
60758 | 147 |
subsection \<open>Simp rules for termination proofs\<close> |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
148 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
149 |
declare |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
150 |
trans_less_add1[termination_simp] |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
151 |
trans_less_add2[termination_simp] |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
152 |
trans_le_add1[termination_simp] |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
153 |
trans_le_add2[termination_simp] |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
154 |
less_imp_le_nat[termination_simp] |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
155 |
le_imp_less_Suc[termination_simp] |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
156 |
|
63654 | 157 |
lemma size_prod_simp[termination_simp]: "size_prod f g p = f (fst p) + g (snd p) + Suc 0" |
158 |
by (induct p) auto |
|
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
159 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
160 |
|
60758 | 161 |
subsection \<open>Decomposition\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
162 |
|
63654 | 163 |
lemma less_by_empty: "A = {} \<Longrightarrow> A \<subseteq> B" |
164 |
and union_comp_emptyL: "A O C = {} \<Longrightarrow> B O C = {} \<Longrightarrow> (A \<union> B) O C = {}" |
|
165 |
and union_comp_emptyR: "A O B = {} \<Longrightarrow> A O C = {} \<Longrightarrow> A O (B \<union> C) = {}" |
|
166 |
and wf_no_loop: "R O R = {} \<Longrightarrow> wf R" |
|
167 |
by (auto simp add: wf_comp_self [of R]) |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
168 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
169 |
|
60758 | 170 |
subsection \<open>Reduction pairs\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
171 |
|
63654 | 172 |
definition "reduction_pair P \<longleftrightarrow> wf (fst P) \<and> fst P O snd P \<subseteq> fst P" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
173 |
|
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
174 |
lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)" |
63654 | 175 |
by (auto simp: reduction_pair_def) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
176 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
177 |
lemma reduction_pair_lemma: |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
178 |
assumes rp: "reduction_pair P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
179 |
assumes "R \<subseteq> fst P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
180 |
assumes "S \<subseteq> snd P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
181 |
assumes "wf S" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
182 |
shows "wf (R \<union> S)" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
183 |
proof - |
60758 | 184 |
from rp \<open>S \<subseteq> snd P\<close> have "wf (fst P)" "fst P O S \<subseteq> fst P" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
185 |
unfolding reduction_pair_def by auto |
60758 | 186 |
with \<open>wf S\<close> have "wf (fst P \<union> S)" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
187 |
by (auto intro: wf_union_compatible) |
60758 | 188 |
moreover from \<open>R \<subseteq> fst P\<close> have "R \<union> S \<subseteq> fst P \<union> S" by auto |
47701 | 189 |
ultimately show ?thesis by (rule wf_subset) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
190 |
qed |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
191 |
|
63654 | 192 |
definition "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
193 |
|
63654 | 194 |
lemma rp_inv_image_rp: "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)" |
195 |
unfolding reduction_pair_def rp_inv_image_def split_def by force |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
196 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
197 |
|
60758 | 198 |
subsection \<open>Concrete orders for SCNP termination proofs\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
199 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
200 |
definition "pair_less = less_than <*lex*> less_than" |
67613 | 201 |
definition "pair_leq = pair_less\<^sup>=" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
202 |
definition "max_strict = max_ext pair_less" |
37767 | 203 |
definition "max_weak = max_ext pair_leq \<union> {({}, {})}" |
204 |
definition "min_strict = min_ext pair_less" |
|
205 |
definition "min_weak = min_ext pair_leq \<union> {({}, {})}" |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
206 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
207 |
lemma wf_pair_less[simp]: "wf pair_less" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
208 |
by (auto simp: pair_less_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
209 |
|
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70520
diff
changeset
|
210 |
lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less" |
72184 | 211 |
by (auto simp: total_on_def pair_less_def) |
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70520
diff
changeset
|
212 |
|
61799 | 213 |
text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
214 |
lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
215 |
and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
216 |
and pair_lessI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
217 |
and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less" |
63654 | 218 |
by (auto simp: pair_leq_def pair_less_def) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
219 |
|
72097 | 220 |
lemma pair_less_iff1 [simp]: "((x,y), (x,z)) \<in> pair_less \<longleftrightarrow> y<z" |
221 |
by (simp add: pair_less_def) |
|
222 |
||
60758 | 223 |
text \<open>Introduction rules for max\<close> |
63654 | 224 |
lemma smax_emptyI: "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" |
47701 | 225 |
and smax_insertI: |
63654 | 226 |
"y \<in> Y \<Longrightarrow> (x, y) \<in> pair_less \<Longrightarrow> (X, Y) \<in> max_strict \<Longrightarrow> (insert x X, Y) \<in> max_strict" |
227 |
and wmax_emptyI: "finite X \<Longrightarrow> ({}, X) \<in> max_weak" |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
228 |
and wmax_insertI: |
63654 | 229 |
"y \<in> YS \<Longrightarrow> (x, y) \<in> pair_leq \<Longrightarrow> (XS, YS) \<in> max_weak \<Longrightarrow> (insert x XS, YS) \<in> max_weak" |
230 |
by (auto simp: max_strict_def max_weak_def elim!: max_ext.cases) |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
231 |
|
60758 | 232 |
text \<open>Introduction rules for min\<close> |
63654 | 233 |
lemma smin_emptyI: "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" |
47701 | 234 |
and smin_insertI: |
63654 | 235 |
"x \<in> XS \<Longrightarrow> (x, y) \<in> pair_less \<Longrightarrow> (XS, YS) \<in> min_strict \<Longrightarrow> (XS, insert y YS) \<in> min_strict" |
236 |
and wmin_emptyI: "(X, {}) \<in> min_weak" |
|
47701 | 237 |
and wmin_insertI: |
63654 | 238 |
"x \<in> XS \<Longrightarrow> (x, y) \<in> pair_leq \<Longrightarrow> (XS, YS) \<in> min_weak \<Longrightarrow> (XS, insert y YS) \<in> min_weak" |
239 |
by (auto simp: min_strict_def min_weak_def min_ext_def) |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
240 |
|
63654 | 241 |
text \<open>Reduction Pairs.\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
242 |
|
47701 | 243 |
lemma max_ext_compat: |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
244 |
assumes "R O S \<subseteq> R" |
63654 | 245 |
shows "max_ext R O (max_ext S \<union> {({}, {})}) \<subseteq> max_ext R" |
246 |
using assms |
|
247 |
apply auto |
|
248 |
apply (elim max_ext.cases) |
|
249 |
apply rule |
|
250 |
apply auto[3] |
|
251 |
apply (drule_tac x=xa in meta_spec) |
|
252 |
apply simp |
|
253 |
apply (erule bexE) |
|
254 |
apply (drule_tac x=xb in meta_spec) |
|
255 |
apply auto |
|
256 |
done |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
257 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
258 |
lemma max_rpair_set: "reduction_pair (max_strict, max_weak)" |
47701 | 259 |
unfolding max_strict_def max_weak_def |
63654 | 260 |
apply (intro reduction_pairI max_ext_wf) |
261 |
apply simp |
|
262 |
apply (rule max_ext_compat) |
|
263 |
apply (auto simp: pair_less_def pair_leq_def) |
|
264 |
done |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
265 |
|
47701 | 266 |
lemma min_ext_compat: |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
267 |
assumes "R O S \<subseteq> R" |
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
268 |
shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R" |
63654 | 269 |
using assms |
270 |
apply (auto simp: min_ext_def) |
|
271 |
apply (drule_tac x=ya in bspec, assumption) |
|
272 |
apply (erule bexE) |
|
273 |
apply (drule_tac x=xc in bspec) |
|
274 |
apply assumption |
|
275 |
apply auto |
|
276 |
done |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
277 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
278 |
lemma min_rpair_set: "reduction_pair (min_strict, min_weak)" |
47701 | 279 |
unfolding min_strict_def min_weak_def |
63654 | 280 |
apply (intro reduction_pairI min_ext_wf) |
281 |
apply simp |
|
282 |
apply (rule min_ext_compat) |
|
283 |
apply (auto simp: pair_less_def pair_leq_def) |
|
284 |
done |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
285 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
286 |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
287 |
subsection \<open>Yet another induction principle on the natural numbers\<close> |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
288 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
289 |
lemma nat_descend_induct [case_names base descend]: |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
290 |
fixes P :: "nat \<Rightarrow> bool" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
291 |
assumes H1: "\<And>k. k > n \<Longrightarrow> P k" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
292 |
assumes H2: "\<And>k. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
293 |
shows "P m" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
294 |
using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+ |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
295 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
63654
diff
changeset
|
296 |
|
60758 | 297 |
subsection \<open>Tool setup\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
298 |
|
69605 | 299 |
ML_file \<open>Tools/Function/termination.ML\<close> |
300 |
ML_file \<open>Tools/Function/scnp_solve.ML\<close> |
|
301 |
ML_file \<open>Tools/Function/scnp_reconstruct.ML\<close> |
|
302 |
ML_file \<open>Tools/Function/fun_cases.ML\<close> |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
303 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64591
diff
changeset
|
304 |
ML_val \<comment> \<open>setup inactive\<close> |
60758 | 305 |
\<open> |
36521 | 306 |
Context.theory_map (Function_Common.set_termination_prover |
60682
5a6cd2560549
have the installed termination prover take a 'quiet' flag
blanchet
parents:
59953
diff
changeset
|
307 |
(K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))) |
60758 | 308 |
\<close> |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
309 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
310 |
end |