Made "termination by lexicographic_order" the default for "fun" definitions.
authorkrauss
Wed Nov 08 09:08:54 2006 +0100 (2006-11-08)
changeset 212408e75fb38522c
parent 21239 d4fbe2c87ef1
child 21241 a00a16cbc647
Made "termination by lexicographic_order" the default for "fun" definitions.
NEWS
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/NEWS	Wed Nov 08 02:13:02 2006 +0100
     1.2 +++ b/NEWS	Wed Nov 08 09:08:54 2006 +0100
     1.3 @@ -476,6 +476,22 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Automated termination proofs "by lexicographic_order" are now
     1.8 +included in the abbreviated function command "fun". No explicit
     1.9 +"termination" command is necessary anymore.
    1.10 +INCOMPATIBILITY: If a "fun"-definition cannot be proved terminating by
    1.11 +a lexicographic size order, then the command fails. Use the expanded
    1.12 +version "function" for these cases.
    1.13 +
    1.14 +* New method "lexicographic_order" automatically synthesizes
    1.15 +termination relations as lexicographic combinations of size measures. 
    1.16 +Usage for (function package) termination proofs:
    1.17 +
    1.18 +termination 
    1.19 +by lexicographic_order
    1.20 +
    1.21 +Contributed by Lukas Bulwahn.
    1.22 +
    1.23  * Records: generalised field-update to take a function on the field 
    1.24  rather than the new value: r(|A := x|) is translated to A_update (K x) r
    1.25  The K-combinator that is internally used is called K_record.
     2.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 02:13:02 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 09:08:54 2006 +0100
     2.3 @@ -192,7 +192,7 @@
     2.4      lthy
     2.5        |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
     2.6        ||> by_pat_completeness_simp
     2.7 -      (*|-> termination_by_lexicographic_order*) |> snd
     2.8 +      |-> termination_by_lexicographic_order
     2.9  
    2.10  
    2.11  val funP =
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 02:13:02 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 09:08:54 2006 +0100
     3.3 @@ -73,7 +73,8 @@
     3.4          |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
     3.5          |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
     3.6          |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
     3.7 -        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))
     3.8 +        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
     3.9 +        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
    3.10      end (* FIXME: Add cases for induct and cases thm *)
    3.11  
    3.12  
     4.1 --- a/src/HOL/ex/Fundefs.thy	Wed Nov 08 02:13:02 2006 +0100
     4.2 +++ b/src/HOL/ex/Fundefs.thy	Wed Nov 08 09:08:54 2006 +0100
     4.3 @@ -29,8 +29,8 @@
     4.4  
     4.5  
     4.6  text {* Now termination: *}
     4.7 -termination fib
     4.8 -  by (auto_term "less_than")
     4.9 +(*termination fib
    4.10 +  by (auto_term "less_than")*)
    4.11  
    4.12  thm fib.simps
    4.13  thm fib.induct
    4.14 @@ -42,8 +42,6 @@
    4.15  where
    4.16    "add 0 y = y"
    4.17  | "add (Suc x) y = Suc (add x y)"
    4.18 -termination
    4.19 -  by (auto_term "measure fst")
    4.20  
    4.21  thm add.simps
    4.22  thm add.induct -- {* Note the curried induction predicate *}
    4.23 @@ -51,10 +49,11 @@
    4.24  
    4.25  section {* Nested recursion *}
    4.26  
    4.27 -fun nz :: "nat \<Rightarrow> nat"
    4.28 +function nz :: "nat \<Rightarrow> nat"
    4.29  where
    4.30    "nz 0 = 0"
    4.31  | "nz (Suc x) = nz (nz x)"
    4.32 +by pat_completeness auto
    4.33  
    4.34  lemma nz_is_zero: -- {* A lemma we need to prove termination *}
    4.35    assumes trm: "nz_dom x"
    4.36 @@ -72,9 +71,10 @@
    4.37  text {* Here comes McCarthy's 91-function *}
    4.38  
    4.39  
    4.40 -fun f91 :: "nat => nat"
    4.41 +function f91 :: "nat => nat"
    4.42  where
    4.43    "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
    4.44 +by pat_completeness auto
    4.45  
    4.46  (* Prove a lemma before attempting a termination proof *)
    4.47  lemma f91_estimate: 
    4.48 @@ -112,10 +112,6 @@
    4.49  | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
    4.50                                      else gcd2 (x - y) (Suc y))"
    4.51  
    4.52 -
    4.53 -termination 
    4.54 -  by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))")
    4.55 -
    4.56  thm gcd2.simps
    4.57  thm gcd2.induct
    4.58  
    4.59 @@ -132,9 +128,7 @@
    4.60    apply (case_tac x, case_tac a, auto)
    4.61    apply (case_tac ba, auto)
    4.62    done
    4.63 -
    4.64 -termination 
    4.65 -  by (auto_term "measure (\<lambda>(x,y). x + y)")
    4.66 +termination by lexicographic_order
    4.67  
    4.68  thm gcd3.simps
    4.69  thm gcd3.induct
    4.70 @@ -164,7 +158,7 @@
    4.71      with c2 show "P" .
    4.72    qed
    4.73  qed presburger+ -- {* solve compatibility with presburger *}
    4.74 -termination by (auto_term "{}")
    4.75 +termination by lexicographic_order
    4.76  
    4.77  thm ev.simps
    4.78  thm ev.induct
    4.79 @@ -180,18 +174,15 @@
    4.80  | "evn (Suc n) = od n"
    4.81  | "od (Suc n) = evn n"
    4.82  
    4.83 -thm evn.psimps
    4.84 -thm od.psimps
    4.85 +thm evn.simps
    4.86 +thm od.simps
    4.87  
    4.88  thm evn_od.pinduct
    4.89  thm evn_od.termination
    4.90  thm evn_od.domintros
    4.91  
    4.92 -termination
    4.93 -  by (auto_term "measure (sum_case (%n. n) (%n. n))")
    4.94  
    4.95 -thm evn.simps
    4.96 -thm od.simps
    4.97 +
    4.98  
    4.99  
   4.100  end