Quelle Fun_Def.thy Sprache: Isabelle

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

section \<open>Function Definitions and Termination Proofs\<close>

theory Fun_Def
  imports Basic_BNF_LFPs Partial_Function SAT
  keywords
    "function" "termination" :: thy_goal_defn and
    "fun" "fun_cases" :: thy_defn
begin

subsection \<open>Definitions with default value\<close>

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"
  by (auto simp add: f_def ex1 elm THE_default1_equality[symmetric])

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)"
  by (auto simp add: ex1 f_def THE_default1_equality THE_defaultI')

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"
    then have "D x" using graph ..
    with \<open>\<not> D x\<close> show False ..
  qed
  then have "\(\!y. G x y)" by blast
  then show ?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)

ML_file \<open>Tools/Function/function_core.ML\<close>
ML_file \<open>Tools/Function/mutual.ML\<close>
ML_file \<open>Tools/Function/pattern_split.ML\<close>
ML_file \<open>Tools/Function/relation.ML\<close>
ML_file \<open>Tools/Function/function_elims.ML\<close>

method_setup relation = \<open>
  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
\<close> "prove termination using a user-specified wellfounded relation"

ML_file \<open>Tools/Function/function.ML\<close>
ML_file \<open>Tools/Function/pat_completeness.ML\<close>

method_setup pat_completeness = \<open>
  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
\<close> "prove completeness of (co)datatype patterns"

ML_file \<open>Tools/Function/fun.ML\<close>
ML_file \<open>Tools/Function/induction_schema.ML\<close>

method_setup induction_schema = \<open>
  Scan.succeed (CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
\<close> "prove an induction principle"

subsection \<open>Measure functions\<close>

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

named_theorems measure_function "rules that guide the heuristic generation of measure functions"
ML_file \<open>Tools/Function/measure_functions.ML\<close>

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)

ML_file \<open>Tools/Function/lexicographic_order.ML\<close>

method_setup lexicographic_order = \<open>
  Method.sections clasimp_modifiers >>
  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
\<close> "termination prover for lexicographic orderings"

subsection \<open>Congruence rules\<close>

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
  bex_cong ball_cong imp_cong map_option_cong Option.bind_cong

lemma split_cong [fundef_cong]:
  "(\x y. (x, y) = q \ f x y = g x y) \ p = q \ case_prod f p = case_prod g q"
  by (auto simp: split_def)

lemma comp_cong [fundef_cong]: "f (g x) = f' (g' x') \ (f \ g) x = (f' \ g') x'"
  by (simp only: o_apply)

subsection \<open>Simp rules for termination proofs\<close>

declare
  trans_less_add1[termination_simp]
  trans_less_add2[termination_simp]
  trans_le_add1[termination_simp]
  trans_le_add2[termination_simp]
  less_imp_le_nat[termination_simp]
  le_imp_less_Suc[termination_simp]

lemma size_prod_simp[termination_simp]: "size_prod f g p = f (fst p) + g (snd p) + Suc 0"
  by (induct p) auto

subsection \<open>Decomposition\<close>

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 \<open>Reduction pairs\<close>

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)"
  by (auto simp: reduction_pair_def)

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 \<open>S \<subseteq> snd P\<close> have "wf (fst P)" "fst P O S \<subseteq> fst P"
    unfolding reduction_pair_def by auto
  with \<open>wf S\<close> have "wf (fst P \<union> S)"
    by (auto intro: wf_union_compatible)
  moreover from \<open>R \<subseteq> fst P\<close> have "R \<union> S \<subseteq> fst P \<union> 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 \<open>Concrete orders for SCNP termination proofs\<close>

definition "pair_less = less_than <*lex*> less_than"
definition "pair_leq = pair_less\<^sup>="
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)

lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
  by (auto simp: total_on_def pair_less_def)

text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
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"
  by (auto simp: pair_leq_def pair_less_def)

