method "sizechange" proves termination of functions; added more infrastructure for termination proofs
authorkrauss
Tue Dec 16 08:46:07 2008 +0100 (2008-12-16)
changeset 29125d41182a8135c
parent 29117 5a79ec2fedfb
child 29126 970d746274d5
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
NEWS
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Library/Multiset.thy
src/HOL/Tools/function_package/decompose.ML
src/HOL/Tools/function_package/descent.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/scnp_reconstruct.ML
src/HOL/Tools/function_package/scnp_solve.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Wellfounded.thy
src/HOL/ex/ExecutableContent.thy
     1.1 --- a/NEWS	Tue Dec 16 00:19:47 2008 +0100
     1.2 +++ b/NEWS	Tue Dec 16 08:46:07 2008 +0100
     1.3 @@ -239,6 +239,9 @@
     1.4  mechanisms may be specified (currently, [SML], [code] or [nbe]).  See
     1.5  further src/HOL/ex/Eval_Examples.thy.
     1.6  
     1.7 +* New method "sizechange" to automate termination proofs using (a
     1.8 +modification of) the size-change principle. Requires SAT solver.
     1.9 +
    1.10  * HOL/Orderings: class "wellorder" moved here, with explicit induction
    1.11  rule "less_induct" as assumption.  For instantiation of "wellorder" by
    1.12  means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/FunDef.thy	Tue Dec 16 00:19:47 2008 +0100
     2.2 +++ b/src/HOL/FunDef.thy	Tue Dec 16 08:46:07 2008 +0100
     2.3 @@ -3,11 +3,13 @@
     2.4      Author:     Alexander Krauss, TU Muenchen
     2.5  *)
     2.6  
     2.7 -header {* General recursive function definitions *}
     2.8 +header {* Function Definitions and Termination Proofs *}
     2.9  
    2.10  theory FunDef
    2.11  imports Wellfounded
    2.12  uses
    2.13 +  "Tools/prop_logic.ML"
    2.14 +  "Tools/sat_solver.ML"
    2.15    ("Tools/function_package/fundef_lib.ML")
    2.16    ("Tools/function_package/fundef_common.ML")
    2.17    ("Tools/function_package/inductive_wrap.ML")
    2.18 @@ -22,9 +24,14 @@
    2.19    ("Tools/function_package/lexicographic_order.ML")
    2.20    ("Tools/function_package/fundef_datatype.ML")
    2.21    ("Tools/function_package/induction_scheme.ML")
    2.22 +  ("Tools/function_package/termination.ML")
    2.23 +  ("Tools/function_package/decompose.ML")
    2.24 +  ("Tools/function_package/descent.ML")
    2.25 +  ("Tools/function_package/scnp_solve.ML")
    2.26 +  ("Tools/function_package/scnp_reconstruct.ML")
    2.27  begin
    2.28  
    2.29 -text {* Definitions with default value. *}
    2.30 +subsection {* Definitions with default value. *}
    2.31  
    2.32  definition
    2.33    THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    2.34 @@ -97,9 +104,6 @@
    2.35    "wf R \<Longrightarrow> wfP (in_rel R)"
    2.36    by (simp add: wfP_def)
    2.37  
    2.38 -inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
    2.39 -where is_measure_trivial: "is_measure f"
    2.40 -
    2.41  use "Tools/function_package/fundef_lib.ML"
    2.42  use "Tools/function_package/fundef_common.ML"
    2.43  use "Tools/function_package/inductive_wrap.ML"
    2.44 @@ -110,19 +114,37 @@
    2.45  use "Tools/function_package/pattern_split.ML"
    2.46  use "Tools/function_package/auto_term.ML"
    2.47  use "Tools/function_package/fundef_package.ML"
    2.48 -use "Tools/function_package/measure_functions.ML"
    2.49 -use "Tools/function_package/lexicographic_order.ML"
    2.50  use "Tools/function_package/fundef_datatype.ML"
    2.51  use "Tools/function_package/induction_scheme.ML"
    2.52  
    2.53  setup {* 
    2.54    FundefPackage.setup 
    2.55 +  #> FundefDatatype.setup
    2.56    #> InductionScheme.setup
    2.57 -  #> MeasureFunctions.setup
    2.58 -  #> LexicographicOrder.setup 
    2.59 -  #> FundefDatatype.setup
    2.60  *}
    2.61  
    2.62 +subsection {* Measure Functions *}
    2.63 +
    2.64 +inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
    2.65 +where is_measure_trivial: "is_measure f"
    2.66 +
    2.67 +use "Tools/function_package/measure_functions.ML"
    2.68 +setup MeasureFunctions.setup
    2.69 +
    2.70 +lemma measure_size[measure_function]: "is_measure size"
    2.71 +by (rule is_measure_trivial)
    2.72 +
    2.73 +lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
    2.74 +by (rule is_measure_trivial)
    2.75 +lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
    2.76 +by (rule is_measure_trivial)
    2.77 +
    2.78 +use "Tools/function_package/lexicographic_order.ML"
    2.79 +setup LexicographicOrder.setup 
    2.80 +
    2.81 +
    2.82 +subsection {* Congruence Rules *}
    2.83 +
    2.84  lemma let_cong [fundef_cong]:
    2.85    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
    2.86    unfolding Let_def by blast
    2.87 @@ -140,17 +162,7 @@
    2.88    "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
    2.89    unfolding o_apply .
    2.90  
    2.91 -subsection {* Setup for termination proofs *}
    2.92 -
    2.93 -text {* Rules for generating measure functions *}
    2.94 -
    2.95 -lemma [measure_function]: "is_measure size"
    2.96 -by (rule is_measure_trivial)
    2.97 -
    2.98 -lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
    2.99 -by (rule is_measure_trivial)
   2.100 -lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   2.101 -by (rule is_measure_trivial)
   2.102 +subsection {* Simp rules for termination proofs *}
   2.103  
   2.104  lemma termination_basic_simps[termination_simp]:
   2.105    "x < (y::nat) \<Longrightarrow> x < y + z" 
   2.106 @@ -166,5 +178,150 @@
   2.107    "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
   2.108  by (induct p) auto
   2.109  
   2.110 +subsection {* Decomposition *}
   2.111 +
   2.112 +lemma less_by_empty: 
   2.113 +  "A = {} \<Longrightarrow> A \<subseteq> B"
   2.114 +and  union_comp_emptyL:
   2.115 +  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
   2.116 +and union_comp_emptyR:
   2.117 +  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
   2.118 +and wf_no_loop: 
   2.119 +  "R O R = {} \<Longrightarrow> wf R"
   2.120 +by (auto simp add: wf_comp_self[of R])
   2.121 +
   2.122 +
   2.123 +subsection {* Reduction Pairs *}
   2.124 +
   2.125 +definition
   2.126 +  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
   2.127 +
   2.128 +lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
   2.129 +unfolding reduction_pair_def by auto
   2.130 +
   2.131 +lemma reduction_pair_lemma:
   2.132 +  assumes rp: "reduction_pair P"
   2.133 +  assumes "R \<subseteq> fst P"
   2.134 +  assumes "S \<subseteq> snd P"
   2.135 +  assumes "wf S"
   2.136 +  shows "wf (R \<union> S)"
   2.137 +proof -
   2.138 +  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
   2.139 +    unfolding reduction_pair_def by auto
   2.140 +  with `wf S` have "wf (fst P \<union> S)" 
   2.141 +    by (auto intro: wf_union_compatible)
   2.142 +  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
   2.143 +  ultimately show ?thesis by (rule wf_subset) 
   2.144 +qed
   2.145 +
   2.146 +definition
   2.147 +  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
   2.148 +
   2.149 +lemma rp_inv_image_rp:
   2.150 +  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
   2.151 +  unfolding reduction_pair_def rp_inv_image_def split_def
   2.152 +  by force
   2.153 +
   2.154 +
   2.155 +subsection {* Concrete orders for SCNP termination proofs *}
   2.156 +
   2.157 +definition "pair_less = less_than <*lex*> less_than"
   2.158 +definition "pair_leq = pair_less^="
   2.159 +definition "max_strict = max_ext pair_less"
   2.160 +definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
   2.161 +definition "min_strict = min_ext pair_less"
   2.162 +definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
   2.163 +
   2.164 +lemma wf_pair_less[simp]: "wf pair_less"
   2.165 +  by (auto simp: pair_less_def)
   2.166 +
   2.167 +text {* Introduction rules for pair_less/pair_leq *}
   2.168 +lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   2.169 +  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   2.170 +  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   2.171 +  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   2.172 +  unfolding pair_leq_def pair_less_def by auto
   2.173 +
   2.174 +text {* Introduction rules for max *}
   2.175 +lemma smax_emptyI: 
   2.176 +  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
   2.177 +  and smax_insertI: 
   2.178 +  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
   2.179 +  and wmax_emptyI: 
   2.180 +  "finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
   2.181 +  and wmax_insertI:
   2.182 +  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
   2.183 +unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
   2.184 +
   2.185 +text {* Introduction rules for min *}
   2.186 +lemma smin_emptyI: 
   2.187 +  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
   2.188 +  and smin_insertI: 
   2.189 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
   2.190 +  and wmin_emptyI: 
   2.191 +  "(X, {}) \<in> min_weak" 
   2.192 +  and wmin_insertI: 
   2.193 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
   2.194 +by (auto simp: min_strict_def min_weak_def min_ext_def)
   2.195 +
   2.196 +text {* Reduction Pairs *}
   2.197 +
   2.198 +lemma max_ext_compat: 
   2.199 +  assumes "S O R \<subseteq> R"
   2.200 +  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
   2.201 +using assms 
   2.202 +apply auto
   2.203 +apply (elim max_ext.cases)
   2.204 +apply rule
   2.205 +apply auto[3]
   2.206 +apply (drule_tac x=xa in meta_spec)
   2.207 +apply simp
   2.208 +apply (erule bexE)
   2.209 +apply (drule_tac x=xb in meta_spec)
   2.210 +by auto
   2.211 +
   2.212 +lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   2.213 +  unfolding max_strict_def max_weak_def 
   2.214 +apply (intro reduction_pairI max_ext_wf)
   2.215 +apply simp
   2.216 +apply (rule max_ext_compat)
   2.217 +by (auto simp: pair_less_def pair_leq_def)
   2.218 +
   2.219 +lemma min_ext_compat: 
   2.220 +  assumes "S O R \<subseteq> R"
   2.221 +  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
   2.222 +using assms 
   2.223 +apply (auto simp: min_ext_def)
   2.224 +apply (drule_tac x=ya in bspec, assumption)
   2.225 +apply (erule bexE)
   2.226 +apply (drule_tac x=xc in bspec)
   2.227 +apply assumption
   2.228 +by auto
   2.229 +
   2.230 +lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   2.231 +  unfolding min_strict_def min_weak_def 
   2.232 +apply (intro reduction_pairI min_ext_wf)
   2.233 +apply simp
   2.234 +apply (rule min_ext_compat)
   2.235 +by (auto simp: pair_less_def pair_leq_def)
   2.236 +
   2.237 +
   2.238 +subsection {* Tool setup *}
   2.239 +
   2.240 +use "Tools/function_package/termination.ML"
   2.241 +use "Tools/function_package/decompose.ML"
   2.242 +use "Tools/function_package/descent.ML"
   2.243 +use "Tools/function_package/scnp_solve.ML"
   2.244 +use "Tools/function_package/scnp_reconstruct.ML"
   2.245 +
   2.246 +setup {* ScnpReconstruct.setup *}
   2.247 +(*
   2.248 +setup {*
   2.249 +  Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
   2.250 +  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
   2.251 +*}
   2.252 +*)
   2.253 +
   2.254 +
   2.255  
   2.256  end
     3.1 --- a/src/HOL/IsaMakefile	Tue Dec 16 00:19:47 2008 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Tue Dec 16 08:46:07 2008 +0100
     3.3 @@ -112,6 +112,8 @@
     3.4    Tools/dseq.ML \
     3.5    Tools/function_package/auto_term.ML \
     3.6    Tools/function_package/context_tree.ML \
     3.7 +  Tools/function_package/decompose.ML \
     3.8 +  Tools/function_package/descent.ML \
     3.9    Tools/function_package/fundef_common.ML \
    3.10    Tools/function_package/fundef_core.ML \
    3.11    Tools/function_package/fundef_datatype.ML \
    3.12 @@ -123,8 +125,11 @@
    3.13    Tools/function_package/measure_functions.ML \
    3.14    Tools/function_package/mutual.ML \
    3.15    Tools/function_package/pattern_split.ML \
    3.16 +  Tools/function_package/scnp_reconstruct.ML \
    3.17 +  Tools/function_package/scnp_solve.ML \
    3.18    Tools/function_package/size.ML \
    3.19    Tools/function_package/sum_tree.ML \
    3.20 +  Tools/function_package/termination.ML \
    3.21    Tools/hologic.ML \
    3.22    Tools/inductive_codegen.ML \
    3.23    Tools/inductive_package.ML \
     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Dec 16 00:19:47 2008 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Tue Dec 16 08:46:07 2008 +0100
     4.3 @@ -1481,4 +1481,155 @@
     4.4    @{term "{#x+x|x:#M. x<c#}"}.
     4.5  *}
     4.6  
     4.7 +
     4.8 +subsection {* Termination proofs with multiset orders *}
     4.9 +
    4.10 +lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
    4.11 +  and multi_member_this: "x \<in># {# x #} + XS"
    4.12 +  and multi_member_last: "x \<in># {# x #}"
    4.13 +  by auto
    4.14 +
    4.15 +definition "ms_strict = mult pair_less"
    4.16 +definition "ms_weak = ms_strict \<union> Id"
    4.17 +
    4.18 +lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
    4.19 +unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
    4.20 +by (auto intro: wf_mult1 wf_trancl simp: mult_def)
    4.21 +
    4.22 +lemma smsI:
    4.23 +  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
    4.24 +  unfolding ms_strict_def
    4.25 +by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
    4.26 +
    4.27 +lemma wmsI:
    4.28 +  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
    4.29 +  \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
    4.30 +unfolding ms_weak_def ms_strict_def
    4.31 +by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
    4.32 +
    4.33 +inductive pw_leq
    4.34 +where
    4.35 +  pw_leq_empty: "pw_leq {#} {#}"
    4.36 +| pw_leq_step:  "\<lbrakk>(x,y) \<in> pair_leq; pw_leq X Y \<rbrakk> \<Longrightarrow> pw_leq ({#x#} + X) ({#y#} + Y)"
    4.37 +
    4.38 +lemma pw_leq_lstep:
    4.39 +  "(x, y) \<in> pair_leq \<Longrightarrow> pw_leq {#x#} {#y#}"
    4.40 +by (drule pw_leq_step) (rule pw_leq_empty, simp)
    4.41 +
    4.42 +lemma pw_leq_split:
    4.43 +  assumes "pw_leq X Y"
    4.44 +  shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
    4.45 +  using assms
    4.46 +proof (induct)
    4.47 +  case pw_leq_empty thus ?case by auto
    4.48 +next
    4.49 +  case (pw_leq_step x y X Y)
    4.50 +  then obtain A B Z where
    4.51 +    [simp]: "X = A + Z" "Y = B + Z" 
    4.52 +      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})" 
    4.53 +    by auto
    4.54 +  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less" 
    4.55 +    unfolding pair_leq_def by auto
    4.56 +  thus ?case
    4.57 +  proof
    4.58 +    assume [simp]: "x = y"
    4.59 +    have
    4.60 +      "{#x#} + X = A + ({#y#}+Z) 
    4.61 +      \<and> {#y#} + Y = B + ({#y#}+Z)
    4.62 +      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
    4.63 +      by (auto simp: add_ac)
    4.64 +    thus ?case by (intro exI)
    4.65 +  next
    4.66 +    assume A: "(x, y) \<in> pair_less"
    4.67 +    let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
    4.68 +    have "{#x#} + X = ?A' + Z"
    4.69 +      "{#y#} + Y = ?B' + Z"
    4.70 +      by (auto simp add: add_ac)
    4.71 +    moreover have 
    4.72 +      "(set_of ?A', set_of ?B') \<in> max_strict"
    4.73 +      using 1 A unfolding max_strict_def 
    4.74 +      by (auto elim!: max_ext.cases)
    4.75 +    ultimately show ?thesis by blast
    4.76 +  qed
    4.77 +qed
    4.78 +
    4.79 +lemma 
    4.80 +  assumes pwleq: "pw_leq Z Z'"
    4.81 +  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
    4.82 +  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
    4.83 +  and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
    4.84 +proof -
    4.85 +  from pw_leq_split[OF pwleq] 
    4.86 +  obtain A' B' Z''
    4.87 +    where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
    4.88 +    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
    4.89 +    by blast
    4.90 +  {
    4.91 +    assume max: "(set_of A, set_of B) \<in> max_strict"
    4.92 +    from mx_or_empty
    4.93 +    have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
    4.94 +    proof
    4.95 +      assume max': "(set_of A', set_of B') \<in> max_strict"
    4.96 +      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
    4.97 +        by (auto simp: max_strict_def intro: max_ext_additive)
    4.98 +      thus ?thesis by (rule smsI) 
    4.99 +    next
   4.100 +      assume [simp]: "A' = {#} \<and> B' = {#}"
   4.101 +      show ?thesis by (rule smsI) (auto intro: max)
   4.102 +    qed
   4.103 +    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
   4.104 +    thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
   4.105 +  }
   4.106 +  from mx_or_empty
   4.107 +  have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
   4.108 +  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
   4.109 +qed
   4.110 +
   4.111 +lemma empty_idemp: "{#} + x = x" "x + {#} = x"
   4.112 +and nonempty_plus: "{# x #} + rs \<noteq> {#}"
   4.113 +and nonempty_single: "{# x #} \<noteq> {#}"
   4.114 +by auto
   4.115 +
   4.116 +setup {*
   4.117 +let
   4.118 +  fun msetT T = Type ("Multiset.multiset", [T]);
   4.119 +
   4.120 +  fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
   4.121 +    | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
   4.122 +    | mk_mset T (x :: xs) =
   4.123 +          Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
   4.124 +                mk_mset T [x] $ mk_mset T xs
   4.125 +
   4.126 +  fun mset_member_tac m i =
   4.127 +      (if m <= 0 then
   4.128 +           rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
   4.129 +       else
   4.130 +           rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i)
   4.131 +
   4.132 +  val mset_nonempty_tac =
   4.133 +      rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
   4.134 +
   4.135 +  val regroup_munion_conv =
   4.136 +      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
   4.137 +        (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
   4.138 +
   4.139 +  fun unfold_pwleq_tac i =
   4.140 +    (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
   4.141 +      ORELSE (rtac @{thm pw_leq_lstep} i)
   4.142 +      ORELSE (rtac @{thm pw_leq_empty} i)
   4.143 +
   4.144 +  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
   4.145 +                      @{thm Un_insert_left}, @{thm Un_empty_left}]
   4.146 +in
   4.147 +  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset 
   4.148 +  {
   4.149 +    msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
   4.150 +    mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
   4.151 +    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
   4.152 +    smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
   4.153 +    reduction_pair=@{thm ms_reduction_pair}
   4.154 +  })
   4.155  end
   4.156 +*}
   4.157 +
   4.158 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/function_package/decompose.ML	Tue Dec 16 08:46:07 2008 +0100
     5.3 @@ -0,0 +1,105 @@
     5.4 +(*  Title:       HOL/Tools/function_package/decompose.ML
     5.5 +    Author:      Alexander Krauss, TU Muenchen
     5.6 +
     5.7 +Graph decomposition using "Shallow Dependency Pairs".
     5.8 +*)
     5.9 +
    5.10 +signature DECOMPOSE =
    5.11 +sig
    5.12 +
    5.13 +  val derive_chains : Proof.context -> tactic
    5.14 +                      -> (Termination.data -> int -> tactic)
    5.15 +                      -> Termination.data -> int -> tactic
    5.16 +
    5.17 +  val decompose_tac : Proof.context -> tactic
    5.18 +                      -> Termination.ttac
    5.19 +
    5.20 +end
    5.21 +
    5.22 +structure Decompose : DECOMPOSE =
    5.23 +struct
    5.24 +
    5.25 +structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
    5.26 +
    5.27 +
    5.28 +fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
    5.29 +  let
    5.30 +      val thy = ProofContext.theory_of ctxt
    5.31 +
    5.32 +      fun prove_chain c1 c2 D =
    5.33 +          if is_some (Termination.get_chain D c1 c2) then D else
    5.34 +          let
    5.35 +            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
    5.36 +                                      Const (@{const_name "{}"}, fastype_of c1))
    5.37 +                       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    5.38 +
    5.39 +            val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
    5.40 +                          FundefLib.Solved thm => SOME thm
    5.41 +                        | _ => NONE
    5.42 +          in
    5.43 +            Termination.note_chain c1 c2 chain D
    5.44 +          end
    5.45 +  in
    5.46 +    cont (fold_product prove_chain cs cs D) i
    5.47 +  end)
    5.48 +
    5.49 +
    5.50 +fun mk_dgraph D cs =
    5.51 +    TermGraph.empty
    5.52 +    |> fold (fn c => TermGraph.new_node (c,())) cs
    5.53 +    |> fold_product (fn c1 => fn c2 =>
    5.54 +         if is_none (Termination.get_chain D c1 c2 |> the_default NONE)
    5.55 +         then TermGraph.add_edge (c1, c2) else I)
    5.56 +       cs cs
    5.57 +
    5.58 +
    5.59 +fun ucomp_empty_tac T =
    5.60 +    REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
    5.61 +                    ORELSE' rtac @{thm union_comp_emptyL}
    5.62 +                    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
    5.63 +
    5.64 +fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) =>
    5.65 +   let
    5.66 +     val is = map (fn c => find_index (curry op aconv c) cs') cs
    5.67 +   in
    5.68 +     CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
    5.69 +   end)
    5.70 +
    5.71 +
    5.72 +fun solve_trivial_tac D = Termination.CALLS
    5.73 +(fn ([c], i) =>
    5.74 +    (case Termination.get_chain D c c of
    5.75 +       SOME (SOME thm) => rtac @{thm wf_no_loop} i
    5.76 +                          THEN rtac thm i
    5.77 +     | _ => no_tac)
    5.78 +  | _ => no_tac)
    5.79 +
    5.80 +fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
    5.81 +    let
    5.82 +      val G = mk_dgraph D cs
    5.83 +      val sccs = TermGraph.strong_conn G
    5.84 +
    5.85 +      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
    5.86 +        | split (SCC::rest) i =
    5.87 +            regroup_calls_tac SCC i
    5.88 +            THEN rtac @{thm wf_union_compatible} i
    5.89 +            THEN rtac @{thm less_by_empty} (i + 2)
    5.90 +            THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2)
    5.91 +            THEN split rest (i + 1)
    5.92 +            THEN (solve_trivial_tac D i ORELSE cont D i)
    5.93 +    in
    5.94 +      if length sccs > 1 then split sccs i
    5.95 +      else solve_trivial_tac D i ORELSE err_cont D i
    5.96 +    end)
    5.97 +
    5.98 +fun decompose_tac ctxt chain_tac cont err_cont =
    5.99 +    derive_chains ctxt chain_tac
   5.100 +    (decompose_tac' ctxt cont err_cont)
   5.101 +
   5.102 +fun auto_decompose_tac ctxt =
   5.103 +    Termination.TERMINATION ctxt
   5.104 +      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
   5.105 +                     (K (K all_tac)) (K (K no_tac)))
   5.106 +
   5.107 +
   5.108 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/function_package/descent.ML	Tue Dec 16 08:46:07 2008 +0100
     6.3 @@ -0,0 +1,44 @@
     6.4 +(*  Title:       HOL/Tools/function_package/descent.ML
     6.5 +    Author:      Alexander Krauss, TU Muenchen
     6.6 +
     6.7 +Descent proofs for termination
     6.8 +*)
     6.9 +
    6.10 +
    6.11 +signature DESCENT =
    6.12 +sig
    6.13 +
    6.14 +  val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
    6.15 +                    -> Termination.data -> int -> tactic
    6.16 +
    6.17 +  val derive_all  : Proof.context -> tactic -> (Termination.data -> int -> tactic)
    6.18 +                    -> Termination.data -> int -> tactic
    6.19 +
    6.20 +end
    6.21 +
    6.22 +
    6.23 +structure Descent : DESCENT =
    6.24 +struct
    6.25 +
    6.26 +fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
    6.27 +  let
    6.28 +    val thy = ProofContext.theory_of ctxt
    6.29 +    val measures_of = Termination.get_measures D
    6.30 +
    6.31 +    fun derive c D =
    6.32 +      let
    6.33 +        val (_, p, _, q, _, _) = Termination.dest_call D c
    6.34 +      in
    6.35 +        if diag andalso p = q
    6.36 +        then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
    6.37 +        else fold_product (Termination.derive_descent thy tac c)
    6.38 +               (measures_of p) (measures_of q) D
    6.39 +      end
    6.40 +  in
    6.41 +    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
    6.42 +  end)
    6.43 +
    6.44 +val derive_diag = gen_descent true
    6.45 +val derive_all = gen_descent false
    6.46 +
    6.47 +end
     7.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 00:19:47 2008 +0100
     7.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 08:46:07 2008 +0100
     7.3 @@ -130,4 +130,50 @@
     7.4      | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
     7.5  
     7.6  
     7.7 +fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
     7.8 +    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
     7.9 +  | dest_binop_list _ t = [ t ]
    7.10 +
    7.11 +
    7.12 +(* separate two parts in a +-expression:
    7.13 +   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
    7.14 +
    7.15 +   Here, + can be any binary operation that is AC.
    7.16 +
    7.17 +   cn - The name of the binop-constructor (e.g. @{const_name "op Un"})
    7.18 +   ac - the AC rewrite rules for cn
    7.19 +   is - the list of indices of the expressions that should become the first part
    7.20 +        (e.g. [0,1,3] in the above example)
    7.21 +*)
    7.22 +
    7.23 +fun regroup_conv neu cn ac is ct =
    7.24 + let
    7.25 +   val mk = HOLogic.mk_binop cn
    7.26 +   val t = term_of ct
    7.27 +   val xs = dest_binop_list cn t
    7.28 +   val js = 0 upto (length xs) - 1 \\ is
    7.29 +   val ty = fastype_of t
    7.30 +   val thy = theory_of_cterm ct
    7.31 + in
    7.32 +   Goal.prove_internal []
    7.33 +     (cterm_of thy
    7.34 +       (Logic.mk_equals (t,
    7.35 +          if is = []
    7.36 +          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
    7.37 +          else if js = []
    7.38 +            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
    7.39 +            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
    7.40 +     (K (MetaSimplifier.rewrite_goals_tac ac
    7.41 +         THEN rtac Drule.reflexive_thm 1))
    7.42 + end
    7.43 +
    7.44 +(* instance for unions *)
    7.45 +fun regroup_union_conv t =
    7.46 +    regroup_conv (@{const_name "{}"})
    7.47 +                  @{const_name "op Un"}
    7.48 +       (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
    7.49 +                                          @{thms "Un_empty_right"} @
    7.50 +                                          @{thms "Un_empty_left"})) t
    7.51 +
    7.52 +
    7.53  end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Tue Dec 16 08:46:07 2008 +0100
     8.3 @@ -0,0 +1,426 @@
     8.4 +(*  Title:       HOL/Tools/function_package/scnp_reconstruct.ML
     8.5 +    Author:      Armin Heller, TU Muenchen
     8.6 +    Author:      Alexander Krauss, TU Muenchen
     8.7 +
     8.8 +Proof reconstruction for SCNP
     8.9 +*)
    8.10 +
    8.11 +signature SCNP_RECONSTRUCT =
    8.12 +sig
    8.13 +
    8.14 +  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
    8.15 +
    8.16 +  val setup : theory -> theory
    8.17 +
    8.18 +  datatype multiset_setup =
    8.19 +    Multiset of
    8.20 +    {
    8.21 +     msetT : typ -> typ,
    8.22 +     mk_mset : typ -> term list -> term,
    8.23 +     mset_regroup_conv : int list -> conv,
    8.24 +     mset_member_tac : int -> int -> tactic,
    8.25 +     mset_nonempty_tac : int -> tactic,
    8.26 +     mset_pwleq_tac : int -> tactic,
    8.27 +     set_of_simps : thm list,
    8.28 +     smsI' : thm,
    8.29 +     wmsI2'' : thm,
    8.30 +     wmsI1 : thm,
    8.31 +     reduction_pair : thm
    8.32 +    }
    8.33 +
    8.34 +
    8.35 +  val multiset_setup : multiset_setup -> theory -> theory
    8.36 +
    8.37 +end
    8.38 +
    8.39 +structure ScnpReconstruct : SCNP_RECONSTRUCT =
    8.40 +struct
    8.41 +
    8.42 +val PROFILE = FundefCommon.PROFILE
    8.43 +fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
    8.44 +
    8.45 +open ScnpSolve
    8.46 +
    8.47 +val natT = HOLogic.natT
    8.48 +val nat_pairT = HOLogic.mk_prodT (natT, natT)
    8.49 +
    8.50 +(* Theory dependencies *)
    8.51 +
    8.52 +datatype multiset_setup =
    8.53 +  Multiset of
    8.54 +  {
    8.55 +   msetT : typ -> typ,
    8.56 +   mk_mset : typ -> term list -> term,
    8.57 +   mset_regroup_conv : int list -> conv,
    8.58 +   mset_member_tac : int -> int -> tactic,
    8.59 +   mset_nonempty_tac : int -> tactic,
    8.60 +   mset_pwleq_tac : int -> tactic,
    8.61 +   set_of_simps : thm list,
    8.62 +   smsI' : thm,
    8.63 +   wmsI2'' : thm,
    8.64 +   wmsI1 : thm,
    8.65 +   reduction_pair : thm
    8.66 +  }
    8.67 +
    8.68 +structure MultisetSetup = TheoryDataFun
    8.69 +(
    8.70 +  type T = multiset_setup option
    8.71 +  val empty = NONE
    8.72 +  val copy = I;
    8.73 +  val extend = I;
    8.74 +  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
    8.75 +)
    8.76 +
    8.77 +val multiset_setup = MultisetSetup.put o SOME
    8.78 +
    8.79 +fun undef x = error "undef"
    8.80 +fun get_multiset_setup thy = MultisetSetup.get thy
    8.81 +  |> the_default (Multiset
    8.82 +{ msetT = undef, mk_mset=undef,
    8.83 +  mset_regroup_conv=undef, mset_member_tac = undef,
    8.84 +  mset_nonempty_tac = undef, mset_pwleq_tac = undef,
    8.85 +  set_of_simps = [],reduction_pair = refl,
    8.86 +  smsI'=refl, wmsI2''=refl, wmsI1=refl })
    8.87 +
    8.88 +fun order_rpair _ MAX = @{thm max_rpair_set}
    8.89 +  | order_rpair msrp MS  = msrp
    8.90 +  | order_rpair _ MIN = @{thm min_rpair_set}
    8.91 +
    8.92 +fun ord_intros_max true =
    8.93 +    (@{thm smax_emptyI}, @{thm smax_insertI})
    8.94 +  | ord_intros_max false =
    8.95 +    (@{thm wmax_emptyI}, @{thm wmax_insertI})
    8.96 +fun ord_intros_min true =
    8.97 +    (@{thm smin_emptyI}, @{thm smin_insertI})
    8.98 +  | ord_intros_min false =
    8.99 +    (@{thm wmin_emptyI}, @{thm wmin_insertI})
   8.100 +
   8.101 +fun gen_probl D cs =
   8.102 +  let
   8.103 +    val n = Termination.get_num_points D
   8.104 +    val arity = length o Termination.get_measures D
   8.105 +    fun measure p i = nth (Termination.get_measures D p) i
   8.106 +
   8.107 +    fun mk_graph c =
   8.108 +      let
   8.109 +        val (_, p, _, q, _, _) = Termination.dest_call D c
   8.110 +
   8.111 +        fun add_edge i j =
   8.112 +          case Termination.get_descent D c (measure p i) (measure q j)
   8.113 +           of SOME (Termination.Less _) => cons (i, GTR, j)
   8.114 +            | SOME (Termination.LessEq _) => cons (i, GEQ, j)
   8.115 +            | _ => I
   8.116 +
   8.117 +        val edges =
   8.118 +          fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
   8.119 +      in
   8.120 +        G (p, q, edges)
   8.121 +      end
   8.122 +  in
   8.123 +    GP (map arity (0 upto n - 1), map mk_graph cs)
   8.124 +  end
   8.125 +
   8.126 +(* General reduction pair application *)
   8.127 +fun rem_inv_img ctxt =
   8.128 +  let
   8.129 +    val unfold_tac = LocalDefs.unfold_tac ctxt
   8.130 +  in
   8.131 +    rtac @{thm subsetI} 1
   8.132 +    THEN etac @{thm CollectE} 1
   8.133 +    THEN REPEAT (etac @{thm exE} 1)
   8.134 +    THEN unfold_tac @{thms inv_image_def}
   8.135 +    THEN rtac @{thm CollectI} 1
   8.136 +    THEN etac @{thm conjE} 1
   8.137 +    THEN etac @{thm ssubst} 1
   8.138 +    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
   8.139 +                     @ @{thms Sum_Type.sum_cases})
   8.140 +  end
   8.141 +
   8.142 +(* Sets *)
   8.143 +
   8.144 +val setT = HOLogic.mk_setT
   8.145 +
   8.146 +fun mk_set T [] = Const (@{const_name "{}"}, setT T)
   8.147 +  | mk_set T (x :: xs) =
   8.148 +      Const (@{const_name insert}, T --> setT T --> setT T) $
   8.149 +            x $ mk_set T xs
   8.150 +
   8.151 +fun set_member_tac m i =
   8.152 +  if m = 0 then rtac @{thm insertI1} i
   8.153 +  else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
   8.154 +
   8.155 +val set_nonempty_tac = rtac @{thm insert_not_empty}
   8.156 +
   8.157 +fun set_finite_tac i =
   8.158 +  rtac @{thm finite.emptyI} i
   8.159 +  ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
   8.160 +
   8.161 +
   8.162 +(* Reconstruction *)
   8.163 +
   8.164 +fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
   8.165 +  let
   8.166 +    val thy = ProofContext.theory_of ctxt
   8.167 +    val Multiset
   8.168 +          { msetT, mk_mset,
   8.169 +            mset_regroup_conv, mset_member_tac,
   8.170 +            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
   8.171 +            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
   8.172 +        = get_multiset_setup thy
   8.173 +
   8.174 +    fun measure_fn p = nth (Termination.get_measures D p)
   8.175 +
   8.176 +    fun get_desc_thm cidx m1 m2 bStrict =
   8.177 +      case Termination.get_descent D (nth cs cidx) m1 m2
   8.178 +       of SOME (Termination.Less thm) =>
   8.179 +          if bStrict then thm
   8.180 +          else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
   8.181 +        | SOME (Termination.LessEq (thm, _))  =>
   8.182 +          if not bStrict then thm
   8.183 +          else sys_error "get_desc_thm"
   8.184 +        | _ => sys_error "get_desc_thm"
   8.185 +
   8.186 +    val (label, lev, sl, covering) = certificate
   8.187 +
   8.188 +    fun prove_lev strict g =
   8.189 +      let
   8.190 +        val G (p, q, el) = nth gs g
   8.191 +
   8.192 +        fun less_proof strict (j, b) (i, a) =
   8.193 +          let
   8.194 +            val tag_flag = b < a orelse (not strict andalso b <= a)
   8.195 +
   8.196 +            val stored_thm =
   8.197 +              get_desc_thm g (measure_fn p i) (measure_fn q j)
   8.198 +                             (not tag_flag)
   8.199 +              |> Conv.fconv_rule (Thm.beta_conversion true)
   8.200 +
   8.201 +            val rule = if strict
   8.202 +              then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
   8.203 +              else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
   8.204 +          in
   8.205 +            rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
   8.206 +            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
   8.207 +          end
   8.208 +
   8.209 +        fun steps_tac MAX strict lq lp =
   8.210 +          let
   8.211 +            val (empty, step) = ord_intros_max strict
   8.212 +          in
   8.213 +            if length lq = 0
   8.214 +            then rtac empty 1 THEN set_finite_tac 1
   8.215 +                 THEN (if strict then set_nonempty_tac 1 else all_tac)
   8.216 +            else
   8.217 +              let
   8.218 +                val (j, b) :: rest = lq
   8.219 +                val (i, a) = the (covering g strict j)
   8.220 +                fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
   8.221 +                val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
   8.222 +              in
   8.223 +                rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
   8.224 +              end
   8.225 +          end
   8.226 +          | steps_tac MIN strict lq lp =
   8.227 +          let
   8.228 +            val (empty, step) = ord_intros_min strict
   8.229 +          in
   8.230 +            if length lp = 0
   8.231 +            then rtac empty 1
   8.232 +                 THEN (if strict then set_nonempty_tac 1 else all_tac)
   8.233 +            else
   8.234 +              let
   8.235 +                val (i, a) :: rest = lp
   8.236 +                val (j, b) = the (covering g strict i)
   8.237 +                fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
   8.238 +                val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
   8.239 +              in
   8.240 +                rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
   8.241 +              end
   8.242 +          end
   8.243 +          | steps_tac MS strict lq lp =
   8.244 +          let
   8.245 +            fun get_str_cover (j, b) =
   8.246 +              if is_some (covering g true j) then SOME (j, b) else NONE
   8.247 +            fun get_wk_cover (j, b) = the (covering g false j)
   8.248 +
   8.249 +            val qs = lq \\ map_filter get_str_cover lq
   8.250 +            val ps = map get_wk_cover qs
   8.251 +
   8.252 +            fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
   8.253 +            val iqs = indices lq qs
   8.254 +            val ips = indices lp ps
   8.255 +
   8.256 +            local open Conv in
   8.257 +            fun t_conv a C =
   8.258 +              params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
   8.259 +            val goal_rewrite =
   8.260 +                t_conv arg1_conv (mset_regroup_conv iqs)
   8.261 +                then_conv t_conv arg_conv (mset_regroup_conv ips)
   8.262 +            end
   8.263 +          in
   8.264 +            CONVERSION goal_rewrite 1
   8.265 +            THEN (if strict then rtac smsI' 1
   8.266 +                  else if qs = lq then rtac wmsI2'' 1
   8.267 +                  else rtac wmsI1 1)
   8.268 +            THEN mset_pwleq_tac 1
   8.269 +            THEN EVERY (map2 (less_proof false) qs ps)
   8.270 +            THEN (if strict orelse qs <> lq
   8.271 +                  then LocalDefs.unfold_tac ctxt set_of_simps
   8.272 +                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
   8.273 +                  else all_tac)
   8.274 +          end
   8.275 +      in
   8.276 +        rem_inv_img ctxt
   8.277 +        THEN steps_tac label strict (nth lev q) (nth lev p)
   8.278 +      end
   8.279 +
   8.280 +    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
   8.281 +
   8.282 +    fun tag_pair p (i, tag) =
   8.283 +      HOLogic.pair_const natT natT $
   8.284 +        (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
   8.285 +
   8.286 +    fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
   8.287 +                           mk_set nat_pairT (map (tag_pair p) lm))
   8.288 +
   8.289 +    val level_mapping =
   8.290 +      map_index pt_lev lev
   8.291 +        |> Termination.mk_sumcases D (setT nat_pairT)
   8.292 +        |> cterm_of thy
   8.293 +    in
   8.294 +      PROFILE "Proof Reconstruction"
   8.295 +        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
   8.296 +         THEN (rtac @{thm reduction_pair_lemma} 1)
   8.297 +         THEN (rtac @{thm rp_inv_image_rp} 1)
   8.298 +         THEN (rtac (order_rpair ms_rp label) 1)
   8.299 +         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
   8.300 +         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
   8.301 +         THEN LocalDefs.unfold_tac ctxt
   8.302 +           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
   8.303 +         THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
   8.304 +         THEN EVERY (map (prove_lev true) sl)
   8.305 +         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
   8.306 +    end
   8.307 +
   8.308 +
   8.309 +
   8.310 +local open Termination in
   8.311 +fun print_cell (SOME (Less _)) = "<"
   8.312 +  | print_cell (SOME (LessEq _)) = "\<le>"
   8.313 +  | print_cell (SOME (None _)) = "-"
   8.314 +  | print_cell (SOME (False _)) = "-"
   8.315 +  | print_cell (NONE) = "?"
   8.316 +
   8.317 +fun print_error ctxt D = CALLS (fn (cs, i) =>
   8.318 +  let
   8.319 +    val np = get_num_points D
   8.320 +    val ms = map (get_measures D) (0 upto np - 1)
   8.321 +    val tys = map (get_types D) (0 upto np - 1)
   8.322 +    fun index xs = (1 upto length xs) ~~ xs
   8.323 +    fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
   8.324 +    val ims = index (map index ms)
   8.325 +    val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
   8.326 +    fun print_call (k, c) =
   8.327 +      let
   8.328 +        val (_, p, _, q, _, _) = dest_call D c
   8.329 +        val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
   8.330 +                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
   8.331 +        val caller_ms = nth ms p
   8.332 +        val callee_ms = nth ms q
   8.333 +        val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
   8.334 +        fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
   8.335 +        val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
   8.336 +                                        " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
   8.337 +                                ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
   8.338 +      in
   8.339 +        true
   8.340 +      end
   8.341 +    fun list_call (k, c) =
   8.342 +      let
   8.343 +        val (_, p, _, q, _, _) = dest_call D c
   8.344 +        val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
   8.345 +                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
   8.346 +                                (Syntax.string_of_term ctxt c))
   8.347 +      in true end
   8.348 +    val _ = forall list_call ((1 upto length cs) ~~ cs)
   8.349 +    val _ = forall print_call ((1 upto length cs) ~~ cs)
   8.350 +  in
   8.351 +    all_tac
   8.352 +  end)
   8.353 +end
   8.354 +
   8.355 +
   8.356 +fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
   8.357 +  let
   8.358 +    val gp = gen_probl D cs
   8.359 +(*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
   8.360 +    val certificate = generate_certificate use_tags orders gp
   8.361 +(*    val _ = TRACE ("Certificate: " ^ makestring certificate)*)
   8.362 +
   8.363 +    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
   8.364 +    in
   8.365 +    case certificate
   8.366 +     of NONE => err_cont D i
   8.367 +      | SOME cert =>
   8.368 +        if not ms_configured andalso #1 cert = MS
   8.369 +        then err_cont D i
   8.370 +        else SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
   8.371 +             THEN (rtac @{thm wf_empty} i ORELSE cont D i)
   8.372 +  end)
   8.373 +
   8.374 +fun decomp_scnp_tac orders autom_tac ctxt err_cont =
   8.375 +  let
   8.376 +    open Termination
   8.377 +    val derive_diag = Descent.derive_diag ctxt autom_tac
   8.378 +    val derive_all = Descent.derive_all ctxt autom_tac
   8.379 +    val decompose = Decompose.decompose_tac ctxt autom_tac
   8.380 +    val scnp_no_tags = single_scnp_tac false orders ctxt
   8.381 +    val scnp_full = single_scnp_tac true orders ctxt
   8.382 +
   8.383 +    fun first_round c e =
   8.384 +        derive_diag (REPEAT scnp_no_tags c e)
   8.385 +
   8.386 +    val second_round =
   8.387 +        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
   8.388 +
   8.389 +    val third_round =
   8.390 +        derive_all oo
   8.391 +        REPEAT (fn c => fn e =>
   8.392 +          scnp_full (decompose c c) e)
   8.393 +
   8.394 +    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
   8.395 +
   8.396 +    val strategy = Then (Then first_round second_round) third_round
   8.397 +
   8.398 +  in
   8.399 +    TERMINATION ctxt (strategy err_cont err_cont)
   8.400 +  end
   8.401 +
   8.402 +fun decomp_scnp orders ctxt =
   8.403 +  let
   8.404 +    val extra_simps = FundefCommon.TerminationSimps.get ctxt
   8.405 +    val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   8.406 +  in
   8.407 +    Method.SIMPLE_METHOD
   8.408 +      (TRY (FundefCommon.apply_termination_rule ctxt 1)
   8.409 +       THEN TRY Termination.wf_union_tac
   8.410 +       THEN
   8.411 +         (rtac @{thm wf_empty} 1
   8.412 +          ORELSE decomp_scnp_tac orders autom_tac ctxt (print_error ctxt) 1))
   8.413 +  end
   8.414 +
   8.415 +
   8.416 +(* Method setup *)
   8.417 +
   8.418 +val orders =
   8.419 +  (Scan.repeat1
   8.420 +    ((Args.$$$ "max" >> K MAX) ||
   8.421 +     (Args.$$$ "min" >> K MIN) ||
   8.422 +     (Args.$$$ "ms" >> K MS))
   8.423 +  || Scan.succeed [MAX, MS, MIN])
   8.424 +
   8.425 +val setup = Method.add_method
   8.426 +  ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
   8.427 +   "termination prover with graph decomposition and the NP subset of size change termination")
   8.428 +
   8.429 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/function_package/scnp_solve.ML	Tue Dec 16 08:46:07 2008 +0100
     9.3 @@ -0,0 +1,257 @@
     9.4 +(*  Title:       HOL/Tools/function_package/scnp_solve.ML
     9.5 +    Author:      Armin Heller, TU Muenchen
     9.6 +    Author:      Alexander Krauss, TU Muenchen
     9.7 +
     9.8 +Generate certificates for SCNP using a SAT solver
     9.9 +*)
    9.10 +
    9.11 +
    9.12 +signature SCNP_SOLVE =
    9.13 +sig
    9.14 +
    9.15 +  datatype edge = GTR | GEQ
    9.16 +  datatype graph = G of int * int * (int * edge * int) list
    9.17 +  datatype graph_problem = GP of int list * graph list
    9.18 +
    9.19 +  datatype label = MIN | MAX | MS
    9.20 +
    9.21 +  type certificate =
    9.22 +    label                   (* which order *)
    9.23 +    * (int * int) list list (* (multi)sets *)
    9.24 +    * int list              (* strictly ordered calls *)
    9.25 +    * (int -> bool -> int -> (int * int) option) (* covering function *)
    9.26 +
    9.27 +  val generate_certificate : bool -> label list -> graph_problem -> certificate option
    9.28 +
    9.29 +  val solver : string ref
    9.30 +end
    9.31 +
    9.32 +structure ScnpSolve : SCNP_SOLVE =
    9.33 +struct
    9.34 +
    9.35 +(** Graph problems **)
    9.36 +
    9.37 +datatype edge = GTR | GEQ ;
    9.38 +datatype graph = G of int * int * (int * edge * int) list ;
    9.39 +datatype graph_problem = GP of int list * graph list ;
    9.40 +
    9.41 +datatype label = MIN | MAX | MS ;
    9.42 +type certificate =
    9.43 +  label
    9.44 +  * (int * int) list list
    9.45 +  * int list
    9.46 +  * (int -> bool -> int -> (int * int) option)
    9.47 +
    9.48 +fun graph_at (GP (_, gs), i) = nth gs i ;
    9.49 +fun num_prog_pts (GP (arities, _)) = length arities ;
    9.50 +fun num_graphs (GP (_, gs)) = length gs ;
    9.51 +fun arity (GP (arities, gl)) i = nth arities i ;
    9.52 +fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1
    9.53 +
    9.54 +
    9.55 +(** Propositional formulas **)
    9.56 +
    9.57 +val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
    9.58 +val BoolVar = PropLogic.BoolVar
    9.59 +fun Implies (p, q) = Or (Not p, q)
    9.60 +fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
    9.61 +val all = PropLogic.all
    9.62 +
    9.63 +(* finite indexed quantifiers:
    9.64 +
    9.65 +iforall n f   <==>      /\
    9.66 +                       /  \  f i
    9.67 +                      0<=i<n
    9.68 + *)
    9.69 +fun iforall n f = all (map f (0 upto n - 1))
    9.70 +fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
    9.71 +fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
    9.72 +
    9.73 +fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
    9.74 +fun exactly_one n f = iexists n (the_one f n)
    9.75 +
    9.76 +(* SAT solving *)
    9.77 +val solver = ref "auto";
    9.78 +fun sat_solver x =
    9.79 +  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
    9.80 +
    9.81 +(* "Virtual constructors" for various propositional variables *)
    9.82 +fun var_constrs (gp as GP (arities, gl)) =
    9.83 +  let
    9.84 +    val n = Int.max (num_graphs gp, num_prog_pts gp)
    9.85 +    val k = foldl Int.max 1 arities
    9.86 +
    9.87 +    (* Injective, provided  a < 8, x < n, and i < k. *)
    9.88 +    fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
    9.89 +
    9.90 +    fun ES (g, i, j) = BoolVar (prod 0 g i j)
    9.91 +    fun EW (g, i, j) = BoolVar (prod 1 g i j)
    9.92 +    fun WEAK g       = BoolVar (prod 2 g 0 0)
    9.93 +    fun STRICT g     = BoolVar (prod 3 g 0 0)
    9.94 +    fun P (p, i)     = BoolVar (prod 4 p i 0)
    9.95 +    fun GAM (g, i, j)= BoolVar (prod 5 g i j)
    9.96 +    fun EPS (g, i)   = BoolVar (prod 6 g i 0)
    9.97 +    fun TAG (p, i) b = BoolVar (prod 7 p i b)
    9.98 +  in
    9.99 +    (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
   9.100 +  end
   9.101 +
   9.102 +
   9.103 +fun graph_info gp g =
   9.104 +  let
   9.105 +    val G (p, q, edgs) = graph_at (gp, g)
   9.106 +  in
   9.107 +    (g, p, q, arity gp p, arity gp q, edgs)
   9.108 +  end
   9.109 +
   9.110 +
   9.111 +(* Order-independent part of encoding *)
   9.112 +
   9.113 +fun encode_graphs bits gp =
   9.114 +  let
   9.115 +    val ng = num_graphs gp
   9.116 +    val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
   9.117 +
   9.118 +    fun encode_constraint_strict 0 (x, y) = PropLogic.False
   9.119 +      | encode_constraint_strict k (x, y) =
   9.120 +        Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
   9.121 +            And (Equiv (TAG x (k - 1), TAG y (k - 1)),
   9.122 +                 encode_constraint_strict (k - 1) (x, y)))
   9.123 +
   9.124 +    fun encode_constraint_weak k (x, y) =
   9.125 +        Or (encode_constraint_strict k (x, y),
   9.126 +            iforall k (fn i => Equiv (TAG x i, TAG y i)))
   9.127 +
   9.128 +    fun encode_graph (g, p, q, n, m, edges) =
   9.129 +      let
   9.130 +        fun encode_edge i j =
   9.131 +          if exists (fn x => x = (i, GTR, j)) edges then
   9.132 +            And (ES (g, i, j), EW (g, i, j))
   9.133 +          else if not (exists (fn x => x = (i, GEQ, j)) edges) then
   9.134 +            And (Not (ES (g, i, j)), Not (EW (g, i, j)))
   9.135 +          else
   9.136 +            And (
   9.137 +              Equiv (ES (g, i, j),
   9.138 +                     encode_constraint_strict bits ((p, i), (q, j))),
   9.139 +              Equiv (EW (g, i, j),
   9.140 +                     encode_constraint_weak bits ((p, i), (q, j))))
   9.141 +       in
   9.142 +        iforall2 n m encode_edge
   9.143 +      end
   9.144 +  in
   9.145 +    iforall ng (encode_graph o graph_info gp)
   9.146 +  end
   9.147 +
   9.148 +
   9.149 +(* Order-specific part of encoding *)
   9.150 +
   9.151 +fun encode bits gp mu =
   9.152 +  let
   9.153 +    val ng = num_graphs gp
   9.154 +    val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
   9.155 +
   9.156 +    fun encode_graph MAX (g, p, q, n, m, _) =
   9.157 +        all [
   9.158 +          Equiv (WEAK g,
   9.159 +            iforall m (fn j =>
   9.160 +              Implies (P (q, j),
   9.161 +                iexists n (fn i =>
   9.162 +                  And (P (p, i), EW (g, i, j)))))),
   9.163 +          Equiv (STRICT g,
   9.164 +            iforall m (fn j =>
   9.165 +              Implies (P (q, j),
   9.166 +                iexists n (fn i =>
   9.167 +                  And (P (p, i), ES (g, i, j)))))),
   9.168 +          iexists n (fn i => P (p, i))
   9.169 +        ]
   9.170 +      | encode_graph MIN (g, p, q, n, m, _) =
   9.171 +        all [
   9.172 +          Equiv (WEAK g,
   9.173 +            iforall n (fn i =>
   9.174 +              Implies (P (p, i),
   9.175 +                iexists m (fn j =>
   9.176 +                  And (P (q, j), EW (g, i, j)))))),
   9.177 +          Equiv (STRICT g,
   9.178 +            iforall n (fn i =>
   9.179 +              Implies (P (p, i),
   9.180 +                iexists m (fn j =>
   9.181 +                  And (P (q, j), ES (g, i, j)))))),
   9.182 +          iexists m (fn j => P (q, j))
   9.183 +        ]
   9.184 +      | encode_graph MS (g, p, q, n, m, _) =
   9.185 +        all [
   9.186 +          Equiv (WEAK g,
   9.187 +            iforall m (fn j =>
   9.188 +              Implies (P (q, j),
   9.189 +                iexists n (fn i => GAM (g, i, j))))),
   9.190 +          Equiv (STRICT g,
   9.191 +            iexists n (fn i =>
   9.192 +              And (P (p, i), Not (EPS (g, i))))),
   9.193 +          iforall2 n m (fn i => fn j =>
   9.194 +            Implies (GAM (g, i, j),
   9.195 +              all [
   9.196 +                P (p, i),
   9.197 +                P (q, j),
   9.198 +                EW (g, i, j),
   9.199 +                Equiv (Not (EPS (g, i)), ES (g, i, j))])),
   9.200 +          iforall n (fn i =>
   9.201 +            Implies (And (P (p, i), EPS (g, i)),
   9.202 +              exactly_one m (fn j => GAM (g, i, j))))
   9.203 +        ]
   9.204 +  in
   9.205 +    all [
   9.206 +      encode_graphs bits gp,
   9.207 +      iforall ng (encode_graph mu o graph_info gp),
   9.208 +      iforall ng (fn x => WEAK x),
   9.209 +      iexists ng (fn x => STRICT x)
   9.210 +    ]
   9.211 +  end
   9.212 +
   9.213 +
   9.214 +(*Generieren des level-mapping und diverser output*)
   9.215 +fun mk_certificate bits label gp f =
   9.216 +  let
   9.217 +    val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
   9.218 +    fun assign (PropLogic.BoolVar v) = the_default false (f v)
   9.219 +    fun assignTag i j =
   9.220 +      (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
   9.221 +        (bits - 1 downto 0) 0)
   9.222 +
   9.223 +    val level_mapping =
   9.224 +      let fun prog_pt_mapping p =
   9.225 +            map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
   9.226 +              (0 upto (arity gp p) - 1)
   9.227 +      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
   9.228 +
   9.229 +    val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
   9.230 +
   9.231 +    fun covering_pair g bStrict j =
   9.232 +      let
   9.233 +        val (_, p, q, n, m, _) = graph_info gp g
   9.234 +
   9.235 +        fun cover        MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (EW  (g, i, j))) (0 upto n - 1)
   9.236 +          | cover        MS  k = find_index (fn i =>                                     assign (GAM (g, i, k))) (0 upto n - 1)
   9.237 +          | cover        MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (EW  (g, i, j))) (0 upto m - 1)
   9.238 +        fun cover_strict MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (ES  (g, i, j))) (0 upto n - 1)
   9.239 +          | cover_strict MS  k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i)  ))) (0 upto n - 1)
   9.240 +          | cover_strict MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (ES  (g, i, j))) (0 upto m - 1)
   9.241 +        val i = if bStrict then cover_strict label j else cover label j
   9.242 +      in
   9.243 +        find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
   9.244 +      end
   9.245 +  in
   9.246 +    (label, level_mapping, strict_list, covering_pair)
   9.247 +  end
   9.248 +
   9.249 +(*interface for the proof reconstruction*)
   9.250 +fun generate_certificate use_tags labels gp =
   9.251 +  let
   9.252 +    val bits = if use_tags then ndigits gp else 0
   9.253 +  in
   9.254 +    get_first
   9.255 +      (fn l => case sat_solver (encode bits gp l) of
   9.256 +                 SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
   9.257 +               | _ => NONE)
   9.258 +      labels
   9.259 +  end
   9.260 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/function_package/termination.ML	Tue Dec 16 08:46:07 2008 +0100
    10.3 @@ -0,0 +1,324 @@
    10.4 +(*  Title:       HOL/Tools/function_package/termination_data.ML
    10.5 +    Author:      Alexander Krauss, TU Muenchen
    10.6 +
    10.7 +Context data for termination proofs
    10.8 +*)
    10.9 +
   10.10 +
   10.11 +signature TERMINATION =
   10.12 +sig
   10.13 +
   10.14 +  type data
   10.15 +  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
   10.16 +
   10.17 +  val mk_sumcases : data -> typ -> term list -> term
   10.18 +
   10.19 +  val note_measure : int -> term -> data -> data
   10.20 +  val note_chain   : term -> term -> thm option -> data -> data
   10.21 +  val note_descent : term -> term -> term -> cell -> data -> data
   10.22 +
   10.23 +  val get_num_points : data -> int
   10.24 +  val get_types      : data -> int -> typ
   10.25 +  val get_measures   : data -> int -> term list
   10.26 +
   10.27 +  (* read from cache *)
   10.28 +  val get_chain      : data -> term -> term -> thm option option
   10.29 +  val get_descent    : data -> term -> term -> term -> cell option
   10.30 +
   10.31 +  (* writes *)
   10.32 +  val derive_descent  : theory -> tactic -> term -> term -> term -> data -> data
   10.33 +  val derive_descents : theory -> tactic -> term -> data -> data
   10.34 +
   10.35 +  val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
   10.36 +
   10.37 +  val CALLS : (term list * int -> tactic) -> int -> tactic
   10.38 +
   10.39 +  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
   10.40 +  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   10.41 +
   10.42 +  val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
   10.43 +
   10.44 +  val REPEAT : ttac -> ttac
   10.45 +
   10.46 +  val wf_union_tac : tactic
   10.47 +end
   10.48 +
   10.49 +
   10.50 +
   10.51 +structure Termination : TERMINATION =
   10.52 +struct
   10.53 +
   10.54 +open FundefLib
   10.55 +
   10.56 +val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
   10.57 +structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
   10.58 +structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
   10.59 +
   10.60 +(** Analyzing binary trees **)
   10.61 +
   10.62 +(* Skeleton of a tree structure *)
   10.63 +
   10.64 +datatype skel =
   10.65 +  SLeaf of int (* index *)
   10.66 +| SBranch of (skel * skel)
   10.67 +
   10.68 +
   10.69 +(* abstract make and dest functions *)
   10.70 +fun mk_tree leaf branch =
   10.71 +  let fun mk (SLeaf i) = leaf i
   10.72 +        | mk (SBranch (s, t)) = branch (mk s, mk t)
   10.73 +  in mk end
   10.74 +
   10.75 +
   10.76 +fun dest_tree split =
   10.77 +  let fun dest (SLeaf i) x = [(i, x)]
   10.78 +        | dest (SBranch (s, t)) x =
   10.79 +          let val (l, r) = split x
   10.80 +          in dest s l @ dest t r end
   10.81 +  in dest end
   10.82 +
   10.83 +
   10.84 +(* concrete versions for sum types *)
   10.85 +fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
   10.86 +  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
   10.87 +  | is_inj _ = false
   10.88 +
   10.89 +fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
   10.90 +  | dest_inl _ = NONE
   10.91 +
   10.92 +fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
   10.93 +  | dest_inr _ = NONE
   10.94 +
   10.95 +
   10.96 +fun mk_skel ps =
   10.97 +  let
   10.98 +    fun skel i ps =
   10.99 +      if forall is_inj ps andalso not (null ps)
  10.100 +      then let
  10.101 +          val (j, s) = skel i (map_filter dest_inl ps)
  10.102 +          val (k, t) = skel j (map_filter dest_inr ps)
  10.103 +        in (k, SBranch (s, t)) end
  10.104 +      else (i + 1, SLeaf i)
  10.105 +  in
  10.106 +    snd (skel 0 ps)
  10.107 +  end
  10.108 +
  10.109 +(* compute list of types for nodes *)
  10.110 +fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
  10.111 +
  10.112 +(* find index and raw term *)
  10.113 +fun dest_inj (SLeaf i) trm = (i, trm)
  10.114 +  | dest_inj (SBranch (s, t)) trm =
  10.115 +    case dest_inl trm of
  10.116 +      SOME trm' => dest_inj s trm'
  10.117 +    | _ => dest_inj t (the (dest_inr trm))
  10.118 +
  10.119 +
  10.120 +
  10.121 +(** Matrix cell datatype **)
  10.122 +
  10.123 +datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
  10.124 +
  10.125 +
  10.126 +type data =
  10.127 +  skel                            (* structure of the sum type encoding "program points" *)
  10.128 +  * (int -> typ)                  (* types of program points *)
  10.129 +  * (term list Inttab.table)      (* measures for program points *)
  10.130 +  * (thm option Term2tab.table)   (* which calls form chains? *)
  10.131 +  * (cell Term3tab.table)         (* local descents *)
  10.132 +
  10.133 +
  10.134 +fun map_measures f (p, T, M, C, D) = (p, T, f M, C, D)
  10.135 +fun map_chains f   (p, T, M, C, D) = (p, T, M, f C, D)
  10.136 +fun map_descent f  (p, T, M, C, D) = (p, T, M, C, f D)
  10.137 +
  10.138 +fun note_measure p m = map_measures (Inttab.insert_list (op aconv) (p, m))
  10.139 +fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
  10.140 +fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
  10.141 +
  10.142 +(* Build case expression *)
  10.143 +fun mk_sumcases (sk, _, _, _, _) T fs =
  10.144 +  mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
  10.145 +          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
  10.146 +          sk
  10.147 +  |> fst
  10.148 +
  10.149 +fun mk_sum_skel rel =
  10.150 +  let
  10.151 +    val cs = FundefLib.dest_binop_list @{const_name "op Un"} rel
  10.152 +    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
  10.153 +      let
  10.154 +        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
  10.155 +          = Term.strip_qnt_body "Ex" c
  10.156 +      in cons r o cons l end
  10.157 +  in
  10.158 +    mk_skel (fold collect_pats cs [])
  10.159 +  end
  10.160 +
  10.161 +fun create ctxt T rel =
  10.162 +  let
  10.163 +    val sk = mk_sum_skel rel
  10.164 +    val Ts = node_types sk T
  10.165 +    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
  10.166 +  in
  10.167 +    (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
  10.168 +  end
  10.169 +
  10.170 +fun get_num_points (sk, _, _, _, _) =
  10.171 +  let
  10.172 +    fun num (SLeaf i) = i + 1
  10.173 +      | num (SBranch (s, t)) = num t
  10.174 +  in num sk end
  10.175 +
  10.176 +fun get_types (_, T, _, _, _) = T
  10.177 +fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
  10.178 +
  10.179 +fun get_chain (_, _, _, C, _) c1 c2 =
  10.180 +  Term2tab.lookup C (c1, c2)
  10.181 +
  10.182 +fun get_descent (_, _, _, _, D) c m1 m2 =
  10.183 +  Term3tab.lookup D (c, (m1, m2))
  10.184 +
  10.185 +fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
  10.186 +  let
  10.187 +    val n = get_num_points D
  10.188 +    val (sk, _, _, _, _) = D
  10.189 +    val vs = Term.strip_qnt_vars "Ex" c
  10.190 +
  10.191 +    (* FIXME: throw error "dest_call" for malformed terms *)
  10.192 +    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
  10.193 +      = Term.strip_qnt_body "Ex" c
  10.194 +    val (p, l') = dest_inj sk l
  10.195 +    val (q, r') = dest_inj sk r
  10.196 +  in
  10.197 +    (vs, p, l', q, r', Gam)
  10.198 +  end
  10.199 +  | dest_call D t = error "dest_call"
  10.200 +
  10.201 +
  10.202 +fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
  10.203 +  case get_descent D c m1 m2 of
  10.204 +    SOME _ => D
  10.205 +  | NONE => let
  10.206 +    fun cgoal rel =
  10.207 +      Term.list_all (vs,
  10.208 +        Logic.mk_implies (HOLogic.mk_Trueprop Gam,
  10.209 +          HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
  10.210 +            $ (m2 $ r') $ (m1 $ l'))))
  10.211 +      |> cterm_of thy
  10.212 +    in
  10.213 +      note_descent c m1 m2
  10.214 +        (case try_proof (cgoal @{const_name HOL.less}) tac of
  10.215 +           Solved thm => Less thm
  10.216 +         | Stuck thm =>
  10.217 +           (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
  10.218 +              Solved thm2 => LessEq (thm2, thm)
  10.219 +            | Stuck thm2 =>
  10.220 +              if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
  10.221 +              then False thm2 else None (thm2, thm)
  10.222 +            | _ => raise Match) (* FIXME *)
  10.223 +         | _ => raise Match) D
  10.224 +      end
  10.225 +
  10.226 +fun derive_descent thy tac c m1 m2 D =
  10.227 +  derive_desc_aux thy tac c (dest_call D c) m1 m2 D
  10.228 +
  10.229 +(* all descents in one go *)
  10.230 +fun derive_descents thy tac c D =
  10.231 +  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
  10.232 +  in fold_product (derive_desc_aux thy tac c cdesc)
  10.233 +       (get_measures D p) (get_measures D q) D
  10.234 +  end
  10.235 +
  10.236 +fun CALLS tac i st =
  10.237 +  if Thm.no_prems st then all_tac st
  10.238 +  else case Thm.term_of (Thm.cprem_of st i) of
  10.239 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name "op Un"} rel, i) st
  10.240 +  |_ => no_tac st
  10.241 +
  10.242 +type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
  10.243 +
  10.244 +fun TERMINATION ctxt tac =
  10.245 +  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
  10.246 +  let
  10.247 +    val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
  10.248 +  in
  10.249 +    tac (create ctxt T rel) i
  10.250 +  end)
  10.251 +
  10.252 +
  10.253 +(* A tactic to convert open to closed termination goals *)
  10.254 +local
  10.255 +fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
  10.256 +    let
  10.257 +      val (vars, prop) = FundefLib.dest_all_all t
  10.258 +      val (prems, concl) = Logic.strip_horn prop
  10.259 +      val (lhs, rhs) = concl
  10.260 +                         |> HOLogic.dest_Trueprop
  10.261 +                         |> HOLogic.dest_mem |> fst
  10.262 +                         |> HOLogic.dest_prod
  10.263 +    in
  10.264 +      (vars, prems, lhs, rhs)
  10.265 +    end
  10.266 +
  10.267 +fun mk_pair_compr (T, qs, l, r, conds) =
  10.268 +    let
  10.269 +      val pT = HOLogic.mk_prodT (T, T)
  10.270 +      val n = length qs
  10.271 +      val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
  10.272 +      val conds' = if null conds then [HOLogic.true_const] else conds
  10.273 +    in
  10.274 +      HOLogic.Collect_const pT $
  10.275 +      Abs ("uu_", pT,
  10.276 +           (foldr1 HOLogic.mk_conj (peq :: conds')
  10.277 +            |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
  10.278 +    end
  10.279 +
  10.280 +in
  10.281 +
  10.282 +fun wf_union_tac st =
  10.283 +    let
  10.284 +      val thy = theory_of_thm st
  10.285 +      val cert = cterm_of (theory_of_thm st)
  10.286 +      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
  10.287 +
  10.288 +      fun mk_compr ineq =
  10.289 +          let
  10.290 +            val (vars, prems, lhs, rhs) = dest_term ineq
  10.291 +          in
  10.292 +            mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
  10.293 +          end
  10.294 +
  10.295 +      val relation =
  10.296 +          if null ineqs then
  10.297 +              Const (@{const_name "{}"}, fastype_of rel)
  10.298 +          else
  10.299 +              foldr1 (HOLogic.mk_binop @{const_name "op Un"}) (map mk_compr ineqs)
  10.300 +
  10.301 +      fun solve_membership_tac i =
  10.302 +          (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
  10.303 +          THEN' (fn j => TRY (rtac @{thm UnI1} j))
  10.304 +          THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
  10.305 +          THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
  10.306 +          THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
  10.307 +                 ORELSE' ((rtac @{thm conjI})
  10.308 +                          THEN' (rtac @{thm refl})
  10.309 +                          THEN' (CLASET' blast_tac)))     (* Solve rest of context... not very elegant *)
  10.310 +          ) i
  10.311 +    in
  10.312 +      ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
  10.313 +      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
  10.314 +    end
  10.315 +
  10.316 +
  10.317 +end
  10.318 +
  10.319 +
  10.320 +(* continuation passing repeat combinator *)
  10.321 +fun REPEAT ttac cont err_cont =
  10.322 +    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
  10.323 +
  10.324 +
  10.325 +
  10.326 +
  10.327 +end
    11.1 --- a/src/HOL/Wellfounded.thy	Tue Dec 16 00:19:47 2008 +0100
    11.2 +++ b/src/HOL/Wellfounded.thy	Tue Dec 16 08:46:07 2008 +0100
    11.3 @@ -842,6 +842,11 @@
    11.4    qed
    11.5  qed
    11.6  
    11.7 +lemma max_ext_additive: 
    11.8 + "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
    11.9 +  (A \<union> C, B \<union> D) \<in> max_ext R"
   11.10 +by (force elim!: max_ext.cases)
   11.11 +
   11.12  
   11.13  definition
   11.14    min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
    12.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 00:19:47 2008 +0100
    12.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 08:46:07 2008 +0100
    12.3 @@ -24,4 +24,11 @@
    12.4    "~~/src/HOL/ex/Records"
    12.5  begin
    12.6  
    12.7 +text {* However, some aren't executable *}
    12.8 +
    12.9 +declare pair_leq_def[code del]
   12.10 +declare max_weak_def[code del]
   12.11 +declare min_weak_def[code del]
   12.12 +declare ms_weak_def[code del]
   12.13 +
   12.14  end