1 (* Title: HOL/Library/SCT_Examples.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Examples for Size-Change Termination *} |
|
7 |
|
8 theory Examples |
|
9 imports Size_Change_Termination |
|
10 begin |
|
11 |
|
12 function f :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
13 where |
|
14 "f n 0 = n" |
|
15 | "f 0 (Suc m) = f (Suc m) m" |
|
16 | "f (Suc n) (Suc m) = f m n" |
|
17 by pat_completeness auto |
|
18 |
|
19 |
|
20 termination |
|
21 unfolding f_rel_def lfp_const |
|
22 apply (rule SCT_on_relations) |
|
23 apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *) |
|
24 apply (rule ext, rule ext, simp) (* Show that they are correct *) |
|
25 apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *) |
|
26 apply (rule SCT_Main) (* Apply main theorem *) |
|
27 apply (simp add:finite_acg_simps) (* show finiteness *) |
|
28 oops (*FIXME by eval*) (* Evaluate to true *) |
|
29 |
|
30 function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
31 where |
|
32 "p m n r = (if r>0 then p m (r - 1) n else |
|
33 if n>0 then p r (n - 1) m |
|
34 else m)" |
|
35 by pat_completeness auto |
|
36 |
|
37 termination |
|
38 unfolding p_rel_def lfp_const |
|
39 apply (rule SCT_on_relations) |
|
40 apply (tactic "Sct.abs_rel_tac") |
|
41 apply (rule ext, rule ext, simp) |
|
42 apply (tactic "Sct.mk_call_graph @{context}") |
|
43 apply (rule SCT_Main) |
|
44 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
|
45 oops (* FIXME by eval *) |
|
46 |
|
47 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
48 where |
|
49 "foo True (Suc n) m = foo True n (Suc m)" |
|
50 | "foo True 0 m = foo False 0 m" |
|
51 | "foo False n (Suc m) = foo False (Suc n) m" |
|
52 | "foo False n 0 = n" |
|
53 by pat_completeness auto |
|
54 |
|
55 termination |
|
56 unfolding foo_rel_def lfp_const |
|
57 apply (rule SCT_on_relations) |
|
58 apply (tactic "Sct.abs_rel_tac") |
|
59 apply (rule ext, rule ext, simp) |
|
60 apply (tactic "Sct.mk_call_graph @{context}") |
|
61 apply (rule SCT_Main) |
|
62 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
|
63 oops (* FIXME by eval *) |
|
64 |
|
65 |
|
66 function (sequential) |
|
67 bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
68 where |
|
69 "bar 0 (Suc n) m = bar m m m" |
|
70 | "bar k n m = 0" |
|
71 by pat_completeness auto |
|
72 |
|
73 termination |
|
74 unfolding bar_rel_def lfp_const |
|
75 apply (rule SCT_on_relations) |
|
76 apply (tactic "Sct.abs_rel_tac") |
|
77 apply (rule ext, rule ext, simp) |
|
78 apply (tactic "Sct.mk_call_graph @{context}") |
|
79 apply (rule SCT_Main) |
|
80 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
|
81 by (simp only:sctTest_simps cong: sctTest_congs) |
|
82 |
|
83 end |
|