src/HOL/Hoare/Pointers0.thy
 changeset 35419 d78659d1723e parent 35416 d8d7d1b785af child 38353 d98baa2cf589
1.1 --- a/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 16:42:45 2010 +0100
1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 17:05:57 2010 +0100
1.3 @@ -320,13 +320,11 @@
1.5  text"This is still a bit rough, especially the proof."
1.7 -consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
1.8 -
1.9 -recdef merge "measure(%(xs,ys,f). size xs + size ys)"
1.10 +fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
1.11  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
1.12 -                                else y # merge(x#xs,ys,f))"
1.13 -"merge(x#xs,[],f) = x # merge(xs,[],f)"
1.14 -"merge([],y#ys,f) = y # merge([],ys,f)"
1.15 +                                else y # merge(x#xs,ys,f))" |
1.16 +"merge(x#xs,[],f) = x # merge(xs,[],f)" |
1.17 +"merge([],y#ys,f) = y # merge([],ys,f)" |
1.18  "merge([],[],f) = []"
1.20  lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"