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