--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SizeChange/Examples.thy Tue Nov 06 17:44:53 2007 +0100
@@ -0,0 +1,83 @@
+(* Title: HOL/Library/SCT_Examples.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
+header {* Examples for Size-Change Termination *}
+
+theory Examples
+imports Size_Change_Termination
+begin
+
+function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "f n 0 = n"
+| "f 0 (Suc m) = f (Suc m) m"
+| "f (Suc n) (Suc m) = f m n"
+by pat_completeness auto
+
+
+termination
+ unfolding f_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
+ apply (rule ext, rule ext, simp) (* Show that they are correct *)
+ apply (tactic "Sct.mk_call_graph") (* Build control graph *)
+ apply (rule SCT_Main) (* Apply main theorem *)
+ apply (simp add:finite_acg_simps) (* show finiteness *)
+ by eval (* Evaluate to true *)
+
+function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "p m n r = (if r>0 then p m (r - 1) n else
+ if n>0 then p r (n - 1) m
+ else m)"
+by pat_completeness auto
+
+termination
+ unfolding p_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "Sct.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "Sct.mk_call_graph")
+ apply (rule SCT_Main)
+ apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+ by eval
+
+function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "foo True (Suc n) m = foo True n (Suc m)"
+| "foo True 0 m = foo False 0 m"
+| "foo False n (Suc m) = foo False (Suc n) m"
+| "foo False n 0 = n"
+by pat_completeness auto
+
+termination
+ unfolding foo_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "Sct.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "Sct.mk_call_graph")
+ apply (rule SCT_Main)
+ apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+ by eval
+
+
+function (sequential)
+ bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "bar 0 (Suc n) m = bar m m m"
+| "bar k n m = 0"
+by pat_completeness auto
+
+termination
+ unfolding bar_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "Sct.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "Sct.mk_call_graph")
+ apply (rule SCT_Main)
+ apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+ by (simp only:sctTest_simps cong: sctTest_congs)
+
+end