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