merged
authorkrauss
Sun, 29 Apr 2012 20:53:55 +0200
changeset 47837 ddc7921701c5
parent 47836 471cc845430b (diff)
parent 47834 4e247a648a01 (current diff)
child 47838 47d213b10fd7
merged
src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/Tools/Function/termination.ML	Sun Apr 29 20:42:09 2012 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sun Apr 29 20:53:55 2012 +0200
@@ -315,7 +315,7 @@
   |> fold (fn c => Term_Graph.new_node (c, ())) cs
   |> fold_product (fn c1 => fn c2 =>
      if is_none (get_chain D c1 c2 |> the_default NONE)
-     then Term_Graph.add_edge (c1, c2) else I)
+     then Term_Graph.add_edge (c2, c1) else I)
      cs cs
 
 fun ucomp_empty_tac T =
--- a/src/HOL/ex/Termination.thy	Sun Apr 29 20:42:09 2012 +0200
+++ b/src/HOL/ex/Termination.thy	Sun Apr 29 20:53:55 2012 +0200
@@ -229,4 +229,21 @@
 by pat_completeness auto
 termination by size_change -- {* requires Multiset *}
 
+definition negate :: "int \<Rightarrow> int"
+where "negate i = - i"
+
+function fun3 :: "int => nat"
+where
+  "fun3 i =
+  (if i < 0 then fun3 (negate i)
+   else if i = 0 then 0
+   else fun3 (i - 1))"
+by (pat_completeness) auto
+termination
+  apply size_change
+  apply (simp add: negate_def)
+  apply size_change
+  done
+
+
 end