equal
deleted
inserted
replaced
20 termination |
20 termination |
21 unfolding f_rel_def lfp_const |
21 unfolding f_rel_def lfp_const |
22 apply (rule SCT_on_relations) |
22 apply (rule SCT_on_relations) |
23 apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *) |
23 apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *) |
24 apply (rule ext, rule ext, simp) (* Show that they are correct *) |
24 apply (rule ext, rule ext, simp) (* Show that they are correct *) |
25 apply (tactic "Sct.mk_call_graph") (* Build control graph *) |
25 apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *) |
26 apply (rule SCT_Main) (* Apply main theorem *) |
26 apply (rule SCT_Main) (* Apply main theorem *) |
27 apply (simp add:finite_acg_simps) (* show finiteness *) |
27 apply (simp add:finite_acg_simps) (* show finiteness *) |
28 oops (*FIXME by eval*) (* Evaluate to true *) |
28 oops (*FIXME by eval*) (* Evaluate to true *) |
29 |
29 |
30 function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
30 function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
37 termination |
37 termination |
38 unfolding p_rel_def lfp_const |
38 unfolding p_rel_def lfp_const |
39 apply (rule SCT_on_relations) |
39 apply (rule SCT_on_relations) |
40 apply (tactic "Sct.abs_rel_tac") |
40 apply (tactic "Sct.abs_rel_tac") |
41 apply (rule ext, rule ext, simp) |
41 apply (rule ext, rule ext, simp) |
42 apply (tactic "Sct.mk_call_graph") |
42 apply (tactic "Sct.mk_call_graph @{context}") |
43 apply (rule SCT_Main) |
43 apply (rule SCT_Main) |
44 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
44 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
45 oops (* FIXME by eval *) |
45 oops (* FIXME by eval *) |
46 |
46 |
47 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
47 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
55 termination |
55 termination |
56 unfolding foo_rel_def lfp_const |
56 unfolding foo_rel_def lfp_const |
57 apply (rule SCT_on_relations) |
57 apply (rule SCT_on_relations) |
58 apply (tactic "Sct.abs_rel_tac") |
58 apply (tactic "Sct.abs_rel_tac") |
59 apply (rule ext, rule ext, simp) |
59 apply (rule ext, rule ext, simp) |
60 apply (tactic "Sct.mk_call_graph") |
60 apply (tactic "Sct.mk_call_graph @{context}") |
61 apply (rule SCT_Main) |
61 apply (rule SCT_Main) |
62 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
62 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
63 oops (* FIXME by eval *) |
63 oops (* FIXME by eval *) |
64 |
64 |
65 |
65 |
73 termination |
73 termination |
74 unfolding bar_rel_def lfp_const |
74 unfolding bar_rel_def lfp_const |
75 apply (rule SCT_on_relations) |
75 apply (rule SCT_on_relations) |
76 apply (tactic "Sct.abs_rel_tac") |
76 apply (tactic "Sct.abs_rel_tac") |
77 apply (rule ext, rule ext, simp) |
77 apply (rule ext, rule ext, simp) |
78 apply (tactic "Sct.mk_call_graph") |
78 apply (tactic "Sct.mk_call_graph @{context}") |
79 apply (rule SCT_Main) |
79 apply (rule SCT_Main) |
80 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
80 apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *) |
81 by (simp only:sctTest_simps cong: sctTest_congs) |
81 by (simp only:sctTest_simps cong: sctTest_congs) |
82 |
82 |
83 end |
83 end |