author | wenzelm |
Fri, 15 Jul 2016 15:19:04 +0200 | |
changeset 63505 | 42e1dece537a |
parent 63432 | ba7901e94e7b |
child 63654 | f90e3926e627 |
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 |
59141 | 8 |
imports Basic_BNF_LFPs Partial_Function SAT |
63432 | 9 |
keywords |
10 |
"function" "termination" :: thy_goal and |
|
11 |
"fun" "fun_cases" :: thy_decl |
|
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 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
16 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21364
diff
changeset
|
17 |
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
|
18 |
"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
|
19 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
20 |
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)" |
22816 | 21 |
by (simp add: theI' THE_default_def) |
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
22 |
|
22816 | 23 |
lemma THE_default1_equality: |
24 |
"\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a" |
|
25 |
by (simp add: the1_equality THE_default_def) |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
26 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
27 |
lemma THE_default_none: |
22816 | 28 |
"\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" |
29 |
by (simp add:THE_default_def) |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
30 |
|
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
31 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
32 |
lemma fundef_ex1_existence: |
22816 | 33 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
34 |
assumes ex1: "\<exists>!y. G x y" |
|
35 |
shows "G x (f x)" |
|
36 |
apply (simp only: f_def) |
|
37 |
apply (rule THE_defaultI') |
|
38 |
apply (rule ex1) |
|
39 |
done |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
40 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
41 |
lemma fundef_ex1_uniqueness: |
22816 | 42 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
43 |
assumes ex1: "\<exists>!y. G x y" |
|
44 |
assumes elm: "G x (h x)" |
|
45 |
shows "h x = f x" |
|
46 |
apply (simp only: f_def) |
|
47 |
apply (rule THE_default1_equality [symmetric]) |
|
48 |
apply (rule ex1) |
|
49 |
apply (rule elm) |
|
50 |
done |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
51 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
52 |
lemma fundef_ex1_iff: |
22816 | 53 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
54 |
assumes ex1: "\<exists>!y. G x y" |
|
55 |
shows "(G x y) = (f x = y)" |
|
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset
|
56 |
apply (auto simp:ex1 f_def THE_default1_equality) |
22816 | 57 |
apply (rule THE_defaultI') |
58 |
apply (rule ex1) |
|
59 |
done |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
60 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
61 |
lemma fundef_default_value: |
22816 | 62 |
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" |
63 |
assumes graph: "\<And>x y. G x y \<Longrightarrow> D x" |
|
64 |
assumes "\<not> D x" |
|
65 |
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
|
66 |
proof - |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
67 |
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
|
68 |
proof |
21512
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
69 |
assume "\<exists>y. G x y" |
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset
|
70 |
hence "D x" using graph .. |
60758 | 71 |
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
|
72 |
qed |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset
|
73 |
hence "\<not>(\<exists>!y. G x y)" by blast |
22816 | 74 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
75 |
thus ?thesis |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
76 |
unfolding f_def |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
77 |
by (rule THE_default_none) |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
78 |
qed |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
79 |
|
23739
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
80 |
definition in_rel_def[simp]: |
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
81 |
"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
|
82 |
|
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
83 |
lemma wf_in_rel: |
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
84 |
"wf R \<Longrightarrow> wfP (in_rel R)" |
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
85 |
by (simp add: wfP_def) |
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset
|
86 |
|
48891 | 87 |
ML_file "Tools/Function/function_core.ML" |
88 |
ML_file "Tools/Function/mutual.ML" |
|
89 |
ML_file "Tools/Function/pattern_split.ML" |
|
90 |
ML_file "Tools/Function/relation.ML" |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
49989
diff
changeset
|
91 |
ML_file "Tools/Function/function_elims.ML" |
47701 | 92 |
|
60758 | 93 |
method_setup relation = \<open> |
47701 | 94 |
Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t)) |
60758 | 95 |
\<close> "prove termination using a user-specified wellfounded relation" |
47701 | 96 |
|
48891 | 97 |
ML_file "Tools/Function/function.ML" |
98 |
ML_file "Tools/Function/pat_completeness.ML" |
|
47432 | 99 |
|
60758 | 100 |
method_setup pat_completeness = \<open> |
47432 | 101 |
Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) |
60758 | 102 |
\<close> "prove completeness of (co)datatype patterns" |
47432 | 103 |
|
48891 | 104 |
ML_file "Tools/Function/fun.ML" |
105 |
ML_file "Tools/Function/induction_schema.ML" |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
106 |
|
60758 | 107 |
method_setup induction_schema = \<open> |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61799
diff
changeset
|
108 |
Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) |
60758 | 109 |
\<close> "prove an induction principle" |
47432 | 110 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
111 |
|
60758 | 112 |
subsection \<open>Measure functions\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
113 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
114 |
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
115 |
where is_measure_trivial: "is_measure f" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
116 |
|
57959 | 117 |
named_theorems measure_function "rules that guide the heuristic generation of measure functions" |
48891 | 118 |
ML_file "Tools/Function/measure_functions.ML" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
119 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
120 |
lemma measure_size[measure_function]: "is_measure size" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
121 |
by (rule is_measure_trivial) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
122 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
123 |
lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
124 |
by (rule is_measure_trivial) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
125 |
lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
126 |
by (rule is_measure_trivial) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
127 |
|
48891 | 128 |
ML_file "Tools/Function/lexicographic_order.ML" |
47432 | 129 |
|
60758 | 130 |
method_setup lexicographic_order = \<open> |
47432 | 131 |
Method.sections clasimp_modifiers >> |
132 |
(K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false)) |
|
60758 | 133 |
\<close> "termination prover for lexicographic orderings" |
47432 | 134 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
135 |
|
60758 | 136 |
subsection \<open>Congruence rules\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
137 |
|
22838 | 138 |
lemma let_cong [fundef_cong]: |
139 |
"M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g" |
|
22816 | 140 |
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
|
141 |
|
22816 | 142 |
lemmas [fundef_cong] = |
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
55968
diff
changeset
|
143 |
if_cong image_cong INF_cong SUP_cong |
55466 | 144 |
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
|
145 |
|
22816 | 146 |
lemma split_cong [fundef_cong]: |
22838 | 147 |
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60758
diff
changeset
|
148 |
\<Longrightarrow> case_prod f p = case_prod g q" |
22816 | 149 |
by (auto simp: split_def) |
19934 | 150 |
|
22816 | 151 |
lemma comp_cong [fundef_cong]: |
22838 | 152 |
"f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'" |
22816 | 153 |
unfolding o_apply . |
19934 | 154 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
155 |
|
60758 | 156 |
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
|
157 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
158 |
declare |
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
159 |
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
|
160 |
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
|
161 |
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
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
|
56846
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56643
diff
changeset
|
166 |
lemma size_prod_simp[termination_simp]: |
9df717fef2bb
renamed 'xxx_size' to 'size_xxx' for old datatype package
blanchet
parents:
56643
diff
changeset
|
167 |
"size_prod f g p = f (fst p) + g (snd p) + Suc 0" |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
168 |
by (induct p) auto |
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
169 |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56248
diff
changeset
|
170 |
|
60758 | 171 |
subsection \<open>Decomposition\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
172 |
|
47701 | 173 |
lemma less_by_empty: |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
174 |
"A = {} \<Longrightarrow> A \<subseteq> B" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
175 |
and union_comp_emptyL: |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
176 |
"\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
177 |
and union_comp_emptyR: |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
178 |
"\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}" |
47701 | 179 |
and wf_no_loop: |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
180 |
"R O R = {} \<Longrightarrow> wf R" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
181 |
by (auto simp add: wf_comp_self[of R]) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
182 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
183 |
|
60758 | 184 |
subsection \<open>Reduction pairs\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
185 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
186 |
definition |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
187 |
"reduction_pair P = (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
|
188 |
|
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
189 |
lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
190 |
unfolding reduction_pair_def by auto |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
191 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
192 |
lemma reduction_pair_lemma: |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
193 |
assumes rp: "reduction_pair P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
194 |
assumes "R \<subseteq> fst P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
195 |
assumes "S \<subseteq> snd P" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
196 |
assumes "wf S" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
197 |
shows "wf (R \<union> S)" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
198 |
proof - |
60758 | 199 |
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
|
200 |
unfolding reduction_pair_def by auto |
60758 | 201 |
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
|
202 |
by (auto intro: wf_union_compatible) |
60758 | 203 |
moreover from \<open>R \<subseteq> fst P\<close> have "R \<union> S \<subseteq> fst P \<union> S" by auto |
47701 | 204 |
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
|
205 |
qed |
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 |
definition |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
208 |
"rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
209 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
210 |
lemma rp_inv_image_rp: |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
211 |
"reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
212 |
unfolding reduction_pair_def rp_inv_image_def split_def |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
213 |
by force |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
214 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
215 |
|
60758 | 216 |
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
|
217 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
218 |
definition "pair_less = less_than <*lex*> less_than" |
37767 | 219 |
definition "pair_leq = pair_less^=" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
220 |
definition "max_strict = max_ext pair_less" |
37767 | 221 |
definition "max_weak = max_ext pair_leq \<union> {({}, {})}" |
222 |
definition "min_strict = min_ext pair_less" |
|
223 |
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
|
224 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
225 |
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
|
226 |
by (auto simp: pair_less_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
227 |
|
61799 | 228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<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
|
233 |
unfolding pair_leq_def pair_less_def by auto |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
234 |
|
60758 | 235 |
text \<open>Introduction rules for max\<close> |
47701 | 236 |
lemma smax_emptyI: |
237 |
"finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" |
|
238 |
and smax_insertI: |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
239 |
"\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict" |
47701 | 240 |
and wmax_emptyI: |
241 |
"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
|
242 |
and wmax_insertI: |
47701 | 243 |
"\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
244 |
unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
245 |
|
60758 | 246 |
text \<open>Introduction rules for min\<close> |
47701 | 247 |
lemma smin_emptyI: |
248 |
"X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" |
|
249 |
and smin_insertI: |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
250 |
"\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict" |
47701 | 251 |
and wmin_emptyI: |
252 |
"(X, {}) \<in> min_weak" |
|
253 |
and wmin_insertI: |
|
254 |
"\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
255 |
by (auto simp: min_strict_def min_weak_def min_ext_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
256 |
|
60758 | 257 |
text \<open>Reduction Pairs\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
258 |
|
47701 | 259 |
lemma max_ext_compat: |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
260 |
assumes "R O S \<subseteq> R" |
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
261 |
shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R" |
47701 | 262 |
using assms |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
263 |
apply auto |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
264 |
apply (elim max_ext.cases) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
265 |
apply rule |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
266 |
apply auto[3] |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
267 |
apply (drule_tac x=xa in meta_spec) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
268 |
apply simp |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
269 |
apply (erule bexE) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
270 |
apply (drule_tac x=xb in meta_spec) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
271 |
by auto |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
272 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
273 |
lemma max_rpair_set: "reduction_pair (max_strict, max_weak)" |
47701 | 274 |
unfolding max_strict_def max_weak_def |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
275 |
apply (intro reduction_pairI max_ext_wf) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
276 |
apply simp |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
277 |
apply (rule max_ext_compat) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
278 |
by (auto simp: pair_less_def pair_leq_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
279 |
|
47701 | 280 |
lemma min_ext_compat: |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
281 |
assumes "R O S \<subseteq> R" |
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31775
diff
changeset
|
282 |
shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R" |
47701 | 283 |
using assms |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
284 |
apply (auto simp: min_ext_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
285 |
apply (drule_tac x=ya in bspec, assumption) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
286 |
apply (erule bexE) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
287 |
apply (drule_tac x=xc in bspec) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
288 |
apply assumption |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
289 |
by auto |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
290 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
291 |
lemma min_rpair_set: "reduction_pair (min_strict, min_weak)" |
47701 | 292 |
unfolding min_strict_def min_weak_def |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
293 |
apply (intro reduction_pairI min_ext_wf) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
294 |
apply simp |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
295 |
apply (rule min_ext_compat) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
296 |
by (auto simp: pair_less_def pair_leq_def) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
297 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
298 |
|
60758 | 299 |
subsection \<open>Tool setup\<close> |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
300 |
|
48891 | 301 |
ML_file "Tools/Function/termination.ML" |
302 |
ML_file "Tools/Function/scnp_solve.ML" |
|
303 |
ML_file "Tools/Function/scnp_reconstruct.ML" |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
49989
diff
changeset
|
304 |
ML_file "Tools/Function/fun_cases.ML" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset
|
305 |
|
61799 | 306 |
ML_val \<comment> "setup inactive" |
60758 | 307 |
\<open> |
36521 | 308 |
Context.theory_map (Function_Common.set_termination_prover |
60682
5a6cd2560549
have the installed termination prover take a 'quiet' flag
blanchet
parents:
59953
diff
changeset
|
309 |
(K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))) |
60758 | 310 |
\<close> |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
311 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
312 |
end |