src/HOL/Library/SCT_Interpretation.thy

Added formalization of size-change principle (experimental).

theory SCT_Interpretation
imports Main SCT_Misc SCT_Definition
begin


definition
  "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"

lemma not_acc_smaller:
  assumes notacc: "\<not> acc R x"
  shows "\<exists>y. R y x \<and> \<not> acc R y"
proof (rule classical)
  assume "\<not> ?thesis"
  hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast
  with accI have "acc R x" .
  with notacc show ?thesis by contradiction
qed

lemma non_acc_has_idseq:
  assumes "\<not> acc R x"
  shows "\<exists>s. idseq R s x"
proof -
  
  have	"\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)"
	by (rule choice, auto simp:not_acc_smaller)
  
  then obtain f where
	in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x"
	and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)"
	by blast
  
  let ?s = "\<lambda>i. (f ^ i) x"
  
  {
	fix i
	have "\<not>acc R (?s i)"
	  by (induct i) (auto simp:nia `\<not>acc R x`)
	hence "R (f (?s i)) (?s i)"
	  by (rule in_R)
  }
  
  hence "idseq R ?s x"
	unfolding idseq_def
	by auto
  
  thus ?thesis by auto
qed





types ('a, 'q) cdesc =
  "('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)"


fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
  "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)"

fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
  "mk_rel [] x y = False"
  "mk_rel (c#cs) x y =
  (in_cdesc c x y \<or> mk_rel cs x y)"


lemma some_rd:
  assumes "mk_rel rds x y"
  shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
  using prems
  by (induct rds) (auto simp:in_cdesc_def)

(* from a value sequence, get a sequence of rds *)

lemma ex_cs:
  assumes idseq: "idseq (mk_rel rds) s x"
  shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)"
proof -
  from idseq
  have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)"
	by (auto simp:idseq_def intro:some_rd)
  
  show ?thesis
	by (rule choice) (insert a, blast)
qed



types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)"
types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat"


fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool"
where
  "stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R
  = (\<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> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))"


definition
  decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
where
  "decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)"

definition
  decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
where
  "decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)"

definition
  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
where
  "no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)"



lemma decr_in_cdesc:
  assumes	"in_cdesc RD1 y x"
  assumes "in_cdesc RD2 z y"
  assumes "decr RD1 RD2 m1 m2"
  shows "m2 y < m1 x"
  using prems
  by (cases RD1, cases RD2, auto simp:decr_def)

lemma decreq_in_cdesc:
  assumes	"in_cdesc RD1 y x"
  assumes "in_cdesc RD2 z y"
  assumes "decreq RD1 RD2 m1 m2"
  shows "m2 y \<le> m1 x"
  using prems
  by (cases RD1, cases RD2, auto simp:decreq_def)


lemma no_inf_desc_nat_sequence:
  fixes s :: "nat \<Rightarrow> nat"
  assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i"
  assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i"
  shows False
proof -
  {
	fix i j:: nat 
	assume "n \<le> i"
	assume "i \<le> j"
	{
	  fix k 
	  have "s (i + k) \<le> s i"
	  proof (induct k)
		case 0 thus ?case by simp
	  next
		case (Suc k)
		with leq[of "i + k"] `n \<le> i`
		show ?case by simp
	  qed
	}
	from this[of "j - i"] `n \<le> i` `i \<le> j`
	have "s j \<le> s i" by auto
  }
  note decr = this
  
  let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))"
  have "?min \<in> range (\<lambda>i. s (n + i))"
	by (rule LeastI) auto
  then obtain k where min: "?min = s (n + k)" by auto
  
  from less 
  obtain k' where "n + k < k'"
	and "s (Suc k') < s k'"
	unfolding INF_nat by auto
  
  with decr[of "n + k" k'] min
  have "s (Suc k') < ?min" by auto
  moreover from `n + k < k'`
  have "s (Suc k') = s (n + (Suc k' - n))" by simp
  ultimately
  show False using not_less_Least by blast
qed



definition
  approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc 
  \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
  where
  "approx G C C' M M'
  = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
  \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))"




(* Unfolding "approx" for finite graphs *)

lemma approx_empty: 
  "approx (Graph {}) c1 c2 ms1 ms2"
  unfolding approx_def has_edge_def dest_graph.simps by simp

lemma approx_less:
  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
  assumes "approx (Graph Es) c1 c2 ms1 ms2"
  shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
  using prems
  unfolding approx_def has_edge_def dest_graph.simps decr_def
  by auto

lemma approx_leq:
  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
  assumes "approx (Graph Es) c1 c2 ms1 ms2"
  shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
  using prems
  unfolding approx_def has_edge_def dest_graph.simps decreq_def
  by auto


lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2"
  apply (intro approx_less approx_leq approx_empty) 
  oops


(*
fun
  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
where
  "no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) =
  (\<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)"
*)

lemma no_stepI:
  "stepP c1 c2 m1 m2 (\<lambda>x y. False)
  \<Longrightarrow> no_step c1 c2"
