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