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
```