text:
chapter \<open>V-Sets, Epsilon Closure, Ranks\<close>

theory Rank imports Ordinal
begin

section \<open>V-sets\<close>

text \<open>Definition 4.1\<close>
definition Vset :: "hf \<Rightarrow> hf"
  where "Vset x = ord_rec 0 HPow (\<lambda>z. 0) x"

lemma Vset_0 [simp]: "Vset 0 = 0"
  by (simp add: Vset_def)

lemma Vset_succ [simp]: "Ord k \<Longrightarrow> Vset (succ k) = HPow (Vset k)"
  by (simp add: Vset_def)

lemma Vset_non [simp]: "\<not> Ord x \<Longrightarrow> Vset x = 0"
  by (simp add: Vset_def)

text \<open>Theorem 4.2(a)\<close>
lemma Vset_mono_strict:
  assumes "Ord m" "n \<^bold>\<in> m" shows "Vset n < Vset m"
proof -
  have n: "Ord n"
    by (metis Ord_in_Ord assms)
  hence "Ord m \<Longrightarrow> n \<^bold>\<in> m \<Longrightarrow> Vset n < Vset m"
  proof (induct n arbitrary: m rule: Ord_induct2)
    case 0 thus ?case
      by (metis HPow_iff Ord_cases Vset_0 Vset_succ hemptyE le_imp_less_or_eq zero_le)
  next
    case (succ n)
    then show ?case using \<open>Ord m\<close>
      by (metis Ord_cases hemptyE HPow_mono_strict_iff Vset_succ mem_succ_iff)
  qed
  thus ?thesis using assms .
qed

lemma Vset_mono: "\<lbrakk>Ord m; n \<le> m\<rbrakk> \<Longrightarrow> Vset n \<le> Vset m"
  by (metis Ord_linear2 Vset_mono_strict Vset_non order.order_iff_strict
            order_class.order.antisym zero_le)

text \<open>Theorem 4.2(b)\<close>
lemma Vset_Transset: "Ord m \<Longrightarrow> Transset (Vset m)"
  by (induct rule: Ord_induct2) (auto simp: Transset_def)

lemma Ord_sup [simp]: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> Ord (k \<squnion> l)"
  by (metis Ord_linear_le le_iff_sup sup_absorb1)

lemma Ord_inf [simp]: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> Ord (k \<sqinter> l)"
  by (metis Ord_linear_le inf_absorb2 le_iff_inf)

text \<open>Theorem 4.3\<close>
lemma Vset_universal: "\<exists>n. Ord n \<and> x \<^bold>\<in> Vset n"
proof (induct x rule: hf_induct)
  case 0 thus ?case
    by (metis HPow_iff Ord_0 Ord_succ Vset_succ zero_le)
next
  case (hinsert a b)
  then obtain na nb where nab: "Ord na" "a \<^bold>\<in> Vset na" "Ord nb" "b \<^bold>\<in> Vset nb"
    by blast
  hence "b \<le> Vset nb" using Vset_Transset [of nb]
    by (auto simp: Transset_def)
  also have "... \<le> Vset (na \<squnion> nb)" using nab
    by (metis Ord_sup Vset_mono sup_ge2)
  finally have "b \<triangleleft> a \<^bold>\<in> Vset (succ (na \<squnion> nb))" using nab
    by simp (metis Ord_sup Vset_mono sup_ge1 rev_hsubsetD)
  thus ?case using nab
    by (metis Ord_succ Ord_sup)
qed

section \<open>Least Ordinal Operator\<close>

text \<open>Definition 4.4. For every x, let rank(x) be the least ordinal n such that...\<close>

lemma Ord_minimal:
   "Ord k \<Longrightarrow> P k \<Longrightarrow> \<exists>n. Ord n \<and> P n \<and> (\<forall>m. Ord m \<and> P m \<longrightarrow> n \<le> m)"
  by (induct k rule: Ord_induct) (metis Ord_linear2)