lemma pair_less_iff1 [simp]: "((x,y), (x,z)) \ pair_less \ y
  by (simp add: pair_less_def)

text \<open>Introduction rules for max\<close>
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"
  by (auto simp: max_strict_def max_weak_def elim!: max_ext.cases)

text \<open>Introduction rules for min\<close>
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 \<open>Reduction Pairs.\<close>

lemma max_ext_compat:
  assumes "R O S \ R"
  shows "max_ext R O (max_ext S \ {({}, {})}) \ max_ext R"
proof -
  have "\X Y Z. (X, Y) \ max_ext R \ (Y, Z) \ max_ext S \ (X, Z) \ max_ext R"
  proof -
    fix X Y Z
    assume "(X,Y)\max_ext R"
      "(Y, Z)\max_ext S"
    then have *: "finite X" "finite Y" "finite Z" "Y\{}" "Z\{}"
      "(\x. x\X \ \y\Y. (x, y)\R)"
      "(\y. y\Y \ \z\Z. (y, z)\S)"
      by (auto elim: max_ext.cases)
    moreover have "\x. x\X \ \z\Z. (x, z)\R"
    proof -
      fix x
      assume "x\X"
      then obtain y where 1: "y\Y" "(x, y)\R"
        using * by auto
      then obtain z where "z\Z" "(y, z)\S"
        using * by auto
      then show "\z\Z. (x, z)\R"
        using assms 1 by (auto elim: max_ext.cases)
    qed
    ultimately show "(X,Z)\max_ext R"
      by auto
  qed
  then show "max_ext R O (max_ext S \ {({}, {})}) \ max_ext R"
    by auto
qed

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)
  apply (auto simp: pair_less_def pair_leq_def)
  done

lemma min_ext_compat:
  assumes "R O S \ R"
  shows "min_ext R O (min_ext S \ {({},{})}) \ min_ext R"
proof -
  have "\X Y Z z. \y\Y. \x\X. (x, y) \ R \ \z\Z. \y\Y. (y, z) \ S
  \<Longrightarrow> z \<in> Z \<Longrightarrow> \<exists>x\<in>X. (x, z) \<in> R"
  proof -
    fix X Y Z z
    assume *: "\y\Y. \x\X. (x, y) \ R"
      "\z\Z. \y\Y. (y, z) \ S"
      "z\Z"
    then obtain y' where 1: "y'\<in>Y" "(y', z) \<in> S"
      by auto
    then obtain x' where 2: "x'\<in>X" "(x', y') \<in> R"
      using * by auto
    show "\x\X. (x, z) \ R"
      using 1 2 assms by auto
  qed
  then show ?thesis
    using assms by (auto simp: min_ext_def)
qed

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)
  apply (auto simp: pair_less_def pair_leq_def)
  done

subsection \<open>Yet more induction principles on the natural numbers\<close>

lemma nat_descend_induct [case_names base descend]:
  fixes P :: "nat \ bool"
  assumes H1: "\k. k > n \ P k"
  assumes H2: "\k. k \ n \ (\i. i > k \ P i) \ P k"
  shows "P m"
  using assms by induction_schema (force intro!: wf_measure [of "\k. Suc n - k"])+

lemma induct_nat_012[case_names 0 1 ge2]:
  "P 0 \ P (Suc 0) \ (\n. P n \ P (Suc n) \ P (Suc (Suc n))) \ P n"
proof (induction_schema, pat_completeness)
  show "wf (Wellfounded.measure id)"
    by simp
qed auto

subsection \<open>Tool setup\<close>

ML_file \<open>Tools/Function/termination.ML\<close>
ML_file \<open>Tools/Function/scnp_solve.ML\<close>
ML_file \<open>Tools/Function/scnp_reconstruct.ML\<close>
ML_file \<open>Tools/Function/fun_cases.ML\<close>

ML_val \<comment> \<open>setup inactive\<close>
\<open>
  Context.theory_map (Function_Common.set_termination_prover
    (K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])))
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.