# Theory FunDef

Up to index of Isabelle/HOL

theory FunDef
imports Partial_Function SAT Wellfounded
`(*  Title:      HOL/FunDef.thy    Author:     Alexander Krauss, TU Muenchen*)header {* Function Definitions and Termination Proofs *}theory FunDefimports Partial_Function SAT Wellfoundedkeywords "function" "termination" :: thy_goal and "fun" :: thy_declbeginsubsection {* 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)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)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)"  apply (simp only: f_def)  apply (rule THE_defaultI')  apply (rule ex1)  donelemma 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"  apply (simp only: f_def)  apply (rule THE_default1_equality [symmetric])   apply (rule ex1)  apply (rule elm)  donelemma 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)"  apply (auto simp:ex1 f_def THE_default1_equality)  apply (rule THE_defaultI')  apply (rule ex1)  donelemma 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"proof -  have "¬(∃y. G x y)"  proof    assume "∃y. G x y"    hence "D x" using graph ..    with `¬ D x` show False ..  qed  hence "¬(∃!y. G x y)" by blast  thus ?thesis    unfolding f_def    by (rule THE_default_none)qeddefinition in_rel_def[simp]:  "in_rel R x y == (x, y) ∈ R"lemma wf_in_rel:  "wf R ==> wfP (in_rel R)"  by (simp add: wfP_def)ML_file "Tools/Function/function_common.ML"ML_file "Tools/Function/context_tree.ML"ML_file "Tools/Function/function_core.ML"ML_file "Tools/Function/sum_tree.ML"ML_file "Tools/Function/mutual.ML"ML_file "Tools/Function/pattern_split.ML"ML_file "Tools/Function/relation.ML"method_setup relation = {*  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))*} "prove termination using a user-specified wellfounded relation"ML_file "Tools/Function/function.ML"ML_file "Tools/Function/pat_completeness.ML"method_setup pat_completeness = {*  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)*} "prove completeness of datatype patterns"ML_file "Tools/Function/fun.ML"ML_file "Tools/Function/induction_schema.ML"method_setup induction_schema = {*  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)*} "prove an induction principle"setup {*  Function.setup  #> Function_Fun.setup*}subsection {* Measure Functions *}inductive is_measure :: "('a => nat) => bool"where is_measure_trivial: "is_measure f"ML_file "Tools/Function/measure_functions.ML"setup MeasureFunctions.setuplemma measure_size[measure_function]: "is_measure size"by (rule is_measure_trivial)lemma measure_fst[measure_function]: "is_measure f ==> is_measure (λp. f (fst p))"by (rule is_measure_trivial)lemma measure_snd[measure_function]: "is_measure f ==> is_measure (λp. f (snd p))"by (rule is_measure_trivial)ML_file "Tools/Function/lexicographic_order.ML"method_setup lexicographic_order = {*  Method.sections clasimp_modifiers >>  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))*} "termination prover for lexicographic orderings"setup Lexicographic_Order.setupsubsection {* Congruence Rules *}lemma let_cong [fundef_cong]:  "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"  unfolding Let_def by blastlemmas [fundef_cong] =  if_cong image_cong INT_cong UN_cong  bex_cong ball_cong imp_cong Option.map_cong Option.bind_conglemma 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]:  "f (g x) = f' (g' x') ==> (f o g) x = (f' o g') x'"  unfolding o_apply .subsection {* Simp rules for termination proofs *}lemma termination_basic_simps[termination_simp]:  "x < (y::nat) ==> x < y + z"  "x < z ==> x < y + z"  "x ≤ y ==> x ≤ y + (z::nat)"  "x ≤ z ==> x ≤ y + (z::nat)"  "x < y ==> x ≤ (y::nat)"by arith+declare le_imp_less_Suc[termination_simp]lemma prod_size_simp[termination_simp]:  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"by (induct p) autosubsection {* Decomposition *}lemma less_by_empty:  "A = {} ==> A ⊆ B"and  union_comp_emptyL:  "[| A O C = {}; B O C = {} |] ==> (A ∪ B) O C = {}"and union_comp_emptyR:  "[| A O B = {}; A O C = {} |] ==> A O (B ∪ C) = {}"and wf_no_loop:  "R O R = {} ==> wf R"by (auto simp add: wf_comp_self[of R])subsection {* Reduction Pairs *}definition  "reduction_pair P = (wf (fst P) ∧ fst P O snd P ⊆ fst P)"lemma reduction_pairI[intro]: "wf R ==> R O S ⊆ R ==> reduction_pair (R, S)"unfolding reduction_pair_def by autolemma reduction_pair_lemma:  assumes rp: "reduction_pair P"  assumes "R ⊆ fst P"  assumes "S ⊆ snd P"  assumes "wf S"  shows "wf (R ∪ S)"proof -  from rp `S ⊆ snd P` have "wf (fst P)" "fst P O S ⊆ fst P"    unfolding reduction_pair_def by auto  with `wf S` have "wf (fst P ∪ S)"    by (auto intro: wf_union_compatible)  moreover from `R ⊆ fst P` have "R ∪ S ⊆ fst P ∪ S" by auto  ultimately show ?thesis by (rule wf_subset)qeddefinition  "rp_inv_image = (λ(R,S) f. (inv_image R f, inv_image S f))"lemma rp_inv_image_rp:  "reduction_pair P ==> reduction_pair (rp_inv_image P f)"  unfolding reduction_pair_def rp_inv_image_def split_def  by forcesubsection {* Concrete orders for SCNP termination proofs *}definition "pair_less = less_than <*lex*> less_than"definition "pair_leq = pair_less^="definition "max_strict = max_ext pair_less"definition "max_weak = max_ext pair_leq ∪ {({}, {})}"definition "min_strict = min_ext pair_less"definition "min_weak = min_ext pair_leq ∪ {({}, {})}"lemma wf_pair_less[simp]: "wf pair_less"  by (auto simp: pair_less_def)text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}lemma pair_leqI1: "a < b ==> ((a, s), (b, t)) ∈ pair_leq"  and pair_leqI2: "a ≤ b ==> s ≤ t ==> ((a, s), (b, t)) ∈ pair_leq"  and pair_lessI1: "a < b  ==> ((a, s), (b, t)) ∈ pair_less"  and pair_lessI2: "a ≤ b ==> s < t ==> ((a, s), (b, t)) ∈ pair_less"  unfolding pair_leq_def pair_less_def by autotext {* Introduction rules for max *}lemma smax_emptyI:  "finite Y ==> Y ≠ {} ==> ({}, Y) ∈ max_strict"  and smax_insertI:  "[|y ∈ Y; (x, y) ∈ pair_less; (X, Y) ∈ max_strict|] ==> (insert x X, Y) ∈ max_strict"  and wmax_emptyI:  "finite X ==> ({}, X) ∈ max_weak"  and wmax_insertI:  "[|y ∈ YS; (x, y) ∈ pair_leq; (XS, YS) ∈ max_weak|] ==> (insert x XS, YS) ∈ max_weak"unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)text {* Introduction rules for min *}lemma smin_emptyI:  "X ≠ {} ==> (X, {}) ∈ min_strict"  and smin_insertI:  "[|x ∈ XS; (x, y) ∈ pair_less; (XS, YS) ∈ min_strict|] ==> (XS, insert y YS) ∈ min_strict"  and wmin_emptyI:  "(X, {}) ∈ min_weak"  and wmin_insertI:  "[|x ∈ XS; (x, y) ∈ pair_leq; (XS, YS) ∈ min_weak|] ==> (XS, insert y YS) ∈ min_weak"by (auto simp: min_strict_def min_weak_def min_ext_def)text {* Reduction Pairs *}lemma max_ext_compat:  assumes "R O S ⊆ R"  shows "max_ext R O (max_ext S ∪ {({},{})}) ⊆ max_ext R"using assmsapply autoapply (elim max_ext.cases)apply ruleapply auto[3]apply (drule_tac x=xa in meta_spec)apply simpapply (erule bexE)apply (drule_tac x=xb in meta_spec)by autolemma max_rpair_set: "reduction_pair (max_strict, max_weak)"  unfolding max_strict_def max_weak_defapply (intro reduction_pairI max_ext_wf)apply simpapply (rule max_ext_compat)by (auto simp: pair_less_def pair_leq_def)lemma min_ext_compat:  assumes "R O S ⊆ R"  shows "min_ext R O  (min_ext S ∪ {({},{})}) ⊆ min_ext R"using assmsapply (auto simp: min_ext_def)apply (drule_tac x=ya in bspec, assumption)apply (erule bexE)apply (drule_tac x=xc in bspec)apply assumptionby autolemma min_rpair_set: "reduction_pair (min_strict, min_weak)"  unfolding min_strict_def min_weak_defapply (intro reduction_pairI min_ext_wf)apply simpapply (rule min_ext_compat)by (auto simp: pair_less_def pair_leq_def)subsection {* Tool setup *}ML_file "Tools/Function/termination.ML"ML_file "Tools/Function/scnp_solve.ML"ML_file "Tools/Function/scnp_reconstruct.ML"setup {* ScnpReconstruct.setup *}ML_val -- "setup inactive"{*  Context.theory_map (Function_Common.set_termination_prover    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))*}end`