lemma OrdLeastI: "Ord k \<Longrightarrow> P k \<Longrightarrow> P(LEAST n. Ord n \<and> P n)"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_le: "Ord k \<Longrightarrow> P k \<Longrightarrow> (LEAST n. Ord n \<and> P n) \<le> k"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_Ord:
  assumes "Ord k" "P k"shows "Ord(LEAST n. Ord n \<and> P n)"
proof -
  obtain n where "Ord n" "P n" "\<forall>m. Ord m \<and> P m \<longrightarrow> n \<le> m"
    by (metis Ord_minimal assms)
  thus ?thesis
    by (metis (lifting) Least_equality)
qed

section \<open>Rank Function\<close>

definition rank :: "hf \<Rightarrow> hf"
  where "rank x = (LEAST n. Ord n \<and> x \<^bold>\<in> Vset (succ n))"

lemma in_Vset_rank: "a \<^bold>\<in> Vset(succ(rank a))"
proof -
  from Vset_universal [of a]
  obtain na where na: "Ord na" "a \<^bold>\<in> Vset (succ na)"
    by (metis Ord_Union Ord_in_Ord Ord_pred Vset_0 hempty_iff)
  thus ?thesis
    by (unfold rank_def) (rule OrdLeastI)
qed

lemma Ord_rank [simp]: "Ord (rank a)"
  by (metis Ord_succ_iff Vset_non hemptyE in_Vset_rank)

lemma le_Vset_rank: "a \<le> Vset(rank a)"
  by (metis HPow_iff Ord_succ_iff Vset_non Vset_succ hemptyE in_Vset_rank)

lemma VsetI: "succ(rank a) \<le> k \<Longrightarrow> Ord k \<Longrightarrow> a \<^bold>\<in> Vset k"
  by (metis Vset_mono hsubsetCE in_Vset_rank)

lemma Vset_succ_rank_le: "Ord k \<Longrightarrow> a \<^bold>\<in> Vset (succ k) \<Longrightarrow> rank a \<le> k"
  by (unfold rank_def) (rule OrdLeast_le)

lemma Vset_rank_lt: assumes a: "a \<^bold>\<in> Vset k" shows "rank a < k"
proof -
  { assume k: "Ord k"
    hence ?thesis
    proof (cases k rule: Ord_cases)
      case 0 thus ?thesis using a
        by simp
    next
      case (succ l) thus ?thesis using a
        by (metis Ord_lt_succ_iff_le Ord_succ_iff Vset_non Vset_succ_rank_le hemptyE in_Vset_rank)
    qed
  }
  thus ?thesis using a
    by (metis Vset_non hemptyE)
qed

text \<open>Theorem 4.5\<close>
theorem rank_lt: "a \<^bold>\<in> b \<Longrightarrow> rank(a) < rank(b)"
  by (metis Vset_rank_lt hsubsetD le_Vset_rank)

lemma rank_mono: "x \<le> y \<Longrightarrow> rank x \<le> rank y"
  by (metis HPow_iff Ord_rank Vset_succ Vset_succ_rank_le dual_order.trans le_Vset_rank)

lemma rank_sup [simp]: "rank (a \<squnion> b) = rank a \<squnion> rank b"
proof (rule antisym)
  have o: "Ord (rank a \<squnion> rank b)"
    by simp
  thus "rank (a \<squnion> b) \<le> rank a \<squnion> rank b"
    apply (rule Vset_succ_rank_le, simp)
    apply (metis le_Vset_rank order_trans Vset_mono sup_ge1 sup_ge2 o)
    done
next
  show "rank a \<squnion> rank b \<le> rank (a \<squnion> b)"
    by (metis le_supI le_supI1 le_supI2 order_eq_refl rank_mono)
qed

lemma rank_singleton [simp]: "rank \<lbrace>a\<rbrace> = succ(rank a)"
proof -
  have oba: "Ord (succ (rank a))"
    by simp
  show ?thesis
    proof (rule antisym)
      show "rank \<lbrace>a\<rbrace> \<le> succ (rank a)"
        by (metis Vset_succ_rank_le HPow_iff Vset_succ in_Vset_rank less_eq_insert1_iff oba zero_le)
    next
      show "succ (rank a) \<le> rank\<lbrace>a\<rbrace>"
        by (metis Ord_linear_le Ord_lt_succ_iff_le rank_lt Ord_rank hmem_hinsert less_le_not_le oba)
    qed
