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