src/HOL/FunDef.thy
changeset 55085 0e8e4dc55866
parent 55084 8ee9aabb2bca
child 55086 500ef036117b
     1.1 --- a/src/HOL/FunDef.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,321 +0,0 @@
     1.4 -(*  Title:      HOL/FunDef.thy
     1.5 -    Author:     Alexander Krauss, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Function Definitions and Termination Proofs *}
     1.9 -
    1.10 -theory FunDef
    1.11 -imports Partial_Function SAT Wellfounded
    1.12 -keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
    1.13 -begin
    1.14 -
    1.15 -subsection {* Definitions with default value. *}
    1.16 -
    1.17 -definition
    1.18 -  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    1.19 -  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
    1.20 -
    1.21 -lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
    1.22 -  by (simp add: theI' THE_default_def)
    1.23 -
    1.24 -lemma THE_default1_equality:
    1.25 -    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
    1.26 -  by (simp add: the1_equality THE_default_def)
    1.27 -
    1.28 -lemma THE_default_none:
    1.29 -    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
    1.30 -  by (simp add:THE_default_def)
    1.31 -
    1.32 -
    1.33 -lemma fundef_ex1_existence:
    1.34 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    1.35 -  assumes ex1: "\<exists>!y. G x y"
    1.36 -  shows "G x (f x)"
    1.37 -  apply (simp only: f_def)
    1.38 -  apply (rule THE_defaultI')
    1.39 -  apply (rule ex1)
    1.40 -  done
    1.41 -
    1.42 -lemma fundef_ex1_uniqueness:
    1.43 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    1.44 -  assumes ex1: "\<exists>!y. G x y"
    1.45 -  assumes elm: "G x (h x)"
    1.46 -  shows "h x = f x"
    1.47 -  apply (simp only: f_def)
    1.48 -  apply (rule THE_default1_equality [symmetric])
    1.49 -   apply (rule ex1)
    1.50 -  apply (rule elm)
    1.51 -  done
    1.52 -
    1.53 -lemma fundef_ex1_iff:
    1.54 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    1.55 -  assumes ex1: "\<exists>!y. G x y"
    1.56 -  shows "(G x y) = (f x = y)"
    1.57 -  apply (auto simp:ex1 f_def THE_default1_equality)
    1.58 -  apply (rule THE_defaultI')
    1.59 -  apply (rule ex1)
    1.60 -  done
    1.61 -
    1.62 -lemma fundef_default_value:
    1.63 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    1.64 -  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
    1.65 -  assumes "\<not> D x"
    1.66 -  shows "f x = d x"
    1.67 -proof -
    1.68 -  have "\<not>(\<exists>y. G x y)"
    1.69 -  proof
    1.70 -    assume "\<exists>y. G x y"
    1.71 -    hence "D x" using graph ..
    1.72 -    with `\<not> D x` show False ..
    1.73 -  qed
    1.74 -  hence "\<not>(\<exists>!y. G x y)" by blast
    1.75 -
    1.76 -  thus ?thesis
    1.77 -    unfolding f_def
    1.78 -    by (rule THE_default_none)
    1.79 -qed
    1.80 -
    1.81 -definition in_rel_def[simp]:
    1.82 -  "in_rel R x y == (x, y) \<in> R"
    1.83 -
    1.84 -lemma wf_in_rel:
    1.85 -  "wf R \<Longrightarrow> wfP (in_rel R)"
    1.86 -  by (simp add: wfP_def)
    1.87 -
    1.88 -ML_file "Tools/Function/function_common.ML"
    1.89 -ML_file "Tools/Function/context_tree.ML"
    1.90 -ML_file "Tools/Function/function_core.ML"
    1.91 -ML_file "Tools/Function/sum_tree.ML"
    1.92 -ML_file "Tools/Function/mutual.ML"
    1.93 -ML_file "Tools/Function/pattern_split.ML"
    1.94 -ML_file "Tools/Function/relation.ML"
    1.95 -ML_file "Tools/Function/function_elims.ML"
    1.96 -
    1.97 -method_setup relation = {*
    1.98 -  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
    1.99 -*} "prove termination using a user-specified wellfounded relation"
   1.100 -
   1.101 -ML_file "Tools/Function/function.ML"
   1.102 -ML_file "Tools/Function/pat_completeness.ML"
   1.103 -
   1.104 -method_setup pat_completeness = {*
   1.105 -  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   1.106 -*} "prove completeness of datatype patterns"
   1.107 -
   1.108 -ML_file "Tools/Function/fun.ML"
   1.109 -ML_file "Tools/Function/induction_schema.ML"
   1.110 -
   1.111 -method_setup induction_schema = {*
   1.112 -  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   1.113 -*} "prove an induction principle"
   1.114 -
   1.115 -setup {*
   1.116 -  Function.setup
   1.117 -  #> Function_Fun.setup
   1.118 -*}
   1.119 -
   1.120 -subsection {* Measure Functions *}
   1.121 -
   1.122 -inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
   1.123 -where is_measure_trivial: "is_measure f"
   1.124 -
   1.125 -ML_file "Tools/Function/measure_functions.ML"
   1.126 -setup MeasureFunctions.setup
   1.127 -
   1.128 -lemma measure_size[measure_function]: "is_measure size"
   1.129 -by (rule is_measure_trivial)
   1.130 -
   1.131 -lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
   1.132 -by (rule is_measure_trivial)
   1.133 -lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   1.134 -by (rule is_measure_trivial)
   1.135 -
   1.136 -ML_file "Tools/Function/lexicographic_order.ML"
   1.137 -
   1.138 -method_setup lexicographic_order = {*
   1.139 -  Method.sections clasimp_modifiers >>
   1.140 -  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
   1.141 -*} "termination prover for lexicographic orderings"
   1.142 -
   1.143 -setup Lexicographic_Order.setup
   1.144 -
   1.145 -
   1.146 -subsection {* Congruence Rules *}
   1.147 -
   1.148 -lemma let_cong [fundef_cong]:
   1.149 -  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   1.150 -  unfolding Let_def by blast
   1.151 -
   1.152 -lemmas [fundef_cong] =
   1.153 -  if_cong image_cong INT_cong UN_cong
   1.154 -  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
   1.155 -
   1.156 -lemma split_cong [fundef_cong]:
   1.157 -  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
   1.158 -    \<Longrightarrow> split f p = split g q"
   1.159 -  by (auto simp: split_def)
   1.160 -
   1.161 -lemma comp_cong [fundef_cong]:
   1.162 -  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   1.163 -  unfolding o_apply .
   1.164 -
   1.165 -subsection {* Simp rules for termination proofs *}
   1.166 -
   1.167 -lemma termination_basic_simps[termination_simp]:
   1.168 -  "x < (y::nat) \<Longrightarrow> x < y + z"
   1.169 -  "x < z \<Longrightarrow> x < y + z"
   1.170 -  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
   1.171 -  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
   1.172 -  "x < y \<Longrightarrow> x \<le> (y::nat)"
   1.173 -by arith+
   1.174 -
   1.175 -declare le_imp_less_Suc[termination_simp]
   1.176 -
   1.177 -lemma prod_size_simp[termination_simp]:
   1.178 -  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
   1.179 -by (induct p) auto
   1.180 -
   1.181 -subsection {* Decomposition *}
   1.182 -
   1.183 -lemma less_by_empty:
   1.184 -  "A = {} \<Longrightarrow> A \<subseteq> B"
   1.185 -and  union_comp_emptyL:
   1.186 -  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
   1.187 -and union_comp_emptyR:
   1.188 -  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
   1.189 -and wf_no_loop:
   1.190 -  "R O R = {} \<Longrightarrow> wf R"
   1.191 -by (auto simp add: wf_comp_self[of R])
   1.192 -
   1.193 -
   1.194 -subsection {* Reduction Pairs *}
   1.195 -
   1.196 -definition
   1.197 -  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
   1.198 -
   1.199 -lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
   1.200 -unfolding reduction_pair_def by auto
   1.201 -
   1.202 -lemma reduction_pair_lemma:
   1.203 -  assumes rp: "reduction_pair P"
   1.204 -  assumes "R \<subseteq> fst P"
   1.205 -  assumes "S \<subseteq> snd P"
   1.206 -  assumes "wf S"
   1.207 -  shows "wf (R \<union> S)"
   1.208 -proof -
   1.209 -  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
   1.210 -    unfolding reduction_pair_def by auto
   1.211 -  with `wf S` have "wf (fst P \<union> S)"
   1.212 -    by (auto intro: wf_union_compatible)
   1.213 -  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
   1.214 -  ultimately show ?thesis by (rule wf_subset)
   1.215 -qed
   1.216 -
   1.217 -definition
   1.218 -  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
   1.219 -
   1.220 -lemma rp_inv_image_rp:
   1.221 -  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
   1.222 -  unfolding reduction_pair_def rp_inv_image_def split_def
   1.223 -  by force
   1.224 -
   1.225 -
   1.226 -subsection {* Concrete orders for SCNP termination proofs *}
   1.227 -
   1.228 -definition "pair_less = less_than <*lex*> less_than"
   1.229 -definition "pair_leq = pair_less^="
   1.230 -definition "max_strict = max_ext pair_less"
   1.231 -definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
   1.232 -definition "min_strict = min_ext pair_less"
   1.233 -definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
   1.234 -
   1.235 -lemma wf_pair_less[simp]: "wf pair_less"
   1.236 -  by (auto simp: pair_less_def)
   1.237 -
   1.238 -text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
   1.239 -lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   1.240 -  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   1.241 -  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   1.242 -  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   1.243 -  unfolding pair_leq_def pair_less_def by auto
   1.244 -
   1.245 -text {* Introduction rules for max *}
   1.246 -lemma smax_emptyI:
   1.247 -  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
   1.248 -  and smax_insertI:
   1.249 -  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
   1.250 -  and wmax_emptyI:
   1.251 -  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
   1.252 -  and wmax_insertI:
   1.253 -  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
   1.254 -unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
   1.255 -
   1.256 -text {* Introduction rules for min *}
   1.257 -lemma smin_emptyI:
   1.258 -  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
   1.259 -  and smin_insertI:
   1.260 -  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
   1.261 -  and wmin_emptyI:
   1.262 -  "(X, {}) \<in> min_weak"
   1.263 -  and wmin_insertI:
   1.264 -  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
   1.265 -by (auto simp: min_strict_def min_weak_def min_ext_def)
   1.266 -
   1.267 -text {* Reduction Pairs *}
   1.268 -
   1.269 -lemma max_ext_compat:
   1.270 -  assumes "R O S \<subseteq> R"
   1.271 -  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
   1.272 -using assms
   1.273 -apply auto
   1.274 -apply (elim max_ext.cases)
   1.275 -apply rule
   1.276 -apply auto[3]
   1.277 -apply (drule_tac x=xa in meta_spec)
   1.278 -apply simp
   1.279 -apply (erule bexE)
   1.280 -apply (drule_tac x=xb in meta_spec)
   1.281 -by auto
   1.282 -
   1.283 -lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   1.284 -  unfolding max_strict_def max_weak_def
   1.285 -apply (intro reduction_pairI max_ext_wf)
   1.286 -apply simp
   1.287 -apply (rule max_ext_compat)
   1.288 -by (auto simp: pair_less_def pair_leq_def)
   1.289 -
   1.290 -lemma min_ext_compat:
   1.291 -  assumes "R O S \<subseteq> R"
   1.292 -  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
   1.293 -using assms
   1.294 -apply (auto simp: min_ext_def)
   1.295 -apply (drule_tac x=ya in bspec, assumption)
   1.296 -apply (erule bexE)
   1.297 -apply (drule_tac x=xc in bspec)
   1.298 -apply assumption
   1.299 -by auto
   1.300 -
   1.301 -lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   1.302 -  unfolding min_strict_def min_weak_def
   1.303 -apply (intro reduction_pairI min_ext_wf)
   1.304 -apply simp
   1.305 -apply (rule min_ext_compat)
   1.306 -by (auto simp: pair_less_def pair_leq_def)
   1.307 -
   1.308 -
   1.309 -subsection {* Tool setup *}
   1.310 -
   1.311 -ML_file "Tools/Function/termination.ML"
   1.312 -ML_file "Tools/Function/scnp_solve.ML"
   1.313 -ML_file "Tools/Function/scnp_reconstruct.ML"
   1.314 -ML_file "Tools/Function/fun_cases.ML"
   1.315 -
   1.316 -setup ScnpReconstruct.setup
   1.317 -
   1.318 -ML_val -- "setup inactive"
   1.319 -{*
   1.320 -  Context.theory_map (Function_Common.set_termination_prover
   1.321 -    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
   1.322 -*}
   1.323 -
   1.324 -end