# HG changeset patch # User nipkow # Date 1503604586 -7200 # Node ID 8367a4f25781754ca2f9b2b255705efdf04ffead # Parent 97fc319d608980bae580bf774b53d4e90f3dbf2a tuned diff -r 97fc319d6089 -r 8367a4f25781 src/HOL/Data_Structures/Base_FDS.thy --- a/src/HOL/Data_Structures/Base_FDS.thy Thu Aug 24 12:45:46 2017 +0100 +++ b/src/HOL/Data_Structures/Base_FDS.thy Thu Aug 24 21:56:26 2017 +0200 @@ -11,8 +11,7 @@ of different parameters. To alert the reader whenever such a more subtle termination proof is taking place -the lemma is not enabled all the time but only locally in a \context\ block -around such function definitions. +the lemma is not enabled all the time but only when it is needed. \ lemma size_prod_measure: diff -r 97fc319d6089 -r 8367a4f25781 src/HOL/Data_Structures/Leftist_Heap.thy --- a/src/HOL/Data_Structures/Leftist_Heap.thy Thu Aug 24 12:45:46 2017 +0100 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy Thu Aug 24 21:56:26 2017 +0200 @@ -10,8 +10,6 @@ Complex_Main begin -unbundle pattern_aliases - fun mset_tree :: "('a,'b) tree \ 'a multiset" where "mset_tree Leaf = {#}" | "mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r" @@ -46,16 +44,16 @@ fun get_min :: "'a lheap \ 'a" where "get_min(Node n l a r) = a" -text\Explicit termination argument: sum of sizes\ +text \For function \merge\:\ +unbundle pattern_aliases +declare size_prod_measure[measure_function] -function merge :: "'a::ord lheap \ 'a lheap \ 'a lheap" where +fun merge :: "'a::ord lheap \ 'a lheap \ 'a lheap" where "merge Leaf t2 = t2" | "merge t1 Leaf = t1" | "merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) = (if a1 \ a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))" -by pat_completeness auto -termination by (relation "measure (\(t1,t2). size t1 + size t2)") auto lemma merge_code: "merge t1 t2 = (case (t1,t2) of (Leaf, _) \ t2 | @@ -180,14 +178,12 @@ text\Explicit termination argument: sum of sizes\ -function t_merge :: "'a::ord lheap \ 'a lheap \ nat" where +fun t_merge :: "'a::ord lheap \ 'a lheap \ nat" where "t_merge Leaf t2 = 1" | "t_merge t2 Leaf = 1" | "t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) = (if a1 \ a2 then 1 + t_merge r1 t2 else 1 + t_merge r2 t1)" -by pat_completeness auto -termination by (relation "measure (\(t1,t2). size t1 + size t2)") auto definition t_insert :: "'a::ord \ 'a lheap \ nat" where "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"