qed

lemma rank_hinsert [simp]: "rank (b \<triangleleft> a) = rank b \<squnion> succ(rank a)"
  by (metis hinsert_eq_sup rank_singleton rank_sup)

text \<open>Definition 4.6. The transitive closure of @{term x} is
 the minimal transitive set @{term y} such that @{term"x\<le>y"}.\<close>

section \<open>Epsilon Closure\<close>

definition
  eclose    :: "hf \<Rightarrow> hf"  where
    "eclose X = \<Sqinter> \<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace>"

lemma eclose_facts:
  shows Transset_eclose: "Transset (eclose X)"
   and  le_eclose: "X \<le> eclose X"
proof -
  have nz: "\<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace> \<noteq> 0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  show "Transset (eclose X)" "X \<le> eclose X" using HInter_iff [OF nz]
    by (auto simp: eclose_def Transset_def)
qed

lemma eclose_minimal:
  assumes Y: "Transset Y" "X\<le>Y" shows "eclose X \<le> Y"
proof -
  have "\<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace> \<noteq> 0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  moreover have "Transset (Y \<sqinter> Vset (rank X))"
    by (metis Ord_rank Transset_inf Vset_Transset Y(1))
  moreover have "X \<le> Y \<sqinter> Vset (rank X)"
    by (metis Y(2) le_Vset_rank le_inf_iff)
  ultimately show "eclose X \<le> Y"
    apply (auto simp: eclose_def)
    apply (metis hinter_iff le_inf_iff order_refl)
    done
qed

lemma eclose_0 [simp]: "eclose 0 = 0"
  by (metis Ord_0 Vset_0 Vset_Transset eclose_minimal less_eq_hempty)

lemma eclose_sup [simp]: "eclose (a \<squnion> b) = eclose a \<squnion> eclose b"
proof (rule order_antisym)
  show "eclose (a \<squnion> b) \<le> eclose a \<squnion> eclose b"
    by (metis Transset_eclose Transset_sup eclose_minimal le_eclose sup_mono)
next
  show "eclose a \<squnion> eclose b \<le> eclose (a \<squnion> b)"
    by (metis Transset_eclose eclose_minimal le_eclose le_sup_iff)
qed

lemma eclose_singleton [simp]: "eclose \<lbrace>a\<rbrace> = (eclose a) \<triangleleft> a"
proof (rule order_antisym)
  show "eclose \<lbrace>a\<rbrace> \<le> eclose a \<triangleleft> a"
    by (metis eclose_minimal Transset_eclose Transset_hinsert
              le_eclose less_eq_insert1_iff order_refl zero_le)
next
  show "eclose a \<triangleleft> a \<le> eclose \<lbrace>a\<rbrace>"
    by (metis Transset_def Transset_eclose eclose_minimal le_eclose less_eq_insert1_iff)
qed

lemma eclose_hinsert [simp]: "eclose (b \<triangleleft> a) = eclose b \<squnion> (eclose a \<triangleleft> a)"
  by (metis eclose_singleton eclose_sup hinsert_eq_sup)

lemma eclose_succ [simp]: "eclose (succ a) = eclose a \<triangleleft> a"
  by (auto simp: succ_def)

lemma fst_in_eclose [simp]: "x \<^bold>\<in> eclose \<langle>x, y\<rangle>"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

lemma snd_in_eclose [simp]: "y \<^bold>\<in> eclose \<langle>x, y\<rangle>"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

text \<open>Theorem 4.7. rank(x) = rank(cl(x)).\<close>
lemma rank_eclose [simp]: "rank (eclose x) = rank x"
proof (induct x rule: hf_induct)
  case 0 thus ?case by simp
next
  case (hinsert a b) thus ?case
    by simp (metis hinsert_eq_sup succ_def sup.left_idem)
qed

section \<open>Epsilon-Recursion\<close>

text \<open>Theorem 4.9.  Definition of a function by recursion on rank.\<close>

