equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Size_Change_Termination.thy |
1 (* Title: HOL/Library/Size_Change_Termination.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header "" (* FIXME proper header *) |
6 header "Size-Change Termination" |
7 |
7 |
8 theory Size_Change_Termination |
8 theory Size_Change_Termination |
9 imports SCT_Theorem SCT_Interpretation SCT_Implementation |
9 imports SCT_Theorem SCT_Interpretation SCT_Implementation |
10 uses "sct.ML" |
10 uses "sct.ML" |
11 begin |
11 begin |
100 split_conv |
100 split_conv |
101 |
101 |
102 lemmas sctTest_congs = |
102 lemmas sctTest_congs = |
103 if_weak_cong let_weak_cong setbcomp_cong |
103 if_weak_cong let_weak_cong setbcomp_cong |
104 |
104 |
|
105 |
|
106 lemma SCT_Main: |
|
107 "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A" |
|
108 using LJA_Theorem4 SCT'_exec |
|
109 by auto |
|
110 |
105 end |
111 end |