src/HOL/Fun_Def.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 64591 240a39af9ec4 child 67443 3abf6a722518 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
 blanchet@55085 ` 1` ```(* Title: HOL/Fun_Def.thy ``` wenzelm@20324 ` 2` ``` Author: Alexander Krauss, TU Muenchen ``` wenzelm@22816 ` 3` ```*) ``` wenzelm@20324 ` 4` wenzelm@60758 ` 5` ```section \Function Definitions and Termination Proofs\ ``` wenzelm@20324 ` 6` blanchet@55085 ` 7` ```theory Fun_Def ``` wenzelm@63654 ` 8` ``` imports Basic_BNF_LFPs Partial_Function SAT ``` wenzelm@63654 ` 9` ``` keywords ``` wenzelm@63654 ` 10` ``` "function" "termination" :: thy_goal and ``` wenzelm@63654 ` 11` ``` "fun" "fun_cases" :: thy_decl ``` krauss@19564 ` 12` ```begin ``` krauss@19564 ` 13` wenzelm@60758 ` 14` ```subsection \Definitions with default value\ ``` krauss@20536 ` 15` wenzelm@63654 ` 16` ```definition THE_default :: "'a \ ('a \ bool) \ 'a" ``` wenzelm@63654 ` 17` ``` where "THE_default d P = (if (\!x. P x) then (THE x. P x) else d)" ``` krauss@20536 ` 18` krauss@20536 ` 19` ```lemma THE_defaultI': "\!x. P x \ P (THE_default d P)" ``` wenzelm@22816 ` 20` ``` by (simp add: theI' THE_default_def) ``` krauss@20536 ` 21` wenzelm@63654 ` 22` ```lemma THE_default1_equality: "\!x. P x \ P a \ THE_default d P = a" ``` wenzelm@22816 ` 23` ``` by (simp add: the1_equality THE_default_def) ``` krauss@20536 ` 24` wenzelm@63654 ` 25` ```lemma THE_default_none: "\ (\!x. P x) \ THE_default d P = d" ``` wenzelm@63654 ` 26` ``` by (simp add: THE_default_def) ``` krauss@20536 ` 27` krauss@20536 ` 28` krauss@19564 ` 29` ```lemma fundef_ex1_existence: ``` wenzelm@63654 ` 30` ``` assumes f_def: "f \ (\x::'a. THE_default (d x) (\y. G x y))" ``` wenzelm@22816 ` 31` ``` assumes ex1: "\!y. G x y" ``` wenzelm@22816 ` 32` ``` shows "G x (f x)" ``` wenzelm@22816 ` 33` ``` apply (simp only: f_def) ``` wenzelm@22816 ` 34` ``` apply (rule THE_defaultI') ``` wenzelm@22816 ` 35` ``` apply (rule ex1) ``` wenzelm@22816 ` 36` ``` done ``` krauss@21051 ` 37` krauss@19564 ` 38` ```lemma fundef_ex1_uniqueness: ``` wenzelm@63654 ` 39` ``` assumes f_def: "f \ (\x::'a. THE_default (d x) (\y. G x y))" ``` wenzelm@22816 ` 40` ``` assumes ex1: "\!y. G x y" ``` wenzelm@22816 ` 41` ``` assumes elm: "G x (h x)" ``` wenzelm@22816 ` 42` ``` shows "h x = f x" ``` wenzelm@22816 ` 43` ``` apply (simp only: f_def) ``` wenzelm@22816 ` 44` ``` apply (rule THE_default1_equality [symmetric]) ``` wenzelm@22816 ` 45` ``` apply (rule ex1) ``` wenzelm@22816 ` 46` ``` apply (rule elm) ``` wenzelm@22816 ` 47` ``` done ``` krauss@19564 ` 48` krauss@19564 ` 49` ```lemma fundef_ex1_iff: ``` wenzelm@63654 ` 50` ``` assumes f_def: "f \ (\x::'a. THE_default (d x) (\y. G x y))" ``` wenzelm@22816 ` 51` ``` assumes ex1: "\!y. G x y" ``` wenzelm@22816 ` 52` ``` shows "(G x y) = (f x = y)" ``` krauss@20536 ` 53` ``` apply (auto simp:ex1 f_def THE_default1_equality) ``` wenzelm@22816 ` 54` ``` apply (rule THE_defaultI') ``` wenzelm@22816 ` 55` ``` apply (rule ex1) ``` wenzelm@22816 ` 56` ``` done ``` krauss@19564 ` 57` krauss@20654 ` 58` ```lemma fundef_default_value: ``` wenzelm@63654 ` 59` ``` assumes f_def: "f \ (\x::'a. THE_default (d x) (\y. G x y))" ``` wenzelm@22816 ` 60` ``` assumes graph: "\x y. G x y \ D x" ``` wenzelm@22816 ` 61` ``` assumes "\ D x" ``` wenzelm@22816 ` 62` ``` shows "f x = d x" ``` krauss@20654 ` 63` ```proof - ``` krauss@21051 ` 64` ``` have "\(\y. G x y)" ``` krauss@20654 ` 65` ``` proof ``` krauss@21512 ` 66` ``` assume "\y. G x y" ``` wenzelm@63654 ` 67` ``` then have "D x" using graph .. ``` wenzelm@60758 ` 68` ``` with \\ D x\ show False .. ``` krauss@20654 ` 69` ``` qed ``` wenzelm@63654 ` 70` ``` then have "\(\!y. G x y)" by blast ``` wenzelm@63654 ` 71` ``` then show ?thesis ``` wenzelm@63654 ` 72` ``` unfolding f_def by (rule THE_default_none) ``` krauss@20654 ` 73` ```qed ``` krauss@20654 ` 74` wenzelm@63654 ` 75` ```definition in_rel_def[simp]: "in_rel R x y \ (x, y) \ R" ``` berghofe@23739 ` 76` wenzelm@63654 ` 77` ```lemma wf_in_rel: "wf R \ wfP (in_rel R)" ``` berghofe@23739 ` 78` ``` by (simp add: wfP_def) ``` berghofe@23739 ` 79` wenzelm@48891 ` 80` ```ML_file "Tools/Function/function_core.ML" ``` wenzelm@48891 ` 81` ```ML_file "Tools/Function/mutual.ML" ``` wenzelm@48891 ` 82` ```ML_file "Tools/Function/pattern_split.ML" ``` wenzelm@48891 ` 83` ```ML_file "Tools/Function/relation.ML" ``` Manuel@53603 ` 84` ```ML_file "Tools/Function/function_elims.ML" ``` wenzelm@47701 ` 85` wenzelm@60758 ` 86` ```method_setup relation = \ ``` wenzelm@47701 ` 87` ``` Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t)) ``` wenzelm@60758 ` 88` ```\ "prove termination using a user-specified wellfounded relation" ``` wenzelm@47701 ` 89` wenzelm@48891 ` 90` ```ML_file "Tools/Function/function.ML" ``` wenzelm@48891 ` 91` ```ML_file "Tools/Function/pat_completeness.ML" ``` wenzelm@47432 ` 92` wenzelm@60758 ` 93` ```method_setup pat_completeness = \ ``` wenzelm@47432 ` 94` ``` Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) ``` wenzelm@60758 ` 95` ```\ "prove completeness of (co)datatype patterns" ``` wenzelm@47432 ` 96` wenzelm@48891 ` 97` ```ML_file "Tools/Function/fun.ML" ``` wenzelm@48891 ` 98` ```ML_file "Tools/Function/induction_schema.ML" ``` krauss@19564 ` 99` wenzelm@60758 ` 100` ```method_setup induction_schema = \ ``` wenzelm@61841 ` 101` ``` Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) ``` wenzelm@60758 ` 102` ```\ "prove an induction principle" ``` wenzelm@47432 ` 103` blanchet@56643 ` 104` wenzelm@60758 ` 105` ```subsection \Measure functions\ ``` krauss@29125 ` 106` krauss@29125 ` 107` ```inductive is_measure :: "('a \ nat) \ bool" ``` wenzelm@63654 ` 108` ``` where is_measure_trivial: "is_measure f" ``` krauss@29125 ` 109` wenzelm@57959 ` 110` ```named_theorems measure_function "rules that guide the heuristic generation of measure functions" ``` wenzelm@48891 ` 111` ```ML_file "Tools/Function/measure_functions.ML" ``` krauss@29125 ` 112` krauss@29125 ` 113` ```lemma measure_size[measure_function]: "is_measure size" ``` wenzelm@63654 ` 114` ``` by (rule is_measure_trivial) ``` krauss@29125 ` 115` krauss@29125 ` 116` ```lemma measure_fst[measure_function]: "is_measure f \ is_measure (\p. f (fst p))" ``` wenzelm@63654 ` 117` ``` by (rule is_measure_trivial) ``` wenzelm@63654 ` 118` krauss@29125 ` 119` ```lemma measure_snd[measure_function]: "is_measure f \ is_measure (\p. f (snd p))" ``` wenzelm@63654 ` 120` ``` by (rule is_measure_trivial) ``` krauss@29125 ` 121` wenzelm@48891 ` 122` ```ML_file "Tools/Function/lexicographic_order.ML" ``` wenzelm@47432 ` 123` wenzelm@60758 ` 124` ```method_setup lexicographic_order = \ ``` wenzelm@47432 ` 125` ``` Method.sections clasimp_modifiers >> ``` wenzelm@47432 ` 126` ``` (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false)) ``` wenzelm@60758 ` 127` ```\ "termination prover for lexicographic orderings" ``` wenzelm@47432 ` 128` krauss@29125 ` 129` wenzelm@60758 ` 130` ```subsection \Congruence rules\ ``` krauss@29125 ` 131` wenzelm@63654 ` 132` ```lemma let_cong [fundef_cong]: "M = N \ (\x. x = N \ f x = g x) \ Let M f = Let N g" ``` wenzelm@22816 ` 133` ``` unfolding Let_def by blast ``` krauss@22622 ` 134` wenzelm@22816 ` 135` ```lemmas [fundef_cong] = ``` haftmann@56248 ` 136` ``` if_cong image_cong INF_cong SUP_cong ``` blanchet@55466 ` 137` ``` bex_cong ball_cong imp_cong map_option_cong Option.bind_cong ``` krauss@19564 ` 138` wenzelm@22816 ` 139` ```lemma split_cong [fundef_cong]: ``` wenzelm@63654 ` 140` ``` "(\x y. (x, y) = q \ f x y = g x y) \ p = q \ case_prod f p = case_prod g q" ``` wenzelm@22816 ` 141` ``` by (auto simp: split_def) ``` krauss@19934 ` 142` wenzelm@63654 ` 143` ```lemma comp_cong [fundef_cong]: "f (g x) = f' (g' x') \ (f \ g) x = (f' \ g') x'" ``` wenzelm@63654 ` 144` ``` by (simp only: o_apply) ``` krauss@19934 ` 145` blanchet@56643 ` 146` wenzelm@60758 ` 147` ```subsection \Simp rules for termination proofs\ ``` krauss@26875 ` 148` blanchet@56643 ` 149` ```declare ``` blanchet@56643 ` 150` ``` trans_less_add1[termination_simp] ``` blanchet@56643 ` 151` ``` trans_less_add2[termination_simp] ``` blanchet@56643 ` 152` ``` trans_le_add1[termination_simp] ``` blanchet@56643 ` 153` ``` trans_le_add2[termination_simp] ``` blanchet@56643 ` 154` ``` less_imp_le_nat[termination_simp] ``` blanchet@56643 ` 155` ``` le_imp_less_Suc[termination_simp] ``` krauss@26875 ` 156` wenzelm@63654 ` 157` ```lemma size_prod_simp[termination_simp]: "size_prod f g p = f (fst p) + g (snd p) + Suc 0" ``` wenzelm@63654 ` 158` ``` by (induct p) auto ``` krauss@26875 ` 159` blanchet@56643 ` 160` wenzelm@60758 ` 161` ```subsection \Decomposition\ ``` krauss@29125 ` 162` wenzelm@63654 ` 163` ```lemma less_by_empty: "A = {} \ A \ B" ``` wenzelm@63654 ` 164` ``` and union_comp_emptyL: "A O C = {} \ B O C = {} \ (A \ B) O C = {}" ``` wenzelm@63654 ` 165` ``` and union_comp_emptyR: "A O B = {} \ A O C = {} \ A O (B \ C) = {}" ``` wenzelm@63654 ` 166` ``` and wf_no_loop: "R O R = {} \ wf R" ``` wenzelm@63654 ` 167` ``` by (auto simp add: wf_comp_self [of R]) ``` krauss@29125 ` 168` krauss@29125 ` 169` wenzelm@60758 ` 170` ```subsection \Reduction pairs\ ``` krauss@29125 ` 171` wenzelm@63654 ` 172` ```definition "reduction_pair P \ wf (fst P) \ fst P O snd P \ fst P" ``` krauss@29125 ` 173` krauss@32235 ` 174` ```lemma reduction_pairI[intro]: "wf R \ R O S \ R \ reduction_pair (R, S)" ``` wenzelm@63654 ` 175` ``` by (auto simp: reduction_pair_def) ``` krauss@29125 ` 176` krauss@29125 ` 177` ```lemma reduction_pair_lemma: ``` krauss@29125 ` 178` ``` assumes rp: "reduction_pair P" ``` krauss@29125 ` 179` ``` assumes "R \ fst P" ``` krauss@29125 ` 180` ``` assumes "S \ snd P" ``` krauss@29125 ` 181` ``` assumes "wf S" ``` krauss@29125 ` 182` ``` shows "wf (R \ S)" ``` krauss@29125 ` 183` ```proof - ``` wenzelm@60758 ` 184` ``` from rp \S \ snd P\ have "wf (fst P)" "fst P O S \ fst P" ``` krauss@29125 ` 185` ``` unfolding reduction_pair_def by auto ``` wenzelm@60758 ` 186` ``` with \wf S\ have "wf (fst P \ S)" ``` krauss@29125 ` 187` ``` by (auto intro: wf_union_compatible) ``` wenzelm@60758 ` 188` ``` moreover from \R \ fst P\ have "R \ S \ fst P \ S" by auto ``` wenzelm@47701 ` 189` ``` ultimately show ?thesis by (rule wf_subset) ``` krauss@29125 ` 190` ```qed ``` krauss@29125 ` 191` wenzelm@63654 ` 192` ```definition "rp_inv_image = (\(R,S) f. (inv_image R f, inv_image S f))" ``` krauss@29125 ` 193` wenzelm@63654 ` 194` ```lemma rp_inv_image_rp: "reduction_pair P \ reduction_pair (rp_inv_image P f)" ``` wenzelm@63654 ` 195` ``` unfolding reduction_pair_def rp_inv_image_def split_def by force ``` krauss@29125 ` 196` krauss@29125 ` 197` wenzelm@60758 ` 198` ```subsection \Concrete orders for SCNP termination proofs\ ``` krauss@29125 ` 199` krauss@29125 ` 200` ```definition "pair_less = less_than <*lex*> less_than" ``` haftmann@37767 ` 201` ```definition "pair_leq = pair_less^=" ``` krauss@29125 ` 202` ```definition "max_strict = max_ext pair_less" ``` haftmann@37767 ` 203` ```definition "max_weak = max_ext pair_leq \ {({}, {})}" ``` haftmann@37767 ` 204` ```definition "min_strict = min_ext pair_less" ``` haftmann@37767 ` 205` ```definition "min_weak = min_ext pair_leq \ {({}, {})}" ``` krauss@29125 ` 206` krauss@29125 ` 207` ```lemma wf_pair_less[simp]: "wf pair_less" ``` krauss@29125 ` 208` ``` by (auto simp: pair_less_def) ``` krauss@29125 ` 209` wenzelm@61799 ` 210` ```text \Introduction rules for \pair_less\/\pair_leq\\ ``` krauss@29125 ` 211` ```lemma pair_leqI1: "a < b \ ((a, s), (b, t)) \ pair_leq" ``` krauss@29125 ` 212` ``` and pair_leqI2: "a \ b \ s \ t \ ((a, s), (b, t)) \ pair_leq" ``` krauss@29125 ` 213` ``` and pair_lessI1: "a < b \ ((a, s), (b, t)) \ pair_less" ``` krauss@29125 ` 214` ``` and pair_lessI2: "a \ b \ s < t \ ((a, s), (b, t)) \ pair_less" ``` wenzelm@63654 ` 215` ``` by (auto simp: pair_leq_def pair_less_def) ``` krauss@29125 ` 216` wenzelm@60758 ` 217` ```text \Introduction rules for max\ ``` wenzelm@63654 ` 218` ```lemma smax_emptyI: "finite Y \ Y \ {} \ ({}, Y) \ max_strict" ``` wenzelm@47701 ` 219` ``` and smax_insertI: ``` wenzelm@63654 ` 220` ``` "y \ Y \ (x, y) \ pair_less \ (X, Y) \ max_strict \ (insert x X, Y) \ max_strict" ``` wenzelm@63654 ` 221` ``` and wmax_emptyI: "finite X \ ({}, X) \ max_weak" ``` krauss@29125 ` 222` ``` and wmax_insertI: ``` wenzelm@63654 ` 223` ``` "y \ YS \ (x, y) \ pair_leq \ (XS, YS) \ max_weak \ (insert x XS, YS) \ max_weak" ``` wenzelm@63654 ` 224` ``` by (auto simp: max_strict_def max_weak_def elim!: max_ext.cases) ``` krauss@29125 ` 225` wenzelm@60758 ` 226` ```text \Introduction rules for min\ ``` wenzelm@63654 ` 227` ```lemma smin_emptyI: "X \ {} \ (X, {}) \ min_strict" ``` wenzelm@47701 ` 228` ``` and smin_insertI: ``` wenzelm@63654 ` 229` ``` "x \ XS \ (x, y) \ pair_less \ (XS, YS) \ min_strict \ (XS, insert y YS) \ min_strict" ``` wenzelm@63654 ` 230` ``` and wmin_emptyI: "(X, {}) \ min_weak" ``` wenzelm@47701 ` 231` ``` and wmin_insertI: ``` wenzelm@63654 ` 232` ``` "x \ XS \ (x, y) \ pair_leq \ (XS, YS) \ min_weak \ (XS, insert y YS) \ min_weak" ``` wenzelm@63654 ` 233` ``` by (auto simp: min_strict_def min_weak_def min_ext_def) ``` krauss@29125 ` 234` wenzelm@63654 ` 235` ```text \Reduction Pairs.\ ``` krauss@29125 ` 236` wenzelm@47701 ` 237` ```lemma max_ext_compat: ``` krauss@32235 ` 238` ``` assumes "R O S \ R" ``` wenzelm@63654 ` 239` ``` shows "max_ext R O (max_ext S \ {({}, {})}) \ max_ext R" ``` wenzelm@63654 ` 240` ``` using assms ``` wenzelm@63654 ` 241` ``` apply auto ``` wenzelm@63654 ` 242` ``` apply (elim max_ext.cases) ``` wenzelm@63654 ` 243` ``` apply rule ``` wenzelm@63654 ` 244` ``` apply auto[3] ``` wenzelm@63654 ` 245` ``` apply (drule_tac x=xa in meta_spec) ``` wenzelm@63654 ` 246` ``` apply simp ``` wenzelm@63654 ` 247` ``` apply (erule bexE) ``` wenzelm@63654 ` 248` ``` apply (drule_tac x=xb in meta_spec) ``` wenzelm@63654 ` 249` ``` apply auto ``` wenzelm@63654 ` 250` ``` done ``` krauss@29125 ` 251` krauss@29125 ` 252` ```lemma max_rpair_set: "reduction_pair (max_strict, max_weak)" ``` wenzelm@47701 ` 253` ``` unfolding max_strict_def max_weak_def ``` wenzelm@63654 ` 254` ``` apply (intro reduction_pairI max_ext_wf) ``` wenzelm@63654 ` 255` ``` apply simp ``` wenzelm@63654 ` 256` ``` apply (rule max_ext_compat) ``` wenzelm@63654 ` 257` ``` apply (auto simp: pair_less_def pair_leq_def) ``` wenzelm@63654 ` 258` ``` done ``` krauss@29125 ` 259` wenzelm@47701 ` 260` ```lemma min_ext_compat: ``` krauss@32235 ` 261` ``` assumes "R O S \ R" ``` krauss@32235 ` 262` ``` shows "min_ext R O (min_ext S \ {({},{})}) \ min_ext R" ``` wenzelm@63654 ` 263` ``` using assms ``` wenzelm@63654 ` 264` ``` apply (auto simp: min_ext_def) ``` wenzelm@63654 ` 265` ``` apply (drule_tac x=ya in bspec, assumption) ``` wenzelm@63654 ` 266` ``` apply (erule bexE) ``` wenzelm@63654 ` 267` ``` apply (drule_tac x=xc in bspec) ``` wenzelm@63654 ` 268` ``` apply assumption ``` wenzelm@63654 ` 269` ``` apply auto ``` wenzelm@63654 ` 270` ``` done ``` krauss@29125 ` 271` krauss@29125 ` 272` ```lemma min_rpair_set: "reduction_pair (min_strict, min_weak)" ``` wenzelm@47701 ` 273` ``` unfolding min_strict_def min_weak_def ``` wenzelm@63654 ` 274` ``` apply (intro reduction_pairI min_ext_wf) ``` wenzelm@63654 ` 275` ``` apply simp ``` wenzelm@63654 ` 276` ``` apply (rule min_ext_compat) ``` wenzelm@63654 ` 277` ``` apply (auto simp: pair_less_def pair_leq_def) ``` wenzelm@63654 ` 278` ``` done ``` krauss@29125 ` 279` krauss@29125 ` 280` haftmann@64591 ` 281` ```subsection \Yet another induction principle on the natural numbers\ ``` haftmann@64591 ` 282` haftmann@64591 ` 283` ```lemma nat_descend_induct [case_names base descend]: ``` haftmann@64591 ` 284` ``` fixes P :: "nat \ bool" ``` haftmann@64591 ` 285` ``` assumes H1: "\k. k > n \ P k" ``` haftmann@64591 ` 286` ``` assumes H2: "\k. k \ n \ (\i. i > k \ P i) \ P k" ``` haftmann@64591 ` 287` ``` shows "P m" ``` haftmann@64591 ` 288` ``` using assms by induction_schema (force intro!: wf_measure [of "\k. Suc n - k"])+ ``` haftmann@64591 ` 289` haftmann@64591 ` 290` wenzelm@60758 ` 291` ```subsection \Tool setup\ ``` krauss@29125 ` 292` wenzelm@48891 ` 293` ```ML_file "Tools/Function/termination.ML" ``` wenzelm@48891 ` 294` ```ML_file "Tools/Function/scnp_solve.ML" ``` wenzelm@48891 ` 295` ```ML_file "Tools/Function/scnp_reconstruct.ML" ``` Manuel@53603 ` 296` ```ML_file "Tools/Function/fun_cases.ML" ``` krauss@29125 ` 297` wenzelm@61799 ` 298` ```ML_val \ "setup inactive" ``` wenzelm@60758 ` 299` ```\ ``` krauss@36521 ` 300` ``` Context.theory_map (Function_Common.set_termination_prover ``` blanchet@60682 ` 301` ``` (K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))) ``` wenzelm@60758 ` 302` ```\ ``` krauss@26875 ` 303` krauss@19564 ` 304` ```end ```