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