|
1 (* Title: HOL/Library/Size_Change_Termination.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header "Size-Change Termination" |
|
7 |
|
8 theory Size_Change_Termination |
|
9 imports Correctness Interpretation Implementation |
|
10 uses "sct.ML" |
|
11 begin |
|
12 |
|
13 subsection {* Simplifier setup *} |
|
14 |
|
15 text {* This is needed to run the SCT algorithm in the simplifier: *} |
|
16 |
|
17 lemma setbcomp_simps: |
|
18 "{x\<in>{}. P x} = {}" |
|
19 "{x\<in>insert y ys. P x} = (if P y then insert y {x\<in>ys. P x} else {x\<in>ys. P x})" |
|
20 by auto |
|
21 |
|
22 lemma setbcomp_cong: |
|
23 "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}" |
|
24 by auto |
|
25 |
|
26 lemma cartprod_simps: |
|
27 "{} \<times> A = {}" |
|
28 "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)" |
|
29 by (auto simp:image_def) |
|
30 |
|
31 lemma image_simps: |
|
32 "fu ` {} = {}" |
|
33 "fu ` insert a A = insert (fu a) (fu ` A)" |
|
34 by (auto simp:image_def) |
|
35 |
|
36 lemmas union_simps = |
|
37 Un_empty_left Un_empty_right Un_insert_left |
|
38 |
|
39 lemma subset_simps: |
|
40 "{} \<subseteq> B" |
|
41 "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B" |
|
42 by auto |
|
43 |
|
44 lemma element_simps: |
|
45 "x \<in> {} \<equiv> False" |
|
46 "x \<in> insert a A \<equiv> x = a \<or> x \<in> A" |
|
47 by auto |
|
48 |
|
49 lemma set_eq_simp: |
|
50 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto |
|
51 |
|
52 lemma ball_simps: |
|
53 "\<forall>x\<in>{}. P x \<equiv> True" |
|
54 "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)" |
|
55 by auto |
|
56 |
|
57 lemma bex_simps: |
|
58 "\<exists>x\<in>{}. P x \<equiv> False" |
|
59 "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)" |
|
60 by auto |
|
61 |
|
62 lemmas set_simps = |
|
63 setbcomp_simps |
|
64 cartprod_simps image_simps union_simps subset_simps |
|
65 element_simps set_eq_simp |
|
66 ball_simps bex_simps |
|
67 |
|
68 lemma sedge_simps: |
|
69 "\<down> * x = \<down>" |
|
70 "\<Down> * x = x" |
|
71 by (auto simp:mult_sedge_def) |
|
72 |
|
73 lemmas sctTest_simps = |
|
74 simp_thms |
|
75 if_True |
|
76 if_False |
|
77 nat.inject |
|
78 nat.distinct |
|
79 Pair_eq |
|
80 |
|
81 grcomp_code |
|
82 edges_match.simps |
|
83 connect_edges.simps |
|
84 |
|
85 sedge_simps |
|
86 sedge.distinct |
|
87 set_simps |
|
88 |
|
89 graph_mult_def |
|
90 graph_leq_def |
|
91 dest_graph.simps |
|
92 graph_plus_def |
|
93 graph.inject |
|
94 graph_zero_def |
|
95 |
|
96 test_SCT_def |
|
97 mk_tcl_code |
|
98 |
|
99 Let_def |
|
100 split_conv |
|
101 |
|
102 lemmas sctTest_congs = |
|
103 if_weak_cong let_weak_cong setbcomp_cong |
|
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 |
|
111 end |