wenzelm@20324: (* Title: HOL/FunDef.thy wenzelm@20324: ID: $Id$ wenzelm@20324: Author: Alexander Krauss, TU Muenchen wenzelm@22816: *) wenzelm@20324: wenzelm@22816: header {* General recursive function definitions *} wenzelm@20324: krauss@19564: theory FunDef wenzelm@22816: imports Accessible_Part wenzelm@22816: uses wenzelm@22816: ("Tools/function_package/sum_tools.ML") wenzelm@22816: ("Tools/function_package/fundef_common.ML") wenzelm@22816: ("Tools/function_package/fundef_lib.ML") wenzelm@22816: ("Tools/function_package/inductive_wrap.ML") wenzelm@22816: ("Tools/function_package/context_tree.ML") wenzelm@22816: ("Tools/function_package/fundef_core.ML") wenzelm@22816: ("Tools/function_package/mutual.ML") wenzelm@22816: ("Tools/function_package/pattern_split.ML") wenzelm@22816: ("Tools/function_package/fundef_package.ML") wenzelm@22816: ("Tools/function_package/auto_term.ML") krauss@19564: begin krauss@19564: wenzelm@22816: text {* Definitions with default value. *} krauss@20536: krauss@20536: definition wenzelm@21404: THE_default :: "'a \ ('a \ bool) \ 'a" where krauss@20536: "THE_default d P = (if (\!x. P x) then (THE x. P x) else d)" krauss@20536: krauss@20536: lemma THE_defaultI': "\!x. P x \ P (THE_default d P)" wenzelm@22816: by (simp add: theI' THE_default_def) krauss@20536: wenzelm@22816: lemma THE_default1_equality: wenzelm@22816: "\\!x. P x; P a\ \ THE_default d P = a" wenzelm@22816: by (simp add: the1_equality THE_default_def) krauss@20536: krauss@20536: lemma THE_default_none: wenzelm@22816: "\(\!x. P x) \ THE_default d P = d" wenzelm@22816: by (simp add:THE_default_def) krauss@20536: krauss@20536: krauss@19564: lemma fundef_ex1_existence: wenzelm@22816: assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" wenzelm@22816: assumes ex1: "\!y. G x y" wenzelm@22816: shows "G x (f x)" wenzelm@22816: apply (simp only: f_def) wenzelm@22816: apply (rule THE_defaultI') wenzelm@22816: apply (rule ex1) wenzelm@22816: done krauss@21051: krauss@19564: lemma fundef_ex1_uniqueness: wenzelm@22816: assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" wenzelm@22816: assumes ex1: "\!y. G x y" wenzelm@22816: assumes elm: "G x (h x)" wenzelm@22816: shows "h x = f x" wenzelm@22816: apply (simp only: f_def) wenzelm@22816: apply (rule THE_default1_equality [symmetric]) wenzelm@22816: apply (rule ex1) wenzelm@22816: apply (rule elm) wenzelm@22816: done krauss@19564: krauss@19564: lemma fundef_ex1_iff: wenzelm@22816: assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" wenzelm@22816: assumes ex1: "\!y. G x y" wenzelm@22816: shows "(G x y) = (f x = y)" krauss@20536: apply (auto simp:ex1 f_def THE_default1_equality) wenzelm@22816: apply (rule THE_defaultI') wenzelm@22816: apply (rule ex1) wenzelm@22816: done krauss@19564: krauss@20654: lemma fundef_default_value: wenzelm@22816: assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" wenzelm@22816: assumes graph: "\x y. G x y \ D x" wenzelm@22816: assumes "\ D x" wenzelm@22816: shows "f x = d x" krauss@20654: proof - krauss@21051: have "\(\y. G x y)" krauss@20654: proof krauss@21512: assume "\y. G x y" krauss@21512: hence "D x" using graph .. krauss@21512: with `\ D x` show False .. krauss@20654: qed krauss@21051: hence "\(\!y. G x y)" by blast wenzelm@22816: krauss@20654: thus ?thesis krauss@20654: unfolding f_def krauss@20654: by (rule THE_default_none) krauss@20654: qed krauss@20654: krauss@20654: krauss@19770: use "Tools/function_package/sum_tools.ML" krauss@19564: use "Tools/function_package/fundef_common.ML" krauss@19564: use "Tools/function_package/fundef_lib.ML" krauss@20523: use "Tools/function_package/inductive_wrap.ML" krauss@19564: use "Tools/function_package/context_tree.ML" krauss@22166: use "Tools/function_package/fundef_core.ML" krauss@19770: use "Tools/function_package/mutual.ML" krauss@20270: use "Tools/function_package/pattern_split.ML" krauss@21319: use "Tools/function_package/auto_term.ML" krauss@19564: use "Tools/function_package/fundef_package.ML" krauss@19564: krauss@19564: setup FundefPackage.setup krauss@19770: haftmann@22838: lemma let_cong [fundef_cong]: haftmann@22838: "M = N \ (\x. x = N \ f x = g x) \ Let M f = Let N g" wenzelm@22816: unfolding Let_def by blast krauss@22622: wenzelm@22816: lemmas [fundef_cong] = haftmann@22838: if_cong image_cong INT_cong UN_cong haftmann@22838: bex_cong ball_cong imp_cong krauss@19564: wenzelm@22816: lemma split_cong [fundef_cong]: haftmann@22838: "(\x y. (x, y) = q \ f x y = g x y) \ p = q wenzelm@22816: \ split f p = split g q" wenzelm@22816: by (auto simp: split_def) krauss@19934: wenzelm@22816: lemma comp_cong [fundef_cong]: haftmann@22838: "f (g x) = f' (g' x') \ (f o g) x = (f' o g') x'" wenzelm@22816: unfolding o_apply . krauss@19934: krauss@19564: end