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