lemma hmem_induct [case_names step]:
  assumes ih: "\<And>x. (\<And>y. y \<^bold>\<in> x \<Longrightarrow> P y) \<Longrightarrow> P x" shows "P x"
proof -
  have "\<And>y. y \<^bold>\<in> x \<Longrightarrow> P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case by simp
  next
    case (hinsert a b) thus ?case
      by (metis assms hmem_hinsert)
  qed
  thus ?thesis by (metis ih)
qed

definition
  hmem_rel :: "(hf * hf) set" where
  "hmem_rel = trancl {(x,y). x \<^bold>\<in> y}"

lemma wf_hmem_rel: "wf hmem_rel"
proof -
  have "wf {(x,y). x \<^bold>\<in> y}"
    by (metis (full_types) hmem_induct wfPUNIVI wfP_def)
  thus ?thesis
    by (metis hmem_rel_def wf_trancl)
qed

lemma hmem_eclose_le: "y \<^bold>\<in> x \<Longrightarrow> eclose y \<le> eclose x"
  by (metis Transset_def Transset_eclose eclose_minimal hsubsetD le_eclose)

lemma hmem_rel_iff_hmem_eclose: "(x,y) \<in> hmem_rel \<longleftrightarrow> x \<^bold>\<in> eclose y"
proof (unfold hmem_rel_def, rule iffI)
  assume "(x, y) \<in> trancl {(x, y). x \<^bold>\<in> y}"
  thus "x \<^bold>\<in> eclose y"
    proof (induct rule: trancl_induct)
      case (base y) thus ?case
        by (metis hsubsetCE le_eclose mem_Collect_eq split_conv)
    next
      case (step y z) thus ?case
        by (metis hmem_eclose_le hsubsetD mem_Collect_eq split_conv)
    qed
next
  have "Transset \<lbrace>x \<^bold>\<in> eclose y. (x, y) \<in> hmem_rel\<rbrace>" using Transset_eclose
    by (auto simp: Transset_def hmem_rel_def intro: trancl_trans)
  hence "eclose y \<le> \<lbrace>x \<^bold>\<in> eclose y. (x, y) \<in> hmem_rel\<rbrace>"
    by (rule eclose_minimal) (auto simp: le_HCollect_iff le_eclose hmem_rel_def)
  moreover assume "x \<^bold>\<in> eclose y"
  ultimately show "(x, y) \<in> trancl {(x, y). x \<^bold>\<in> y}"
    by (metis HCollect_iff hmem_rel_def hsubsetD)
qed

definition hmemrec :: "((hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> 'a" where
  "hmemrec G \<equiv> wfrec hmem_rel G"

definition ecut :: "(hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> hf \<Rightarrow> 'a" where
  "ecut f x \<equiv> (\<lambda>y. if y \<^bold>\<in> eclose x then f y else undefined)"

lemma hmemrec: "hmemrec G a = G (ecut (hmemrec G) a) a"
  by (simp add: cut_def ecut_def hmem_rel_iff_hmem_eclose def_wfrec [OF hmemrec_def wf_hmem_rel])

text \<open>This form avoids giant explosions in proofs.\<close>
lemma def_hmemrec: "f \<equiv> hmemrec G \<Longrightarrow> f a = G (ecut (hmemrec G) a) a"
  by (metis hmemrec)

lemma ecut_apply: "y \<^bold>\<in> eclose x \<Longrightarrow> ecut f x y = f y"
  by (metis ecut_def)

lemma RepFun_ecut: "y \<le> z \<Longrightarrow> RepFun y (ecut f z) = RepFun y f"
  apply (auto simp: hf_ext)
  apply (metis ecut_def hsubsetD le_eclose)
  apply (metis ecut_apply le_eclose hsubsetD)
  done

text \<open>Now, a stronger induction rule, for the transitive closure of membership\<close>
lemma hmem_rel_induct [case_names step]:
  assumes ih: "\<And>x. (\<And>y. (y,x) \<in> hmem_rel \<Longrightarrow> P y) \<Longrightarrow> P x" shows "P x"
