Theory FunDef

(*  Title:      HOL/FunDef.thy
    Author:     Alexander Krauss, TU Muenchen
*)

header {* Function Definitions and Termination Proofs *}

theory FunDef
imports Wellfounded
uses
  "Tools/prop_logic.ML"
  "Tools/sat_solver.ML"
  ("Tools/function_package/fundef_lib.ML")
  ("Tools/function_package/fundef_common.ML")
  ("Tools/function_package/inductive_wrap.ML")
  ("Tools/function_package/context_tree.ML")
  ("Tools/function_package/fundef_core.ML")
  ("Tools/function_package/sum_tree.ML")
  ("Tools/function_package/mutual.ML")
  ("Tools/function_package/pattern_split.ML")
  ("Tools/function_package/fundef_package.ML")
  ("Tools/function_package/auto_term.ML")
  ("Tools/function_package/measure_functions.ML")
  ("Tools/function_package/lexicographic_order.ML")
  ("Tools/function_package/fundef_datatype.ML")
  ("Tools/function_package/induction_scheme.ML")
  ("Tools/function_package/termination.ML")
  ("Tools/function_package/decompose.ML")
  ("Tools/function_package/descent.ML")
  ("Tools/function_package/scnp_solve.ML")
  ("Tools/function_package/scnp_reconstruct.ML")
begin

subsection {* 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)
  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"
  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)"
  apply (auto simp:ex1 f_def THE_default1_equality)
  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"
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)
qed

definition 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)

use "Tools/function_package/fundef_lib.ML"
use "Tools/function_package/fundef_common.ML"
use "Tools/function_package/inductive_wrap.ML"
use "Tools/function_package/context_tree.ML"
use "Tools/function_package/fundef_core.ML"
use "Tools/function_package/sum_tree.ML"
use "Tools/function_package/mutual.ML"
use "Tools/function_package/pattern_split.ML"
use "Tools/function_package/auto_term.ML"
use "Tools/function_package/fundef_package.ML"
use "Tools/function_package/fundef_datatype.ML"
use "Tools/function_package/induction_scheme.ML"

setup {* 
  FundefPackage.setup 
  #> FundefDatatype.setup
  #> InductionScheme.setup
*}

subsection {* Measure Functions *}

inductive is_measure :: "('a => nat) => bool"
where is_measure_trivial: "is_measure f"

use "Tools/function_package/measure_functions.ML"
setup MeasureFunctions.setup

lemma 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)

use "Tools/function_package/lexicographic_order.ML"
setup LexicographicOrder.setup 


subsection {* 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 blast

lemmas [fundef_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 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) auto

subsection {* 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) ∧ snd P O fst P ⊆ fst P)"

lemma reduction_pairI[intro]: "wf R ==> S O R ⊆ R ==> reduction_pair (R, S)"
unfolding reduction_pair_def by auto

lemma 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)" "S O fst P ⊆ 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) 
qed

definition
  "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 force


subsection {* Concrete orders for SCNP termination proofs *}

definition "pair_less = less_than <*lex*> less_than"
definition [code del]: "pair_leq = pair_less^="
definition "max_strict = max_ext pair_less"
definition [code del]: "max_weak = max_ext pair_leq ∪ {({}, {})}"
definition [code del]: "min_strict = min_ext pair_less"
definition [code del]: "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 auto

text {* 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 "S O R ⊆ R"
  shows "(max_ext S ∪ {({},{})}) O max_ext R ⊆ max_ext R"
using assms 
apply auto
apply (elim max_ext.cases)
apply rule
apply auto[3]
apply (drule_tac x=xa in meta_spec)
apply simp
apply (erule bexE)
apply (drule_tac x=xb in meta_spec)
by auto

lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
  unfolding max_strict_def max_weak_def 
apply (intro reduction_pairI max_ext_wf)
apply simp
apply (rule max_ext_compat)
by (auto simp: pair_less_def pair_leq_def)

lemma min_ext_compat: 
  assumes "S O R ⊆ R"
  shows "(min_ext S ∪ {({},{})}) O min_ext R ⊆ min_ext R"
using assms 
apply (auto simp: min_ext_def)
apply (drule_tac x=ya in bspec, assumption)
apply (erule bexE)
apply (drule_tac x=xc in bspec)
apply assumption
by auto

lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
  unfolding min_strict_def min_weak_def 
apply (intro reduction_pairI min_ext_wf)
apply simp
apply (rule min_ext_compat)
by (auto simp: pair_less_def pair_leq_def)


subsection {* Tool setup *}

use "Tools/function_package/termination.ML"
use "Tools/function_package/decompose.ML"
use "Tools/function_package/descent.ML"
use "Tools/function_package/scnp_solve.ML"
use "Tools/function_package/scnp_reconstruct.ML"

setup {* ScnpReconstruct.setup *}

ML_val -- "setup inactive"
{*
  Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
*}

end