wenzelm@20324: (* Title: HOL/FunDef.thy wenzelm@20324: ID: $Id$ wenzelm@20324: Author: Alexander Krauss, TU Muenchen wenzelm@20324: wenzelm@20324: A package for general recursive function definitions. wenzelm@20324: *) wenzelm@20324: krauss@19564: theory FunDef krauss@19770: imports Accessible_Part Datatype Recdef krauss@19564: uses krauss@19770: ("Tools/function_package/sum_tools.ML") krauss@19564: ("Tools/function_package/fundef_common.ML") krauss@19564: ("Tools/function_package/fundef_lib.ML") krauss@20523: ("Tools/function_package/inductive_wrap.ML") krauss@19564: ("Tools/function_package/context_tree.ML") krauss@19564: ("Tools/function_package/fundef_prep.ML") krauss@19564: ("Tools/function_package/fundef_proof.ML") krauss@19564: ("Tools/function_package/termination.ML") krauss@19770: ("Tools/function_package/mutual.ML") krauss@20270: ("Tools/function_package/pattern_split.ML") krauss@19564: ("Tools/function_package/fundef_package.ML") krauss@19770: ("Tools/function_package/fundef_datatype.ML") krauss@19770: ("Tools/function_package/auto_term.ML") krauss@19564: begin krauss@19564: krauss@20536: krauss@20536: definition krauss@20536: THE_default :: "'a \ ('a \ bool) \ 'a" 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)" krauss@20536: by (simp add:theI' THE_default_def) krauss@20536: krauss@20536: lemma THE_default1_equality: krauss@20536: "\\!x. P x; P a\ \ THE_default d P = a" krauss@20536: by (simp add:the1_equality THE_default_def) krauss@20536: krauss@20536: lemma THE_default_none: krauss@20536: "\(\!x. P x) \ THE_default d P = d" krauss@20536: by (simp add:THE_default_def) krauss@20536: krauss@20536: krauss@19564: lemma fundef_ex1_existence: krauss@20654: assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" krauss@19564: assumes ex1: "\!y. (x,y)\G" krauss@19564: shows "(x, f x)\G" krauss@20536: by (simp only:f_def, rule THE_defaultI', rule ex1) krauss@19564: krauss@19564: lemma fundef_ex1_uniqueness: krauss@20654: assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" krauss@19564: assumes ex1: "\!y. (x,y)\G" krauss@19564: assumes elm: "(x, h x)\G" krauss@19564: shows "h x = f x" krauss@20536: by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) krauss@19564: krauss@19564: lemma fundef_ex1_iff: krauss@20654: assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" krauss@19564: assumes ex1: "\!y. (x,y)\G" krauss@19564: shows "((x, y)\G) = (f x = y)" krauss@20536: apply (auto simp:ex1 f_def THE_default1_equality) krauss@20536: by (rule THE_defaultI', rule ex1) krauss@19564: krauss@20654: lemma fundef_default_value: krauss@20654: assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" krauss@20654: assumes graph: "\x y. (x,y) \ G \ x \ D" krauss@20654: assumes "x \ D" krauss@20654: shows "f x = d x" krauss@20654: proof - krauss@20654: have "\(\y. (x, y) \ G)" krauss@20654: proof krauss@20654: assume "(\y. (x, y) \ G)" krauss@20654: with graph and `x\D` show False by blast krauss@20654: qed krauss@20654: hence "\(\!y. (x, y) \ G)" by blast krauss@20654: krauss@20654: thus ?thesis krauss@20654: unfolding f_def krauss@20654: by (rule THE_default_none) krauss@20654: qed krauss@20654: krauss@20654: krauss@20654: krauss@19564: krauss@19770: subsection {* Projections *} krauss@19770: consts krauss@19770: lpg::"(('a + 'b) * 'a) set" krauss@19770: rpg::"(('a + 'b) * 'b) set" krauss@19770: krauss@19770: inductive lpg krauss@19770: intros krauss@19770: "(Inl x, x) : lpg" krauss@19770: inductive rpg krauss@19770: intros krauss@19770: "(Inr y, y) : rpg" krauss@19770: definition krauss@19770: "lproj x = (THE y. (x,y) : lpg)" krauss@19770: "rproj x = (THE y. (x,y) : rpg)" krauss@19770: krauss@19770: lemma lproj_inl: krauss@19770: "lproj (Inl x) = x" krauss@19770: by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases) krauss@19770: lemma rproj_inr: krauss@19770: "rproj (Inr x) = x" krauss@19770: by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases) krauss@19770: krauss@19770: krauss@19770: krauss@19770: 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@19564: use "Tools/function_package/fundef_prep.ML" krauss@19564: use "Tools/function_package/fundef_proof.ML" krauss@19564: use "Tools/function_package/termination.ML" krauss@19770: use "Tools/function_package/mutual.ML" krauss@20270: use "Tools/function_package/pattern_split.ML" krauss@19564: use "Tools/function_package/fundef_package.ML" krauss@19564: krauss@19564: setup FundefPackage.setup krauss@19564: krauss@19770: use "Tools/function_package/fundef_datatype.ML" krauss@19770: setup FundefDatatype.setup krauss@19770: krauss@19770: use "Tools/function_package/auto_term.ML" krauss@19770: setup FundefAutoTerm.setup krauss@19770: krauss@19770: krauss@19770: lemmas [fundef_cong] = krauss@19770: let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong krauss@19564: krauss@19564: krauss@19934: lemma split_cong[fundef_cong]: krauss@19934: "\ \x y. (x, y) = q \ f x y = g x y; p = q \ krauss@19934: \ split f p = split g q" krauss@19934: by (auto simp:split_def) krauss@19934: krauss@19934: krauss@19564: end