proof -
  have "\<And>y. (y,x) \<in> hmem_rel \<Longrightarrow> P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case
      by (metis eclose_0 hmem_hempty hmem_rel_iff_hmem_eclose)
  next
    case (hinsert a b)
    thus ?case
      by (metis assms eclose_hinsert hmem_hinsert hmem_rel_iff_hmem_eclose hunion_iff)
  qed
  thus ?thesis  by (metis assms)
qed

lemma rank_HUnion_less:  "x \<noteq> 0 \<Longrightarrow> rank (\<Squnion>x) < rank x"
  apply (induct x rule: hf_induct, auto)
  apply (metis hmem_hinsert rank_hinsert rank_lt)
  apply (metis HUnion_hempty Ord_lt_succ_iff_le Ord_rank hunion_hempty_right
               less_supI1 less_supI2 rank_sup sup.cobounded2)
  done

corollary Sup_ne: "x \<noteq> 0 \<Longrightarrow> \<Squnion>x \<noteq> x"
  by (metis less_irrefl rank_HUnion_less)

end

repo: PSL


text:
theory T117
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(x, join(y, z)) = join(undr(x, y), undr(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(x, meet(y, z)) = join(over(x, y), over(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(meet(x, y), z) = join(undr(x, z), undr(y, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z)))
"
nitpick[card nat=8,timeout=86400]
oops
end

author: inpefess

repo: residuated-binars


text:
(*  Title:      HOL/MicroJava/BV/JVM.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

section \<open>Kildall for the JVM \label{sec:JVM}\<close>

theory BVExec
imports
  "../DFA/Abstract_BV"
  TF_JVM
begin

definition kiljvm :: "'addr jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow>
                    'addr instr list \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> ty\<^sub>i' err list"
where
  "kiljvm P mxs mxl T\<^sub>r is xt \<equiv>
  kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
          (exec P mxs T\<^sub>r xt is)"

definition  wt_kildall :: "'addr jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
                         'addr instr list \<Rightarrow> ex_table \<Rightarrow> bool"
where
  "wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv>
   0 < size is \<and>
   (let first  = Some ([],[OK (Class C')]@(map OK Ts)@(replicate mxl\<^sub>0 Err));
        start  = OK first#(replicate (size is - 1) (OK None));
        result = kiljvm P mxs (1+size Ts+mxl\<^sub>0) T\<^sub>r is xt  start
    in \<forall>n < size is. result!n \<noteq> Err)"

definition wf_jvm_prog\<^sub>k :: "'addr jvm_prog \<Rightarrow> bool"
where
  "wf_jvm_prog\<^sub>k P \<equiv>
  wf_prog (\<lambda>P C' (M,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt) P"

theorem (in start_context) is_bcv_kiljvm:
  "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
(*<*)
  apply (insert wf)
  apply (unfold kiljvm_def)
  apply (fold r_def f_def step_def_exec)
  apply (rule is_bcv_kildall)
       apply simp
       apply (rule Semilat.intro)
       apply (fold sl_def2, erule semilat_JVM)
      apply simp
      apply blast
     apply (simp add: JVM_le_unfold)
    apply (rule exec_pres_type)
   apply (rule bounded_step)
  apply (erule step_mono)
  done
(*>*)

(* FIXME: move? *)
lemma subset_replicate [intro?]: "set (replicate n x) \<subseteq> {x}"
  by (induct n) auto

lemma in_set_replicate:
  assumes "x \<in> set (replicate n y)"
  shows "x = y"
(*<*)
proof -
  note assms
  also have "set (replicate n y) \<subseteq> {y}" ..
  finally show ?thesis by simp
qed
(*>*)

lemma (in start_context) start_in_A [intro?]:
  "0 < size is \<Longrightarrow> start \<in> list (size is) A"
  using Ts C
(*<*)
  apply (simp add: JVM_states_unfold)
  apply (force intro!: listI list_appendI dest!: in_set_replicate)
  done
(*>*)

theorem (in start_context) wt_kil_correct:
  assumes wtk: "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
  shows "\<exists>\<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
(*<*)
proof -
  from wtk obtain res where
    result:   "res = kiljvm P mxs mxl T\<^sub>r is xt start" and
    success:  "\<forall>n < size is. res!n \<noteq> Err" and
    instrs:   "0 < size is"
    by (unfold wt_kildall_def) simp

  have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
    by (rule is_bcv_kiljvm)

  from instrs have "start \<in> list (size is) A" ..
  with bcv success result have
    "\<exists>ts\<in>list (size is) A. start [\<sqsubseteq>\<^sub>r] ts \<and> wt_step r Err step ts"
    by (unfold is_bcv_def) blast
  then obtain \<tau>s' where
    in_A: "\<tau>s' \<in> list (size is) A" and
    s:    "start [\<sqsubseteq>\<^sub>r] \<tau>s'" and
    w:    "wt_step r Err step \<tau>s'"
    by blast
  hence wt_err_step: "wt_err_step (sup_state_opt P) step \<tau>s'"
    by (simp add: wt_err_step_def JVM_le_Err_conv)

  from in_A have l: "size \<tau>s' = size is" by simp
  moreover {
    from in_A  have "check_types P mxs mxl \<tau>s'" by (simp add: check_types_def)
    also from w have "\<forall>x \<in> set \<tau>s'. x \<noteq> Err"
      by (auto simp add: wt_step_def all_set_conv_all_nth)
    hence [symmetric]: "map OK (map ok_val \<tau>s') = \<tau>s'"
      by (auto intro!: map_idI simp add: wt_step_def)
    finally  have "check_types P mxs mxl (map OK (map ok_val \<tau>s'))" .
  }
  moreover {
    from s have "start!0 \<sqsubseteq>\<^sub>r \<tau>s'!0" by (rule le_listD) simp
    moreover
    from instrs w l
    have "\<tau>s'!0 \<noteq> Err" by (unfold wt_step_def) simp
    then obtain \<tau>s0 where "\<tau>s'!0 = OK \<tau>s0" by auto
    ultimately
    have "wt_start P C Ts mxl\<^sub>0 (map ok_val \<tau>s')" using l instrs
      by (unfold wt_start_def)
         (simp add: lesub_def JVM_le_Err_conv Err.le_def)
  }
  moreover
  from in_A have "set \<tau>s' \<subseteq> A" by simp
  with wt_err_step bounded_step
  have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s')"
    by (auto intro: wt_err_imp_wt_app_eff simp add: l)
  ultimately
  have "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s')"
    using instrs by (simp add: wt_method_def2 check_types_def del: map_map)
  thus ?thesis by blast
qed
(*>*)

theorem (in start_context) wt_kil_complete:
  assumes wtm: "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
  shows "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
(*<*)
proof -
  from wtm obtain
    instrs:   "0 < size is" and
    length:   "length \<tau>s = length is" and
    ck_type:  "check_types P mxs mxl (map OK \<tau>s)" and
    wt_start: "wt_start P C Ts mxl\<^sub>0 \<tau>s" and
    app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"
    by (simp add: wt_method_def2 check_types_def)

  from ck_type
  have in_A: "set (map OK \<tau>s) \<subseteq> A"
    by (simp add: check_types_def)
  with app_eff in_A bounded_step
  have "wt_err_step (sup_state_opt P) (err_step (size \<tau>s) app eff) (map OK \<tau>s)"
    by - (erule wt_app_eff_imp_wt_err,
          auto simp add: exec_def length states_def)
  hence wt_err: "wt_err_step (sup_state_opt P) step (map OK \<tau>s)"
    by (simp add: length)
  have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
    by (rule is_bcv_kiljvm)
  moreover from instrs have "start \<in> list (size is) A" ..
  moreover
  let ?\<tau>s = "map OK \<tau>s"
  have less_\<tau>s: "start [\<sqsubseteq>\<^sub>r] ?\<tau>s"
  proof (rule le_listI)
    from length instrs
    show "length start = length (map OK \<tau>s)" by simp
  next
    fix n
    from wt_start have "P \<turnstile> ok_val (start!0) \<le>' \<tau>s!0"
      by (simp add: wt_start_def)
    moreover from instrs length have "0 < length \<tau>s" by simp
    ultimately have "start!0 \<sqsubseteq>\<^sub>r ?\<tau>s!0"
      by (simp add: JVM_le_Err_conv lesub_def)
    moreover {
      fix n'
      have "OK None \<sqsubseteq>\<^sub>r ?\<tau>s!n"
        by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
                 split: err.splits)
      hence "\<lbrakk>n = Suc n'; n < size start\<rbrakk> \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by simp
    }
    ultimately
    show "n < size start \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by (cases n, blast+)
  qed
  moreover
  from ck_type length
  have "?\<tau>s \<in> list (size is) A"
    by (auto intro!: listI simp add: check_types_def)
  moreover
  from wt_err have "wt_step r Err step ?\<tau>s"
    by (simp add: wt_err_step_def JVM_le_Err_conv)
  ultimately
  have "\<forall>p. p < size is \<longrightarrow> kiljvm P  mxs mxl T\<^sub>r is xt start ! p \<noteq> Err"
    by (unfold is_bcv_def) blast
  with instrs
  show "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt" by (unfold wt_kildall_def) simp
qed
(*>*)

theorem jvm_kildall_correct:
  "wf_jvm_prog\<^sub>k P = wf_jvm_prog P"
(*<*)
proof
  let ?\<Phi> = "\<lambda>C M. let (C,Ts,T\<^sub>r,meth) = method P C M; (mxs,mxl\<^sub>0,is,xt) = the meth in
              SOME \<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"

  \<comment> \<open>soundness\<close>
  assume wt: "wf_jvm_prog\<^sub>k P"
  hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P"
    apply (unfold wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)
    apply (erule wf_prog_lift)
    apply (auto intro: someI_ex[OF start_context.wt_kil_correct [OF start_context.intro]])
    done
  thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
next
  \<comment> \<open>completeness\<close>
  assume wt: "wf_jvm_prog P"
  thus "wf_jvm_prog\<^sub>k P"
    apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)
    apply (clarify)
    apply (erule wf_prog_lift)
    apply (auto intro!: start_context.wt_kil_complete start_context.intro)
    done
qed
(*>*)

end


text:
theory ArityAnalysisSig
imports "../Launchbury/Terms" AEnv "Arity-Nominal" "../Launchbury/Nominal-HOLCF"  "../Launchbury/Substitution"
begin

locale ArityAnalysis =
  fixes Aexp :: "exp \<Rightarrow> Arity \<rightarrow> AEnv"
begin
  abbreviation Aexp_syn ("\<A>\<^bsub>_\<^esub>")where "\<A>\<^bsub>a\<^esub> e \<equiv> Aexp e\<cdot>a"
  abbreviation Aexp_bot_syn ("\<A>\<^sup>\<bottom>\<^bsub>_\<^esub>")
    where "\<A>\<^sup>\<bottom>\<^bsub>a\<^esub> e \<equiv> fup\<cdot>(Aexp e)\<cdot>a"

end

locale ArityAnalysisHeap =
  fixes Aheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> AEnv"

locale EdomArityAnalysis = ArityAnalysis +
  assumes Aexp_edom: "edom (\<A>\<^bsub>a\<^esub> e) \<subseteq> fv e"
begin

  lemma fup_Aexp_edom: "edom (\<A>\<^sup>\<bottom>\<^bsub>a\<^esub> e) \<subseteq> fv e"
    by (cases a) (auto dest:set_mp[OF Aexp_edom])

  lemma Aexp_fresh_bot[simp]: assumes "atom v \<sharp> e" shows "\<A>\<^bsub>a\<^esub> e v = \<bottom>"
  proof-
    from assms have "v \<notin> fv e" by (metis fv_not_fresh)
    with Aexp_edom have "v \<notin> edom (\<A>\<^bsub>a\<^esub> e)" by auto
    thus ?thesis unfolding edom_def by simp
  qed
end

locale ArityAnalysisHeapEqvt = ArityAnalysisHeap +
  assumes Aheap_eqvt[eqvt]: "\<pi> \<bullet> Aheap = Aheap"

end

author: nomeata

repo: isa-launchbury