src/HOL/Fun_Def.thy
changeset 55085 0e8e4dc55866
parent 54407 e95831757903
child 55466 786edc984c98
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Fun_Def.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -0,0 +1,319 @@
     1.4 +(*  Title:      HOL/Fun_Def.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 Fun_Def
    1.11 +imports Partial_Function SAT
    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_core.ML"
    1.89 +ML_file "Tools/Function/sum_tree.ML"
    1.90 +ML_file "Tools/Function/mutual.ML"
    1.91 +ML_file "Tools/Function/pattern_split.ML"
    1.92 +ML_file "Tools/Function/relation.ML"
    1.93 +ML_file "Tools/Function/function_elims.ML"
    1.94 +
    1.95 +method_setup relation = {*
    1.96 +  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
    1.97 +*} "prove termination using a user-specified wellfounded relation"
    1.98 +
    1.99 +ML_file "Tools/Function/function.ML"
   1.100 +ML_file "Tools/Function/pat_completeness.ML"
   1.101 +
   1.102 +method_setup pat_completeness = {*
   1.103 +  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   1.104 +*} "prove completeness of datatype patterns"
   1.105 +
   1.106 +ML_file "Tools/Function/fun.ML"
   1.107 +ML_file "Tools/Function/induction_schema.ML"
   1.108 +
   1.109 +method_setup induction_schema = {*
   1.110 +  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   1.111 +*} "prove an induction principle"
   1.112 +
   1.113 +setup {*
   1.114 +  Function.setup
   1.115 +  #> Function_Fun.setup
   1.116 +*}
   1.117 +
   1.118 +subsection {* Measure Functions *}
   1.119 +
   1.120 +inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
   1.121 +where is_measure_trivial: "is_measure f"
   1.122 +
   1.123 +ML_file "Tools/Function/measure_functions.ML"
   1.124 +setup MeasureFunctions.setup
   1.125 +
   1.126 +lemma measure_size[measure_function]: "is_measure size"
   1.127 +by (rule is_measure_trivial)
   1.128 +
   1.129 +lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
   1.130 +by (rule is_measure_trivial)
   1.131 +lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   1.132 +by (rule is_measure_trivial)
   1.133 +
   1.134 +ML_file "Tools/Function/lexicographic_order.ML"
   1.135 +
   1.136 +method_setup lexicographic_order = {*
   1.137 +  Method.sections clasimp_modifiers >>
   1.138 +  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
   1.139 +*} "termination prover for lexicographic orderings"
   1.140 +
   1.141 +setup Lexicographic_Order.setup
   1.142 +
   1.143 +
   1.144 +subsection {* Congruence Rules *}
   1.145 +
   1.146 +lemma let_cong [fundef_cong]:
   1.147 +  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   1.148 +  unfolding Let_def by blast
   1.149 +
   1.150 +lemmas [fundef_cong] =
   1.151 +  if_cong image_cong INT_cong UN_cong
   1.152 +  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
   1.153 +
   1.154 +lemma split_cong [fundef_cong]:
   1.155 +  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
   1.156 +    \<Longrightarrow> split f p = split g q"
   1.157 +  by (auto simp: split_def)
   1.158 +
   1.159 +lemma comp_cong [fundef_cong]:
   1.160 +  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   1.161 +  unfolding o_apply .
   1.162 +
   1.163 +subsection {* Simp rules for termination proofs *}
   1.164 +
   1.165 +lemma termination_basic_simps[termination_simp]:
   1.166 +  "x < (y::nat) \<Longrightarrow> x < y + z"
   1.167 +  "x < z \<Longrightarrow> x < y + z"
   1.168 +  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
   1.169 +  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
   1.170 +  "x < y \<Longrightarrow> x \<le> (y::nat)"
   1.171 +by arith+
   1.172 +
   1.173 +declare le_imp_less_Suc[termination_simp]
   1.174 +
   1.175 +lemma prod_size_simp[termination_simp]:
   1.176 +  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
   1.177 +by (induct p) auto
   1.178 +
   1.179 +subsection {* Decomposition *}
   1.180 +
   1.181 +lemma less_by_empty:
   1.182 +  "A = {} \<Longrightarrow> A \<subseteq> B"
   1.183 +and  union_comp_emptyL:
   1.184 +  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
   1.185 +and union_comp_emptyR:
   1.186 +  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
   1.187 +and wf_no_loop:
   1.188 +  "R O R = {} \<Longrightarrow> wf R"
   1.189 +by (auto simp add: wf_comp_self[of R])
   1.190 +
   1.191 +
   1.192 +subsection {* Reduction Pairs *}
   1.193 +
   1.194 +definition
   1.195 +  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
   1.196 +
   1.197 +lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
   1.198 +unfolding reduction_pair_def by auto
   1.199 +
   1.200 +lemma reduction_pair_lemma:
   1.201 +  assumes rp: "reduction_pair P"
   1.202 +  assumes "R \<subseteq> fst P"
   1.203 +  assumes "S \<subseteq> snd P"
   1.204 +  assumes "wf S"
   1.205 +  shows "wf (R \<union> S)"
   1.206 +proof -
   1.207 +  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
   1.208 +    unfolding reduction_pair_def by auto
   1.209 +  with `wf S` have "wf (fst P \<union> S)"
   1.210 +    by (auto intro: wf_union_compatible)
   1.211 +  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
   1.212 +  ultimately show ?thesis by (rule wf_subset)
   1.213 +qed
   1.214 +
   1.215 +definition
   1.216 +  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
   1.217 +
   1.218 +lemma rp_inv_image_rp:
   1.219 +  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
   1.220 +  unfolding reduction_pair_def rp_inv_image_def split_def
   1.221 +  by force
   1.222 +
   1.223 +
   1.224 +subsection {* Concrete orders for SCNP termination proofs *}
   1.225 +
   1.226 +definition "pair_less = less_than <*lex*> less_than"
   1.227 +definition "pair_leq = pair_less^="
   1.228 +definition "max_strict = max_ext pair_less"
   1.229 +definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
   1.230 +definition "min_strict = min_ext pair_less"
   1.231 +definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
   1.232 +
   1.233 +lemma wf_pair_less[simp]: "wf pair_less"
   1.234 +  by (auto simp: pair_less_def)
   1.235 +
   1.236 +text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
   1.237 +lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   1.238 +  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   1.239 +  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   1.240 +  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   1.241 +  unfolding pair_leq_def pair_less_def by auto
   1.242 +
   1.243 +text {* Introduction rules for max *}
   1.244 +lemma smax_emptyI:
   1.245 +  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
   1.246 +  and smax_insertI:
   1.247 +  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
   1.248 +  and wmax_emptyI:
   1.249 +  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
   1.250 +  and wmax_insertI:
   1.251 +  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
   1.252 +unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
   1.253 +
   1.254 +text {* Introduction rules for min *}
   1.255 +lemma smin_emptyI:
   1.256 +  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
   1.257 +  and smin_insertI:
   1.258 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
   1.259 +  and wmin_emptyI:
   1.260 +  "(X, {}) \<in> min_weak"
   1.261 +  and wmin_insertI:
   1.262 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
   1.263 +by (auto simp: min_strict_def min_weak_def min_ext_def)
   1.264 +
   1.265 +text {* Reduction Pairs *}
   1.266 +
   1.267 +lemma max_ext_compat:
   1.268 +  assumes "R O S \<subseteq> R"
   1.269 +  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
   1.270 +using assms
   1.271 +apply auto
   1.272 +apply (elim max_ext.cases)
   1.273 +apply rule
   1.274 +apply auto[3]
   1.275 +apply (drule_tac x=xa in meta_spec)
   1.276 +apply simp
   1.277 +apply (erule bexE)
   1.278 +apply (drule_tac x=xb in meta_spec)
   1.279 +by auto
   1.280 +
   1.281 +lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   1.282 +  unfolding max_strict_def max_weak_def
   1.283 +apply (intro reduction_pairI max_ext_wf)
   1.284 +apply simp
   1.285 +apply (rule max_ext_compat)
   1.286 +by (auto simp: pair_less_def pair_leq_def)
   1.287 +
   1.288 +lemma min_ext_compat:
   1.289 +  assumes "R O S \<subseteq> R"
   1.290 +  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
   1.291 +using assms
   1.292 +apply (auto simp: min_ext_def)
   1.293 +apply (drule_tac x=ya in bspec, assumption)
   1.294 +apply (erule bexE)
   1.295 +apply (drule_tac x=xc in bspec)
   1.296 +apply assumption
   1.297 +by auto
   1.298 +
   1.299 +lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   1.300 +  unfolding min_strict_def min_weak_def
   1.301 +apply (intro reduction_pairI min_ext_wf)
   1.302 +apply simp
   1.303 +apply (rule min_ext_compat)
   1.304 +by (auto simp: pair_less_def pair_leq_def)
   1.305 +
   1.306 +
   1.307 +subsection {* Tool setup *}
   1.308 +
   1.309 +ML_file "Tools/Function/termination.ML"
   1.310 +ML_file "Tools/Function/scnp_solve.ML"
   1.311 +ML_file "Tools/Function/scnp_reconstruct.ML"
   1.312 +ML_file "Tools/Function/fun_cases.ML"
   1.313 +
   1.314 +setup ScnpReconstruct.setup
   1.315 +
   1.316 +ML_val -- "setup inactive"
   1.317 +{*
   1.318 +  Context.theory_map (Function_Common.set_termination_prover
   1.319 +    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
   1.320 +*}
   1.321 +
   1.322 +end