by (cases c1, cases c2) (auto simp: no_step_def)

definition
  sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list 
  \<Rightarrow> 'a measures list \<Rightarrow> bool"
where
  "sound_int \<A> RDs M =
  (\<forall>n<length RDs. \<forall>m<length RDs.
  no_step (RDs ! n) (RDs ! m) \<or>
  (\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))"


(* The following are uses by the tactics *)
lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)"
  by auto

lemma all_less_zero: "\<forall>n<(0::nat). P n"
  by simp

lemma all_less_Suc:
  assumes Pk: "P k"
  assumes Pn: "\<forall>n<k. P n"
  shows "\<forall>n<Suc k. P n"
proof (intro allI impI)
  fix n assume "n < Suc k"
  show "P n"
  proof (cases "n < k")
    case True with Pn show ?thesis by simp
  next
    case False with `n < Suc k` have "n = k" by simp
    with Pk show ?thesis by simp
  qed
qed


lemma step_witness:
  assumes "in_cdesc RD1 y x"
  assumes "in_cdesc RD2 z y"
  shows "\<not> no_step RD1 RD2"
  using prems
  by (cases RD1, cases RD2) (auto simp:no_step_def)


theorem SCT_on_relations:
  assumes R: "R = mk_rel RDs"
  assumes sound: "sound_int \<A> RDs M"
  assumes "SCT \<A>"
  shows "\<forall>x. acc R x"
proof (rule, rule classical)
  fix x
  assume "\<not> acc R x"
  with non_acc_has_idseq	
  have "\<exists>s. idseq R s x" .
  then obtain s where "idseq R s x" ..
  hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and>
	in_cdesc (cs i) (s (Suc i)) (s i)"
	unfolding R by (rule ex_cs) 
  then obtain cs where
	[simp]: "\<And>i. cs i \<in> set RDs"
	  and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)"
	by blast
  
  let ?cis = "\<lambda>i. index_of RDs (cs i)"
  have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i)))
	\<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
	(M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G")
  proof
	fix i
	let ?n = "?cis i" and ?n' = "?cis (Suc i)"
    
	have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)"
	  "in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))"
	  by (simp_all add:index_of_member)
	with step_witness
 	have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" .
	moreover have
	  "?n < length RDs" 
	  "?n' < length RDs"
	  by (simp_all add:index_of_length[symmetric])
	ultimately
	obtain G
	  where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'"
	  and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')"
	  using sound
	  unfolding sound_int_def by auto
    
	thus "\<exists>G. ?P i G" by blast
  qed
  with choice
  have "\<exists>Gs. \<forall>i. ?P i (Gs i)" .
  then obtain Gs where 
	A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))" 
	and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
	(M ! ?cis i) (M ! ?cis (Suc i))"
	by blast
  
  let ?p = "\<lambda>i. (?cis i, Gs i)"
  
  from A have "has_ipath \<A> ?p"
	unfolding has_ipath_def
	by auto
  
  with `SCT \<A>` SCT_def 
  obtain th where "is_desc_thread th ?p"
	by auto
  
  then obtain n
	where fr: "\<forall>i\<ge>n. eqlat ?p th i"
	and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i"
	unfolding is_desc_thread_def by auto
  
  from B
  have approx:
	"\<And>i. approx (Gs i) (cs i) (cs (Suc i)) 
	(M ! ?cis i) (M ! ?cis (Suc i))"
	by (simp add:index_of_member)
  
  let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)"
  
  have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i"
  proof -
	fix i 
	let ?q1 = "th i" and ?q2 = "th (Suc i)"
	assume "n < i"
	
	with fr	have "eqlat ?p th i" by simp 
	hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2" 
      by simp
	thus "?seq (Suc i) \<le> ?seq i"
	proof
	  assume "dsc (Gs i) ?q1 ?q2"
	  
	  with approx
	  have a:"decr (cs i) (cs (Suc i)) 
		((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
		unfolding approx_def by auto
      
	  show ?thesis
		apply (rule less_imp_le)
		apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
		by (rule ird a)+
	next
	  assume "eq (Gs i) ?q1 ?q2"
	  
	  with approx
	  have a:"decreq (cs i) (cs (Suc i)) 
		((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
		unfolding approx_def by auto
      
	  show ?thesis
		apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"])
		by (rule ird a)+
	qed
  qed
  moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat
  proof 
	fix i 
	from inf obtain j where "i < j" and d: "descat ?p th j"
	  unfolding INF_nat by auto
	let ?q1 = "th j" and ?q2 = "th (Suc j)"
	from d have "dsc (Gs j) ?q1 ?q2" by auto
	
	with approx
	have a:"decr (cs j) (cs (Suc j)) 
	  ((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)" 
	  unfolding approx_def by auto
    
	have "?seq (Suc j) < ?seq j"
	  apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"])
	  by (rule ird a)+
	with `i < j` 
	show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto
  qed
  ultimately have False
    by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp
  thus "acc R x" ..
qed


end