# HG changeset patch # User wenzelm # Date 1177598350 -7200 # Node ID 0eba117368d92dcf6d2c611ea914bf2c3411db25 # Parent d2b05f9462e071f19f4e47e65c8e09a43a0a6da3 added header; tuned presentation; diff -r d2b05f9462e0 -r 0eba117368d9 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Apr 26 16:24:13 2007 +0200 +++ b/src/HOL/FunDef.thy Thu Apr 26 16:39:10 2007 +0200 @@ -1,72 +1,77 @@ (* Title: HOL/FunDef.thy ID: $Id$ Author: Alexander Krauss, TU Muenchen +*) -A package for general recursive function definitions. -*) +header {* General recursive function definitions *} theory FunDef -imports Accessible_Part -uses -("Tools/function_package/sum_tools.ML") -("Tools/function_package/fundef_common.ML") -("Tools/function_package/fundef_lib.ML") -("Tools/function_package/inductive_wrap.ML") -("Tools/function_package/context_tree.ML") -("Tools/function_package/fundef_core.ML") -("Tools/function_package/mutual.ML") -("Tools/function_package/pattern_split.ML") -("Tools/function_package/fundef_package.ML") -("Tools/function_package/auto_term.ML") +imports Accessible_Part +uses + ("Tools/function_package/sum_tools.ML") + ("Tools/function_package/fundef_common.ML") + ("Tools/function_package/fundef_lib.ML") + ("Tools/function_package/inductive_wrap.ML") + ("Tools/function_package/context_tree.ML") + ("Tools/function_package/fundef_core.ML") + ("Tools/function_package/mutual.ML") + ("Tools/function_package/pattern_split.ML") + ("Tools/function_package/fundef_package.ML") + ("Tools/function_package/auto_term.ML") begin -section {* Definitions with default value *} +text {* Definitions with default value. *} definition THE_default :: "'a \ ('a \ bool) \ 'a" where "THE_default d P = (if (\!x. P x) then (THE x. P x) else d)" lemma THE_defaultI': "\!x. P x \ P (THE_default d P)" - by (simp add:theI' THE_default_def) + by (simp add: theI' THE_default_def) -lemma THE_default1_equality: - "\\!x. P x; P a\ \ THE_default d P = a" - by (simp add:the1_equality THE_default_def) +lemma THE_default1_equality: + "\\!x. P x; P a\ \ THE_default d P = a" + by (simp add: the1_equality THE_default_def) lemma THE_default_none: - "\(\!x. P x) \ THE_default d P = d" -by (simp add:THE_default_def) + "\(\!x. P x) \ THE_default d P = d" + by (simp add:THE_default_def) lemma fundef_ex1_existence: -assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" -assumes ex1: "\!y. G x y" -shows "G x (f x)" - by (simp only:f_def, rule THE_defaultI', rule ex1) - - - - + assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" + assumes ex1: "\!y. G x y" + shows "G x (f x)" + apply (simp only: f_def) + apply (rule THE_defaultI') + apply (rule ex1) + done lemma fundef_ex1_uniqueness: -assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" -assumes ex1: "\!y. G x y" -assumes elm: "G x (h x)" -shows "h x = f x" - by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) + assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" + assumes ex1: "\!y. G x y" + assumes elm: "G x (h x)" + shows "h x = f x" + apply (simp only: f_def) + apply (rule THE_default1_equality [symmetric]) + apply (rule ex1) + apply (rule elm) + done lemma fundef_ex1_iff: -assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" -assumes ex1: "\!y. G x y" -shows "(G x y) = (f x = y)" + assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" + assumes ex1: "\!y. G x y" + shows "(G x y) = (f x = y)" apply (auto simp:ex1 f_def THE_default1_equality) - by (rule THE_defaultI', rule ex1) + apply (rule THE_defaultI') + apply (rule ex1) + done lemma fundef_default_value: -assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" -assumes graph: "\x y. G x y \ D x" -assumes "\ D x" -shows "f x = d x" + assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" + assumes graph: "\x y. G x y \ D x" + assumes "\ D x" + shows "f x = d x" proof - have "\(\y. G x y)" proof @@ -75,14 +80,13 @@ with `\ D x` show False .. qed hence "\(\!y. G x y)" by blast - + thus ?thesis unfolding f_def by (rule THE_default_none) qed - use "Tools/function_package/sum_tools.ML" use "Tools/function_package/fundef_common.ML" use "Tools/function_package/fundef_lib.ML" @@ -98,20 +102,20 @@ lemma let_cong: "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" - by (unfold Let_def) blast + unfolding Let_def by blast -lemmas [fundef_cong] = +lemmas [fundef_cong] = let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong -lemma split_cong[fundef_cong]: - "\ \x y. (x, y) = q \ f x y = g x y; p = q \ - \ split f p = split g q" - by (auto simp:split_def) +lemma split_cong [fundef_cong]: + "\ \x y. (x, y) = q \ f x y = g x y; p = q \ + \ split f p = split g q" + by (auto simp: split_def) -lemma comp_cong[fundef_cong]: +lemma comp_cong [fundef_cong]: "f (g x) = f' (g' x') - ==> (f o g) x = (f' o g') x'" -unfolding o_apply . + ==> (f o g) x = (f' o g') x'" + unfolding o_apply . end