author | wenzelm |
Fri, 13 Apr 2007 21:26:35 +0200 | |
changeset 22665 | cf152ff55d16 |
parent 22492 | 43545e640877 |
child 23374 | a2f492c599e0 |
permissions | -rw-r--r-- |
22371 | 1 |
(* Title: HOL/Library/SCT_Interpretation.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
*) |
|
5 |
||
22665 | 6 |
header "" |
7 |
||
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
8 |
theory SCT_Interpretation |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
9 |
imports Main SCT_Misc SCT_Definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
10 |
begin |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
11 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
12 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
13 |
"idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
14 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
15 |
lemma not_acc_smaller: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
16 |
assumes notacc: "\<not> acc R x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
17 |
shows "\<exists>y. R y x \<and> \<not> acc R y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
18 |
proof (rule classical) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
19 |
assume "\<not> ?thesis" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
20 |
hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
21 |
with accI have "acc R x" . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
22 |
with notacc show ?thesis by contradiction |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
23 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
24 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
25 |
lemma non_acc_has_idseq: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
26 |
assumes "\<not> acc R x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
27 |
shows "\<exists>s. idseq R s x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
28 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
29 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
30 |
have "\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
31 |
by (rule choice, auto simp:not_acc_smaller) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
32 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
33 |
then obtain f where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
34 |
in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
35 |
and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
36 |
by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
37 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
38 |
let ?s = "\<lambda>i. (f ^ i) x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
39 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
40 |
{ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
41 |
fix i |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
42 |
have "\<not>acc R (?s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
43 |
by (induct i) (auto simp:nia `\<not>acc R x`) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
44 |
hence "R (f (?s i)) (?s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
45 |
by (rule in_R) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
46 |
} |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
47 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
48 |
hence "idseq R ?s x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
49 |
unfolding idseq_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
50 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
51 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
52 |
thus ?thesis by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
53 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
54 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
55 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
56 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
57 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
58 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
59 |
types ('a, 'q) cdesc = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
60 |
"('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
61 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
62 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
63 |
fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
64 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
65 |
"in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
66 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
67 |
fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
68 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
69 |
"mk_rel [] x y = False" |
22492 | 70 |
| "mk_rel (c#cs) x y = |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
71 |
(in_cdesc c x y \<or> mk_rel cs x y)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
72 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
73 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
74 |
lemma some_rd: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
75 |
assumes "mk_rel rds x y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
76 |
shows "\<exists>rd\<in>set rds. in_cdesc rd x y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
77 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
78 |
by (induct rds) (auto simp:in_cdesc_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
79 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
80 |
(* from a value sequence, get a sequence of rds *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
81 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
82 |
lemma ex_cs: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
83 |
assumes idseq: "idseq (mk_rel rds) s x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
84 |
shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
85 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
86 |
from idseq |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
87 |
have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
88 |
by (auto simp:idseq_def intro:some_rd) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
89 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
90 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
91 |
by (rule choice) (insert a, blast) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
92 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
93 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
94 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
95 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
96 |
types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
97 |
types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
98 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
99 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
100 |
fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
101 |
('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
102 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
103 |
"stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
104 |
= (\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
105 |
\<longrightarrow> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
106 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
107 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
108 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
109 |
decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
110 |
('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
111 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
112 |
"decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
113 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
114 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
115 |
decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
116 |
('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
117 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
118 |
"decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
119 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
120 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
121 |
no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
122 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
123 |
"no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
124 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
125 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
126 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
127 |
lemma decr_in_cdesc: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
128 |
assumes "in_cdesc RD1 y x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
129 |
assumes "in_cdesc RD2 z y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
130 |
assumes "decr RD1 RD2 m1 m2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
131 |
shows "m2 y < m1 x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
132 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
133 |
by (cases RD1, cases RD2, auto simp:decr_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
134 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
135 |
lemma decreq_in_cdesc: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
136 |
assumes "in_cdesc RD1 y x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
137 |
assumes "in_cdesc RD2 z y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
138 |
assumes "decreq RD1 RD2 m1 m2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
139 |
shows "m2 y \<le> m1 x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
140 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
141 |
by (cases RD1, cases RD2, auto simp:decreq_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
142 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
143 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
144 |
lemma no_inf_desc_nat_sequence: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
145 |
fixes s :: "nat \<Rightarrow> nat" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
146 |
assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
147 |
assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
148 |
shows False |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
149 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
150 |
{ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
151 |
fix i j:: nat |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
152 |
assume "n \<le> i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
153 |
assume "i \<le> j" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
154 |
{ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
155 |
fix k |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
156 |
have "s (i + k) \<le> s i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
157 |
proof (induct k) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
158 |
case 0 thus ?case by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
159 |
next |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
160 |
case (Suc k) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
161 |
with leq[of "i + k"] `n \<le> i` |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
162 |
show ?case by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
163 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
164 |
} |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
165 |
from this[of "j - i"] `n \<le> i` `i \<le> j` |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
166 |
have "s j \<le> s i" by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
167 |
} |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
168 |
note decr = this |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
169 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
170 |
let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
171 |
have "?min \<in> range (\<lambda>i. s (n + i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
172 |
by (rule LeastI) auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
173 |
then obtain k where min: "?min = s (n + k)" by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
174 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
175 |
from less |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
176 |
obtain k' where "n + k < k'" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
177 |
and "s (Suc k') < s k'" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
178 |
unfolding INF_nat by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
179 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
180 |
with decr[of "n + k" k'] min |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
181 |
have "s (Suc k') < ?min" by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
182 |
moreover from `n + k < k'` |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
183 |
have "s (Suc k') = s (n + (Suc k' - n))" by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
184 |
ultimately |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
185 |
show False using not_less_Least by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
186 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
187 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
188 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
189 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
190 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
191 |
approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
192 |
\<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
193 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
194 |
"approx G C C' M M' |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
195 |
= (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
196 |
\<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
197 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
198 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
199 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
200 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
201 |
(* Unfolding "approx" for finite graphs *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
202 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
203 |
lemma approx_empty: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
204 |
"approx (Graph {}) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
205 |
unfolding approx_def has_edge_def dest_graph.simps by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
206 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
207 |
lemma approx_less: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
208 |
assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
209 |
assumes "approx (Graph Es) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
210 |
shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
211 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
212 |
unfolding approx_def has_edge_def dest_graph.simps decr_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
213 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
214 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
215 |
lemma approx_leq: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
216 |
assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
217 |
assumes "approx (Graph Es) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
218 |
shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
219 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
220 |
unfolding approx_def has_edge_def dest_graph.simps decreq_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
221 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
222 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
223 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
224 |
lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
225 |
apply (intro approx_less approx_leq approx_empty) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
226 |
oops |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
227 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
228 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
229 |
(* |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
230 |
fun |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
231 |
no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
232 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
233 |
"no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
234 |
(\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 \<longrightarrow> False)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
235 |
*) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
236 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
237 |
lemma no_stepI: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
238 |
"stepP c1 c2 m1 m2 (\<lambda>x y. False) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
239 |
\<Longrightarrow> no_step c1 c2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
240 |
by (cases c1, cases c2) (auto simp: no_step_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
241 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
242 |
definition |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
243 |
sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
244 |
\<Rightarrow> 'a measures list \<Rightarrow> bool" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
245 |
where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
246 |
"sound_int \<A> RDs M = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
247 |
(\<forall>n<length RDs. \<forall>m<length RDs. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
248 |
no_step (RDs ! n) (RDs ! m) \<or> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
249 |
(\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
250 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
251 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
252 |
(* The following are uses by the tactics *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
253 |
lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
254 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
255 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
256 |
lemma all_less_zero: "\<forall>n<(0::nat). P n" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
257 |
by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
258 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
259 |
lemma all_less_Suc: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
260 |
assumes Pk: "P k" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
261 |
assumes Pn: "\<forall>n<k. P n" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
262 |
shows "\<forall>n<Suc k. P n" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
263 |
proof (intro allI impI) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
264 |
fix n assume "n < Suc k" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
265 |
show "P n" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
266 |
proof (cases "n < k") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
267 |
case True with Pn show ?thesis by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
268 |
next |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
269 |
case False with `n < Suc k` have "n = k" by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
270 |
with Pk show ?thesis by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
271 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
272 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
273 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
274 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
275 |
lemma step_witness: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
276 |
assumes "in_cdesc RD1 y x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
277 |
assumes "in_cdesc RD2 z y" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
278 |
shows "\<not> no_step RD1 RD2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
279 |
using prems |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
280 |
by (cases RD1, cases RD2) (auto simp:no_step_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
281 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
282 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
283 |
theorem SCT_on_relations: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
284 |
assumes R: "R = mk_rel RDs" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
285 |
assumes sound: "sound_int \<A> RDs M" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
286 |
assumes "SCT \<A>" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
287 |
shows "\<forall>x. acc R x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
288 |
proof (rule, rule classical) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
289 |
fix x |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
290 |
assume "\<not> acc R x" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
291 |
with non_acc_has_idseq |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
292 |
have "\<exists>s. idseq R s x" . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
293 |
then obtain s where "idseq R s x" .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
294 |
hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and> |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
295 |
in_cdesc (cs i) (s (Suc i)) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
296 |
unfolding R by (rule ex_cs) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
297 |
then obtain cs where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
298 |
[simp]: "\<And>i. cs i \<in> set RDs" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
299 |
and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
300 |
by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
301 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
302 |
let ?cis = "\<lambda>i. index_of RDs (cs i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
303 |
have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
304 |
\<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
305 |
(M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
306 |
proof |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
307 |
fix i |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
308 |
let ?n = "?cis i" and ?n' = "?cis (Suc i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
309 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
310 |
have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
311 |
"in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
312 |
by (simp_all add:index_of_member) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
313 |
with step_witness |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
314 |
have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
315 |
moreover have |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
316 |
"?n < length RDs" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
317 |
"?n' < length RDs" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
318 |
by (simp_all add:index_of_length[symmetric]) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
319 |
ultimately |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
320 |
obtain G |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
321 |
where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
322 |
and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
323 |
using sound |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
324 |
unfolding sound_int_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
325 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
326 |
thus "\<exists>G. ?P i G" by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
327 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
328 |
with choice |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
329 |
have "\<exists>Gs. \<forall>i. ?P i (Gs i)" . |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
330 |
then obtain Gs where |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
331 |
A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
332 |
and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
333 |
(M ! ?cis i) (M ! ?cis (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
334 |
by blast |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
335 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
336 |
let ?p = "\<lambda>i. (?cis i, Gs i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
337 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
338 |
from A have "has_ipath \<A> ?p" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
339 |
unfolding has_ipath_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
340 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
341 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
342 |
with `SCT \<A>` SCT_def |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
343 |
obtain th where "is_desc_thread th ?p" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
344 |
by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
345 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
346 |
then obtain n |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
347 |
where fr: "\<forall>i\<ge>n. eqlat ?p th i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
348 |
and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
349 |
unfolding is_desc_thread_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
350 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
351 |
from B |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
352 |
have approx: |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
353 |
"\<And>i. approx (Gs i) (cs i) (cs (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
354 |
(M ! ?cis i) (M ! ?cis (Suc i))" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
355 |
by (simp add:index_of_member) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
356 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
357 |
let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
358 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
359 |
have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
360 |
proof - |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
361 |
fix i |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
362 |
let ?q1 = "th i" and ?q2 = "th (Suc i)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
363 |
assume "n < i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
364 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
365 |
with fr have "eqlat ?p th i" by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
366 |
hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
367 |
by simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
368 |
thus "?seq (Suc i) \<le> ?seq i" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
369 |
proof |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
370 |
assume "dsc (Gs i) ?q1 ?q2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
371 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
372 |
with approx |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
373 |
have a:"decr (cs i) (cs (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
374 |
((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
375 |
unfolding approx_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
376 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
377 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
378 |
apply (rule less_imp_le) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
379 |
apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"]) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
380 |
by (rule ird a)+ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
381 |
next |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
382 |
assume "eq (Gs i) ?q1 ?q2" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
383 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
384 |
with approx |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
385 |
have a:"decreq (cs i) (cs (Suc i)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
386 |
((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
387 |
unfolding approx_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
388 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
389 |
show ?thesis |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
390 |
apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"]) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
391 |
by (rule ird a)+ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
392 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
393 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
394 |
moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
395 |
proof |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
396 |
fix i |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
397 |
from inf obtain j where "i < j" and d: "descat ?p th j" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
398 |
unfolding INF_nat by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
399 |
let ?q1 = "th j" and ?q2 = "th (Suc j)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
400 |
from d have "dsc (Gs j) ?q1 ?q2" by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
401 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
402 |
with approx |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
403 |
have a:"decr (cs j) (cs (Suc j)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
404 |
((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
405 |
unfolding approx_def by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
406 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
407 |
have "?seq (Suc j) < ?seq j" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
408 |
apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"]) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
409 |
by (rule ird a)+ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
410 |
with `i < j` |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
411 |
show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
412 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
413 |
ultimately have False |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
414 |
by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
415 |
thus "acc R x" .. |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
416 |
qed |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
417 |
|
22371 | 418 |
end |