src/HOL/MicroJava/BV/Kildall_Lift.thy

tuned;

(*  Title:      HOL/MicroJava/BV/Kildall_Lift.thy
    ID:         $Id$
    Author:     Gerwin Klein
    Copyright   2001 TUM
*)

theory Kildall_Lift = Kildall + Typing_Framework_err:

constdefs
 app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
"app_mono r app n A ==
 \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"

 succs_stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> bool"
"succs_stable r step == \<forall>p t t'. map fst (step p t') = map fst (step p t)"

lemma succs_stableD:
  "succs_stable r step \<Longrightarrow> map fst (step p t) = map fst (step p t')"
  by (unfold succs_stable_def) blast

lemma eqsub_def [simp]: "a <=_(op =) b = (a = b)" by (simp add: lesub_def)

lemma list_le_eq [simp]: "\<And>b. a <=[op =] b = (a = b)"
apply (induct a) 
 apply simp
 apply rule
  apply simp
 apply simp
apply (case_tac b)
 apply simp
apply simp
done

lemma map_err: "map_err a = zip (map fst a) (map (\<lambda>x. Err) (map snd a))"
apply (induct a)
apply (auto simp add: map_err_def map_snd_def)
done

lemma map_snd: "map_snd f a = zip (map fst a) (map f (map snd a))"
apply (induct a)
apply (auto simp add: map_snd_def)
done

lemma zipI: 
  "\<And>b c d. a <=[r1] c \<Longrightarrow> b <=[r2] d \<Longrightarrow> zip a b <=[Product.le r1 r2] zip c d"
apply (induct a)
 apply simp
apply (case_tac c)
 apply simp
apply (case_tac b)
 apply simp
apply (case_tac d)
 apply simp
apply simp
done

lemma step_type_ord: 
  "\<And>b. a <=|r| b \<Longrightarrow> map snd a <=[r] map snd b \<and> map fst a = map fst b"
apply (induct a)
 apply simp
apply (case_tac b)
 apply simp
apply simp
apply (auto simp add: Product.le_def lesub_def)
done

lemma map_OK_Err: 
  "\<And>y. length y = length x \<Longrightarrow> map OK x <=[Err.le r] map (\<lambda>x. Err) y"
apply (induct x)
 apply simp
apply simp
apply (case_tac y)
apply auto
done

lemma map_Err_Err:
  "\<And>b. length a = length b \<Longrightarrow> map (\<lambda>x. Err) a <=[Err.le r] map (\<lambda>x. Err) b"
apply (induct a)
 apply simp
apply (case_tac b)
apply auto
done

lemma succs_stable_length: 
  "succs_stable r step \<Longrightarrow> length (step p t) = length (step p t')"
proof -
  assume "succs_stable r step"  
  hence "map fst (step p t) = map fst (step p t')" by (rule succs_stableD)
  hence "length (map fst (step p t)) = length (map fst (step p t'))" by simp
  thus ?thesis by simp
qed

lemma le_list_map_OK [simp]:
  "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
  apply (induct a)
   apply simp
  apply simp
  apply (case_tac b)
   apply simp
  apply simp
  done

lemma mono_lift:
  "order r \<Longrightarrow> succs_stable r step \<Longrightarrow> app_mono r app n A \<Longrightarrow> 
  \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
  mono (Err.le r) (err_step app step) n (err A)"
apply (unfold app_mono_def mono_def err_step_def)
apply clarify
apply (case_tac s)
 apply simp
 apply (rule le_list_refl)
 apply simp
apply simp
apply (subgoal_tac "map fst (step p arbitrary) = map fst (step p a)")
 prefer 2
 apply (erule succs_stableD)
apply (case_tac t)
 apply simp
 apply (rule conjI)
  apply clarify
  apply (simp add: map_err map_snd)
  apply (rule zipI)
   apply simp
  apply (rule map_OK_Err)
  apply (subgoal_tac "length (step p arbitrary) = length (step p a)")
   prefer 2
   apply (erule succs_stable_length)
  apply simp
 apply clarify
 apply (simp add: map_err)
 apply (rule zipI)
  apply simp
 apply (rule map_Err_Err)
 apply simp
 apply (erule succs_stable_length)
apply simp
apply (elim allE)
apply (erule impE, blast)+
apply (rule conjI)
 apply clarify
 apply (simp add: map_snd)
 apply (rule zipI)
  apply simp
  apply (erule succs_stableD)
 apply (simp add: step_type_ord)
apply clarify
apply (rule conjI)
 apply clarify
 apply (simp add: map_snd map_err)
 apply (rule zipI)
  apply simp
  apply (erule succs_stableD)
 apply (rule map_OK_Err)
 apply (simp add: succs_stable_length)
apply clarify
apply (simp add: map_err)
apply (rule zipI)
 apply simp
 apply (erule succs_stableD)
apply (rule map_Err_Err)
apply (simp add: succs_stable_length)
done
 
lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
apply (induct xs)
apply (auto simp add: map_snd_def)
done

lemma bounded_lift:
  "bounded (err_step app step) n = bounded step n"
apply (unfold bounded_def err_step_def)
apply rule
apply clarify
 apply (erule allE, erule impE, assumption)
 apply (erule_tac x = "OK s" in allE)
 apply simp
 apply (case_tac "app p s")
  apply (simp add: map_snd_def)
  apply (drule bspec, assumption)
  apply simp
 apply (simp add: map_err_def map_snd_def)
 apply (drule bspec, assumption)
 apply simp
apply clarify
apply (case_tac s)
 apply simp
 apply (simp add: map_err_def)
 apply (blast dest: in_map_sndD)
apply (simp split: split_if_asm)
 apply (blast dest: in_map_sndD)
apply (simp add: map_err_def)
apply (blast dest: in_map_sndD)
done

lemma set_zipD: "\<And>y. (a,b) \<in> set (zip x y) \<Longrightarrow> (a \<in> set x \<and> b \<in> set y)"
apply (induct x)
 apply simp
apply (case_tac y)
 apply simp
apply simp
apply blast
done

lemma pres_type_lift:
  "\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A) 
  \<Longrightarrow> pres_type (err_step app step) n (err A)"  
apply (unfold pres_type_def err_step_def)
apply clarify
apply (case_tac b)
 apply simp
apply (case_tac s)
 apply (simp add: map_err)
 apply (drule set_zipD)
 apply clarify
 apply simp
 apply blast
apply (simp add: map_err split: split_if_asm)
 apply (simp add: map_snd_def)
 apply fastsimp
apply (drule set_zipD)
apply simp
apply blast
done

end