text:
theory Apply_Pure
  imports Registers.Pure_States
begin

lemma clinear_option_case_aux: \<open>clinear X \<Longrightarrow> X (case t of Some u \<Rightarrow> f u | None \<Rightarrow> g) \<equiv> (case t of Some u \<Rightarrow> X (f u) | None \<Rightarrow> X g)\<close> for X
  apply (rule eq_reflection)
  by (simp add: option.case_eq_if)

ML \<open>
local
open Conv
open Type
val move_clinear_down_rules = @{thms
  complex_vector.linear_add[THEN eq_reflection]
  complex_vector.linear_diff[THEN eq_reflection]
  complex_vector.linear_sum[THEN eq_reflection]
  clinear.scaleC[THEN eq_reflection]
  clinear_option_case_aux
}
;;
;;
fun has_head ctxt head cterm = let
  (* val cterm = cterm |> Thm.beta_conversion true |> Thm.rhs_of *)
  val idx = Thm.maxidx_of_cterm cterm
  val head_argT = fastype_of head |> Term.dest_funT |> fst
  val pat = Term.betapply (head, Var(("x",idx+1), head_argT))
  val match = SOME (Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, Thm.term_of cterm)
                      (Vartab.empty, Vartab.empty))
          handle Pattern.MATCH => NONE
  (* val _ = \<^print> (cterm |> Thm.term_of, pat, match) *)
  in Option.isSome match end

(* Converts only a toplevel "head $ stuff" *)
fun move_clinear_down_conv' ctxt head conv : conv =
  ((fn ct => conv ct handle CTERM ("no conversion",_) =>
    ((* \<^print> ("no conv", ct); *) raise CTERM ("move_clinear_down_conv: no matching rules", [ct])))
  then_conv
  (sub_conv (fn ctxt => move_clinear_down_conv'' ctxt head conv |> try_conv) ctxt)) (* #> (fn x => (\<^print> ("conv'", x); x)) *)
(* Converts "head $ stuff" anywhere in term *)
and move_clinear_down_conv'' ctxt head (conv:conv) (cterm:cterm) : thm =
  (if has_head ctxt head cterm then ((* tracing "head"; \<^print> cterm; *) move_clinear_down_conv' ctxt head conv cterm)
  else ((* tracing "sub"; \<^print> cterm; *) Conv.sub_conv (fn ctxt => move_clinear_down_conv'' ctxt head conv) ctxt cterm))
     (* |> (fn x => (\<^print> ("conv''", cterm, x); x)) *)
in
fun move_clinear_down_conv ctxt (subterm:bool) head_clinear_thm cterm : thm = let
  val head = (case Thm.prop_of head_clinear_thm of
            Const(\<^const_name>\<open>Trueprop\<close>, _) $ (Const(\<^const_name>\<open>clinear\<close>,_) $ head') => head'
            | _ => raise THM ("move_clinear_down_conv: head_clinear_thm must be of the form 'clinear \<dots>'", 0, [head_clinear_thm]))
  val _ = subterm orelse has_head ctxt head cterm orelse
          let val head_dots = betapply (head, Var(("dddot",0),dummyT))
          in raise CTERM ("move_clinear_down_conv: term must be of the form '" ^ Syntax.string_of_term ctxt head_dots ^ "'", [cterm]) end

  val rules = move_clinear_down_rules |> map (fn rule => rule OF [head_clinear_thm])
  val conv = Conv.rewrs_conv rules
  (* val _ = rules |> \<^print> *)
  val thm = (if subterm then move_clinear_down_conv'' else move_clinear_down_conv') ctxt head conv cterm
  (* val _ = thm |> \<^print> *)
in thm end
fun move_clinear_down_tac ctxt head_clinear_thm = CONVERSION (move_clinear_down_conv ctxt true head_clinear_thm)
end
\<close>

ML \<open>
local
open Conv
in
fun apply_to_pure_states_conv focus_thm compatible_thm apply_thm = let
  val state_apply1 = @{thm state_apply1[THEN eq_reflection]} OF [compatible_thm]
  val clinear_thm = @{thm pure_state_clinear} OF [compatible_thm]
  val unfocus_thm = Thm.symmetric focus_thm
  val _ = unfocus_thm |> \<^print>
  in
    fn ctxt =>
    (fn ct => (\<^print> ct; all_conv ct))
    then_conv
    (rewr_conv focus_thm |> arg_conv)
    then_conv
    rewr_conv state_apply1
    then_conv
    (rewr_conv apply_thm |> arg1_conv |> arg1_conv)
    then_conv
    (move_clinear_down_conv ctxt false clinear_thm)
    then_conv
    (top_sweep_rewrs_conv [unfocus_thm] ctxt)
  end
fun apply_to_pure_states_tac focus_thm compatible_thm apply_thm ctxt =
  CONVERSION (top_sweep_conv (apply_to_pure_states_conv focus_thm compatible_thm apply_thm) ctxt)
end
\<close>

lemma pure_state_id: \<open>pure_state id \<psi> = \<psi>\<close>
proof -
  have \<open>ket default \<in> range ((*\<^sub>V) (selfbutterket default))\<close>
    by (metis (mono_tags, opaque_lifting) butterfly_apply cinner_ket_same rangeI scaleC_one)
  then show ?thesis
    apply (simp add: pure_state'_def id_def pure_state_target_vector_ket_default)
    apply (subst pure_state_target_vector_ket_default)
    by auto
qed

end

author: dominique-unruh

repo: luby-rackoff-formalization


text:
(*  Author:      Lukas Bulwahn, TU Muenchen, 2009  *)

theory Execute
imports FJSound
begin

section \<open>Executing FeatherweightJava programs\<close>
text \<open>We execute FeatherweightJava programs using the predicate compiler.\<close>

code_pred (modes: i => i => i => bool,
  i => i => o => bool as supertypes_of) subtyping .

thm subtyping.equation

text \<open>The reduction relation requires that we inverse the @{term List.append} function.
Therefore, we define a new predicate append and derive introduction rules.\<close>

definition append where "append xs ys zs = (zs = xs @ ys)"

lemma [code_pred_intro]: "append [] xs xs"
unfolding append_def by simp

lemma [code_pred_intro]: "append xs ys zs \<Longrightarrow> append (x#xs) ys (x#zs)"
unfolding append_def by simp

text \<open>With this at hand, we derive new introduction rules for the reduction relation:\<close>

lemma rc_invk_arg': "CT \<turnstile> ei \<rightarrow> ei' \<Longrightarrow> append el (ei # er) e' \<Longrightarrow> append el (ei' # er) e'' \<Longrightarrow>
CT \<turnstile> MethodInvk e m e' \<rightarrow> MethodInvk e m e''"
unfolding append_def by simp (rule reduction.intros(6))

lemma rc_new_arg': "CT \<turnstile> ei \<rightarrow> ei' \<Longrightarrow> append el (ei # er) e \<Longrightarrow> append el (ei' # er) e'
   ==> CT \<turnstile> New C e \<rightarrow> New C e'"
unfolding append_def by simp (rule reduction.intros(7))

lemmas [code_pred_intro] = reduction.intros(1-5)
  rc_invk_arg' rc_new_arg' reduction.intros(8)

code_pred (modes: i => i => i => bool, i => i => o => bool as reduce) reduction
proof -
  case append
  from this show thesis
    unfolding append_def by (cases xa) fastforce+
next
  case reduction
  from reduction.prems show thesis
  proof (cases rule: reduction.cases)
    case r_field
    with reduction(1) show thesis by fastforce
  next
    case r_invk
    with reduction(2) show thesis by fastforce
  next
    case r_cast
    with reduction(3) show thesis by fastforce
  next
    case rc_field
    with reduction(4) show thesis by fastforce
  next
    case rc_invk_recv
    with reduction(5) show thesis by fastforce
  next
    case rc_invk_arg
    with reduction(6) show thesis
      unfolding append_def by fastforce
  next
    case rc_new_arg
    with reduction(7) show thesis
      unfolding append_def by fastforce
  next
    case rc_cast
    with reduction(8) show thesis by fastforce
  qed
qed

thm reduction.equation

code_pred reductions .

thm reductions.equation

text \<open>We also make the class typing executable: this requires that
  we derive rules for @{term "method_typing"}.\<close>

definition method_typing_aux
where
  "method_typing_aux CT m D Cs C = (\<not> (\<forall>Ds D0. mtype(CT,m,D) = Ds \<rightarrow> D0 \<longrightarrow> Cs = Ds \<and> C = D0))"

lemma method_typing_aux:
  "(\<forall>Ds D0. mtype(CT,m,D) = Ds \<rightarrow> D0 \<longrightarrow> Cs = Ds \<and> C = D0) = (\<not> method_typing_aux CT m D Cs C)"
unfolding method_typing_aux_def by auto

lemma [code_pred_intro]:
  "mtype(CT,m,D) = Ds \<rightarrow> D0 \<Longrightarrow> Cs \<noteq> Ds \<Longrightarrow> method_typing_aux CT m D Cs C"
unfolding method_typing_aux_def by auto

lemma [code_pred_intro]:
  "mtype(CT,m,D) = Ds \<rightarrow> D0 \<Longrightarrow> C \<noteq> D0 \<Longrightarrow> method_typing_aux CT m D Cs C"
unfolding method_typing_aux_def by auto

declare method_typing.intros[unfolded method_typing_aux, code_pred_intro]

declare class_typing.intros[unfolded append_def[symmetric], code_pred_intro]

code_pred (modes: i => i => bool) class_typing
proof -
  case class_typing
  from class_typing.cases[OF class_typing.prems, of thesis] this(1) show thesis
    unfolding append_def by fastforce
next
  case method_typing
  from method_typing.cases[OF method_typing.prems, of thesis] this(1) show thesis
    unfolding append_def method_typing_aux_def by fastforce
next
  case method_typing_aux
  from this show thesis
    unfolding method_typing_aux_def by auto
qed

subsection \<open>A simple example\<close>

text \<open>We now execute a simple FJ example program:\<close>

abbreviation A :: className
where "A == Suc 0"

abbreviation B :: className
where "B == 2"

abbreviation cPair :: className
where "cPair == 3"

definition classA_Def :: classDef
where
  "classA_Def = \<lparr> cName = A, cSuper = Object, cFields = [], cConstructor = \<lparr>kName = A, kParams = [], kSuper = [], kInits = []\<rparr>, cMethods = []\<rparr>"

definition
  "classB_Def = \<lparr> cName = B, cSuper = Object, cFields = [], cConstructor = \<lparr>kName = B, kParams = [], kSuper = [], kInits = []\<rparr>, cMethods = []\<rparr>"

abbreviation ffst :: varName
where
  "ffst == 4"

abbreviation fsnd :: varName
where
  "fsnd == 5"

abbreviation setfst :: methodName
where
  "setfst == 6"

abbreviation newfst :: varName
where
  "newfst == 7"

definition classPair_Def :: classDef
where
  "classPair_Def = \<lparr> cName = cPair, cSuper = Object,
    cFields = [\<lparr> vdName = ffst, vdType = Object \<rparr>, \<lparr> vdName = fsnd, vdType = Object \<rparr>],
    cConstructor = \<lparr> kName = cPair, kParams = [\<lparr> vdName = ffst, vdType = Object \<rparr>, \<lparr> vdName = fsnd, vdType = Object \<rparr>], kSuper = [], kInits = [ffst, fsnd]\<rparr> ,
    cMethods = [\<lparr> mReturn = cPair, mName = setfst, mParams = [\<lparr>vdName = newfst, vdType = Object \<rparr>],
      mBody = New cPair [Var newfst, FieldProj (Var this) fsnd]  \<rparr>]\<rparr>"

definition exampleProg :: classTable
  where "exampleProg = (((%x. None)(A := Some classA_Def))(B := Some classB_Def))(cPair := Some classPair_Def)"

value "exampleProg \<turnstile> classA_Def OK"
value "exampleProg \<turnstile> classB_Def OK"
value "exampleProg \<turnstile> classPair_Def OK"

values "{x. exampleProg \<turnstile> MethodInvk (New cPair [New A [], New B []]) setfst [New B []] \<rightarrow>* x}"
values "{x. exampleProg \<turnstile> FieldProj (FieldProj (New cPair [New cPair [New A [], New B []], New A []]) ffst) fsnd \<rightarrow>* x}"

end

repo: PSL


text:
(*  Title:      HOL/Auth/n_flash_nodata_cub_lemma_inv__4_on_rules.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

header{*The n_flash_nodata_cub Protocol Case Study*}

theory n_flash_nodata_cub_lemma_inv__4_on_rules imports n_flash_nodata_cub_lemma_on_inv__4
begin
section{*All lemmas on causal relation between inv__4*}
lemma lemma_inv__4_on_rules:
  assumes b1: "r \<in> rules N" and b2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__4  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  proof -
  have c1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_Get  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_PI_Remote_GetX  src)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_PI_Remote_PutX  dst)\<or>
    (\<exists> src. src\<le>N\<and>r=n_PI_Remote_Replace  src)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Nak  dst)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__0  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__1  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__2  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__0  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Dirty  src)\<or>
    (\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Nak  src dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst)\<or>
    (\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Put  src dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__0  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__1  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__2  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__0  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__1  src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src)\<or>
    (\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp)\<or>
    (\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src)\<or>
    (\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src)\<or>
    (\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_Nak  src dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst)\<or>
    (\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_PutX  src dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Put  dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_PutX  dst)\<or>
    (\<exists> dst. dst\<le>N\<and>r=n_NI_Inv  dst)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_InvAck_exists_Home  src)\<or>
    (\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_InvAck_exists  src pp)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_InvAck_1 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_InvAck_2 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_InvAck_3 N src)\<or>
    (\<exists> src. src\<le>N\<and>r=n_NI_Replace  src)\<or>
    (r=n_PI_Local_Get_Get  )\<or>
    (r=n_PI_Local_Get_Put  )\<or>
    (r=n_PI_Local_GetX_GetX__part__0  )\<or>
    (r=n_PI_Local_GetX_GetX__part__1  )\<or>
    (r=n_PI_Local_GetX_PutX_HeadVld__part__0 N )\<or>
    (r=n_PI_Local_GetX_PutX_HeadVld__part__1 N )\<or>
    (r=n_PI_Local_GetX_PutX__part__0  )\<or>
    (r=n_PI_Local_GetX_PutX__part__1  )\<or>
    (r=n_PI_Local_PutX  )\<or>
    (r=n_PI_Local_Replace  )\<or>
    (r=n_NI_Nak_Home  )\<or>
    (r=n_NI_Nak_Clear  )\<or>
    (r=n_NI_Local_Put  )\<or>
    (r=n_NI_Local_PutXAcksDone  )\<or>
    (r=n_NI_Wb  )\<or>
    (r=n_NI_FAck  )\<or>
    (r=n_NI_ShWb N )\<or>
    (r=n_NI_Replace_Home  )"
  apply (cut_tac b1, auto) done
    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_Get  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Remote_GetVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_GetX  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Remote_GetXVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_PI_Remote_PutX  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Remote_PutXVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_Replace  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Remote_ReplaceVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Nak  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_NakVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__0  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Nak__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__1  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Nak__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__2  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Nak__part__2Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__0  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Get__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Get__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Put_HeadVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_PutVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Dirty  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_Get_Put_DirtyVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Nak  src dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_Get_NakVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_Get_Nak_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Put  src dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_Get_PutVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_Get_Put_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__0  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_Nak__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__1  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_Nak__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__2  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_Nak__part__2Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__0  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_GetX__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__1  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_GetX__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_2Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_3Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_4Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_5Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_6Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_7__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_7__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_7_NODE_Get__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_7_NODE_Get__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_8_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_8_Home_NODE_GetVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_8Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_8_NODE_GetVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_9__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_9__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_10_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_10Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_GetX_PutX_11Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_Nak  src dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_GetX_NakVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_GetX_Nak_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_PutX  src dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_GetX_PutXVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_GetX_PutX_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Put  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_PutVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_PutX  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Remote_PutXVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Inv  dst)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_InvAck_exists_Home  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvAck_exists_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_InvAck_exists  src pp)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvAck_existsVsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_InvAck_1 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvAck_1Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_InvAck_2 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvAck_2Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_InvAck_3 N src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_InvAck_3Vsinv__4) done
    }

    moreover {
      assume d1: "(\<exists> src. src\<le>N\<and>r=n_NI_Replace  src)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_ReplaceVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_Get_Get  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_Get_GetVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_Get_Put  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_Get_PutVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_GetX__part__0  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_GetX__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_GetX__part__1  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_GetX__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_PutX_HeadVld__part__0 N )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_PutX_HeadVld__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_PutX_HeadVld__part__1 N )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_PutX_HeadVld__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_PutX__part__0  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_PutX__part__0Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_GetX_PutX__part__1  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_GetX_PutX__part__1Vsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_PutX  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_PutXVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_PI_Local_Replace  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_PI_Local_ReplaceVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Nak_Home  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Nak_HomeVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Nak_Clear  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Nak_ClearVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Local_Put  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_PutVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Local_PutXAcksDone  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Local_PutXAcksDoneVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Wb  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_WbVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_FAck  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_FAckVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_ShWb N )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_ShWbVsinv__4) done
    }

    moreover {
      assume d1: "(r=n_NI_Replace_Home  )"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_NI_Replace_HomeVsinv__4) done
    }

  ultimately show "invHoldForRule s f r (invariants N)"
  by satx
qed

end

author: paraVerifier

repo: paraVerifier


text:
theory RCCDagstuhl2_NN_T
imports "$HETS_ISABELLE_LIB/MainHC"
begin

ML_file "$HETS_ISABELLE_LIB/prelude.ML"

setup "Header.initialize
       [\"Ax1\", \"C_def\", \"EMSCB_center\", \"EMSCB_closed\",
        \"EMSCB_rep_pos\", \"EMSCB_rep_0\", \"EMSCB_rep_inj\", \"Ax4\",
        \"MS_pos\", \"MS_zero\", \"MS_pos_definite\", \"MS_symm\",
        \"MS_triangle\", \"one_greater_zero\", \"zero_leq_one\",
        \"half_gt_zero\", \"half_plus_minus\", \"add_monotone\",
        \"sub_leq\", \"half_leq\", \"half_leq_zero\", \"comm_add\",
        \"Real_half_plus\", \"Real_half_minus\", \"Real_minus_half\",
        \"Real_half_monot\", \"Real_abs_def\", \"Real_sqr_def\",
        \"Real_sqrt_dom\", \"Real_sqrt_idef\", \"Real_2_def\",
        \"Real_minus_def\", \"Real_divide_dom\", \"Real_divide_idef\",
        \"Real_half_idef\", \"Real_ub_def\", \"Real_lb_def\",
        \"Real_inf_def\", \"Real_sup_def\", \"Real_isBounded_def\",
        \"completeness\", \"Real_inj_0\", \"Real_inj_suc\",
        \"Real_archimedian\", \"FWO_plus_right\", \"FWO_times_right\",
        \"FWO_plus\", \"FWO_plus_left\", \"FWO_times_left\",
        \"Field_unary_minus_idef\", \"dichotomy_TotalOrder\", \"antisym\",
        \"trans\", \"refl\", \"min_inf_relation\", \"max_sup_relation\",
        \"ga_comm_min\", \"ga_comm_max\", \"ga_assoc_min\",
        \"ga_assoc_max\", \"ga_left_comm_min\", \"ga_left_comm_max\",
        \"min_def_ExtTotalOrder\", \"max_def_ExtTotalOrder\",
        \"ga_comm_inf\", \"ga_comm_sup\", \"inf_def_ExtPartialOrder\",
        \"sup_def_ExtPartialOrder\", \"geq_def_ExtPartialOrder\",
        \"less_def_ExtPartialOrder\", \"greater_def_ExtPartialOrder\",
        \"C_non_null\", \"C_sym\", \"C_id\", \"C_non_triv\"]"

typedecl ClosedBall
typedecl Real
typedecl S

datatype X_Nat = X0X1 ("0''") | X_suc "X_Nat" ("suc/'(_')" [3] 999)

consts
X0X2 :: "Real" ("0''''")
X1 :: "Real" ("1''")
X2 :: "Real" ("2''")
XMinus__X :: "Real => Real" ("(-''/ _)" [56] 56)
XVBar__XVBar :: "Real => Real" ("(|/ _/ |)" [10] 999)
X__C__X :: "ClosedBall => ClosedBall => bool" ("(_/ C/ _)" [44,44] 42)
X__XGtXEq__X :: "Real => Real => bool" ("(_/ >=''/ _)" [44,44] 42)
X__XGt__X :: "Real => Real => bool" ("(_/ >''/ _)" [44,44] 42)
X__XLtXEq__XX1 :: "Real => Real => bool" ("(_/ <=''/ _)" [44,44] 42)
X__XLtXEq__XX2 :: "Real => (Real => bool) => bool" ("(_/ <=''''/ _)" [44,44] 42)
X__XLtXEq__XX3 :: "(Real => bool) => Real => bool" ("(_/ <='_3/ _)" [44,44] 42)
X__XLt__X :: "Real => Real => bool" ("(_/ <''/ _)" [44,44] 42)
X__XMinus__X :: "Real => Real => Real" ("(_/ -''/ _)" [54,54] 52)
X__XPlus__X :: "Real => Real => Real" ("(_/ +''/ _)" [54,54] 52)
X__XSlash__X :: "Real => Real => Real partial" ("(_/ '/''/ _)" [54,54] 52)
X__Xx__X :: "Real => Real => Real" ("(_/ *''/ _)" [54,54] 52)
X_closedBall :: "S => Real => ClosedBall" ("closedBall/'(_,/ _')" [3,3] 999)
X_d :: "S => S => Real" ("d/'(_,/ _')" [3,3] 999)
X_half :: "Real => Real" ("half/'(_')" [3] 999)
X_inj :: "X_Nat => Real" ("inj''/'(_')" [3] 999)
X_isBounded :: "(Real => bool) => bool" ("isBounded/'(_')" [3] 999)
X_max :: "Real => Real => Real" ("max''/'(_,/ _')" [3,3] 999)
X_min :: "Real => Real => Real" ("min''/'(_,/ _')" [3,3] 999)
X_nonempty :: "ClosedBall => bool" ("nonempty/'(_')" [3] 999)
infX1 :: "Real => Real => Real partial" ("inf''/'(_,/ _')" [3,3] 999)
infX2 :: "(Real => bool) => Real partial" ("inf''''/'(_')" [3] 999)
rep :: "ClosedBall => S => bool"
sqr__X :: "Real => Real" ("(sqr/ _)" [56] 56)
sqrt__X :: "Real => Real partial" ("(sqrt/ _)" [56] 56)
supX1 :: "Real => Real => Real partial" ("sup''/'(_,/ _')" [3,3] 999)
supX2 :: "(Real => bool) => Real partial" ("sup''''/'(_')" [3] 999)

axiomatization
where
Ax1 [rule_format] : "ALL (x :: ClosedBall). nonempty(x) = (x C x)"
and
C_def [rule_format] :
"ALL (x :: ClosedBall).
 ALL (y :: ClosedBall). (x C y) = (EX (s :: S). rep x s & rep y s)"
and
EMSCB_center [rule_format] :
"ALL (r :: Real).
 ALL (x :: S). r >' 0'' --> rep (closedBall(x, r)) x"
and
EMSCB_closed [rule_format] :
"ALL (a :: ClosedBall).
 ALL (x :: S).
 ~ rep a x -->
 (EX (r :: Real).
  ALL (y :: S). ~ (rep (closedBall(x, r)) y & ~ rep a y))"
and
EMSCB_rep_pos [rule_format] :
"ALL (r :: Real).
 ALL (x :: S).
 ALL (y :: S).
 r >' 0'' --> rep (closedBall(x, r)) y = (d(x, y) <=' r)"
and
EMSCB_rep_0 [rule_format] :
"ALL (r :: Real).
 ALL (x :: S).
 ALL (y :: S). ~ r >' 0'' --> ~ rep (closedBall(x, r)) y"
and
EMSCB_rep_inj [rule_format] :
"ALL (a :: ClosedBall).
 ALL (b :: ClosedBall). rep a = rep b --> a = b"
and
Ax4 [rule_format] :
"ALL (a :: ClosedBall).
 EX (z :: S). EX (t :: Real). a = closedBall(z, t)"
and
MS_pos [rule_format] :
"ALL (x :: S). ALL (y :: S). 0'' <=' d(x, y)"
and
MS_zero [rule_format] : "ALL (x :: S). d(x, x) = 0''"
and
MS_pos_definite [rule_format] :
"ALL (x :: S). ALL (y :: S). d(x, y) = 0'' = (x = y)"
and
MS_symm [rule_format] :
"ALL (x :: S). ALL (y :: S). d(x, y) = d(y, x)"
and
MS_triangle [rule_format] :
"ALL (x :: S).
 ALL (y :: S). ALL (z :: S). d(x, z) <=' d(x, y) +' d(y, z)"
and
one_greater_zero [rule_format] : "1' >' 0''"
and
zero_leq_one [rule_format] : "0'' <=' 1'"
and
half_gt_zero [rule_format] :
"ALL (r :: Real). r >' 0'' --> half(r) >' 0''"
and
half_plus_minus [rule_format] :
"ALL (r :: Real).
 ALL (s :: Real). r <=' s --> s +' half(r -' s) <=' s"
and
add_monotone [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real).
 ALL (c :: Real).
 ALL (e :: Real). a <=' b & c <=' e --> a +' c <=' b +' e"
and
sub_leq [rule_format] :
"ALL (a :: Real). ALL (b :: Real). ~ a <=' b --> a -' b >' 0''"
and
half_leq [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real). a <=' half(a -' b) +' b --> a <=' b"
and
half_leq_zero [rule_format] :
"ALL (r :: Real). 0'' <=' r --> 0'' <=' half(r)"
and
comm_add [rule_format] :
"ALL (a :: Real). ALL (b :: Real). a +' b = b +' a"
and
Real_half_plus [rule_format] :
"ALL (r :: Real).
 ALL (s :: Real). half(r +' s) = half(r) +' half(s)"
and
Real_half_minus [rule_format] :
"ALL (r :: Real).
 ALL (s :: Real). half(r -' s) = half(r) -' half(s)"
and
Real_minus_half [rule_format] :
"ALL (r :: Real). r -' half(r) = half(r)"
and
Real_half_monot [rule_format] :
"ALL (r :: Real).
 ALL (s :: Real). (half(r) <=' half(s)) = (r <=' s)"
and
Real_abs_def [rule_format] :
"ALL (r :: Real). | r | = max'(r, -' r)"
and
Real_sqr_def [rule_format] : "ALL (r :: Real). sqr r = r *' r"
and
Real_sqrt_dom [rule_format] :
"ALL (r :: Real). defOp (sqrt r) = (r >=' 0'')"
and
Real_sqrt_idef [rule_format] :
"ALL (r :: Real). sqrt sqr r = makePartial ( | r | )"
and
Real_2_def [rule_format] : "2' = 1' +' 1'"
and
Real_minus_def [rule_format] :
"ALL (r :: Real). ALL (r' :: Real). r -' r' = r +' -' r'"
and
Real_divide_dom [rule_format] :
"ALL (r :: Real). ~ defOp (r /' 0'')"
and
Real_divide_idef [rule_format] :
"ALL (r :: Real).
 ALL (r' :: Real).
 ALL (r'' :: Real).
 (~ r' = 0'' --> r /' r' = makePartial r'') = (r'' *' r' = r)"
and
Real_half_idef [rule_format] : "ALL (r :: Real). 2' *' half(r) = r"
and
Real_ub_def [rule_format] :
"ALL (M :: Real => bool).
 ALL (r :: Real). (M <=_3 r) = (ALL (s :: Real). M s --> s <=' r)"
and
Real_lb_def [rule_format] :
"ALL (M :: Real => bool).
 ALL (r :: Real). (r <='' M) = (ALL (s :: Real). M s --> r <=' s)"
and
Real_inf_def [rule_format] :
"ALL (M :: Real => bool).
 ALL (r :: Real).
 inf''(M) = makePartial r =
 (r <='' M & (ALL (s :: Real). s <='' M --> s <=' r))"
and
Real_sup_def [rule_format] :
"ALL (M :: Real => bool).
 ALL (r :: Real).
 sup''(M) = makePartial r =
 (M <=_3 r & (ALL (s :: Real). M <=_3 s --> r <=' s))"
and
Real_isBounded_def [rule_format] :
"ALL (M :: Real => bool).
 isBounded(M) =
 (EX (ub :: Real). EX (lb :: Real). lb <='' M & M <=_3 ub)"
and
completeness [rule_format] :
"ALL (M :: Real => bool).
 isBounded(M) --> defOp (inf''(M)) & defOp (sup''(M))"
and
Real_inj_0 [rule_format] : "inj'(0') = 0''"
and
Real_inj_suc [rule_format] :
"ALL (X_n :: X_Nat). inj'(suc(X_n)) = 1' +' inj'(X_n)"
and
Real_archimedian [rule_format] :
"ALL (r :: Real). EX (X_n :: X_Nat). r <=' inj'(X_n)"
and
FWO_plus_right [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real). ALL (c :: Real). b <=' c --> a +' b <=' a +' c"
and
FWO_times_right [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real).
 ALL (c :: Real). b <=' c & 0'' <=' a --> a *' b <=' a *' c"
and
FWO_plus [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real).
 ALL (c :: Real).
 ALL (X_d :: Real). a <=' c & b <=' X_d --> a +' b <=' c +' X_d"
and
FWO_plus_left [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real). ALL (c :: Real). a <=' b --> a +' c <=' b +' c"
and
FWO_times_left [rule_format] :
"ALL (a :: Real).
 ALL (b :: Real).
 ALL (c :: Real). a <=' b & 0'' <=' c --> a *' c <=' b *' c"
and
Field_unary_minus_idef [rule_format] :
"ALL (x :: Real). -' x +' x = 0''"
and
dichotomy_TotalOrder [rule_format] :
"ALL (x :: Real). ALL (y :: Real). x <=' y | y <=' x"
and
antisym [rule_format] :
"ALL (x :: Real). ALL (y :: Real). x <=' y & y <=' x --> x = y"
and
trans [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real). ALL (z :: Real). x <=' y & y <=' z --> x <=' z"
and
refl [rule_format] : "ALL (x :: Real). x <=' x"
and
min_inf_relation [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real). makePartial (min'(x, y)) = inf'(x, y)"
and
max_sup_relation [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real). makePartial (max'(x, y)) = sup'(x, y)"
and
ga_comm_min [rule_format] :
"ALL (x :: Real). ALL (y :: Real). min'(x, y) = min'(y, x)"
and
ga_comm_max [rule_format] :
"ALL (x :: Real). ALL (y :: Real). max'(x, y) = max'(y, x)"
and
ga_assoc_min [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real). min'(min'(x, y), z) = min'(x, min'(y, z))"
and
ga_assoc_max [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real). max'(max'(x, y), z) = max'(x, max'(y, z))"
and
ga_left_comm_min [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real). min'(x, min'(y, z)) = min'(y, min'(x, z))"
and
ga_left_comm_max [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real). max'(x, max'(y, z)) = max'(y, max'(x, z))"
and
min_def_ExtTotalOrder [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real). min'(x, y) = (if x <=' y then x else y)"
and
max_def_ExtTotalOrder [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real). max'(x, y) = (if x <=' y then y else x)"
and
ga_comm_inf [rule_format] :
"ALL (x :: Real). ALL (y :: Real). inf'(x, y) = inf'(y, x)"
and
ga_comm_sup [rule_format] :
"ALL (x :: Real). ALL (y :: Real). sup'(x, y) = sup'(y, x)"
and
inf_def_ExtPartialOrder [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real).
 inf'(x, y) = makePartial z =
 (z <=' x &
  z <=' y & (ALL (t :: Real). t <=' x & t <=' y --> t <=' z))"
and
sup_def_ExtPartialOrder [rule_format] :
"ALL (x :: Real).
 ALL (y :: Real).
 ALL (z :: Real).
 sup'(x, y) = makePartial z =
 (x <=' z &
  y <=' z & (ALL (t :: Real). x <=' t & y <=' t --> z <=' t))"
and
geq_def_ExtPartialOrder [rule_format] :
"ALL (x :: Real). ALL (y :: Real). (x >=' y) = (y <=' x)"
and
less_def_ExtPartialOrder [rule_format] :
"ALL (x :: Real). ALL (y :: Real). (x <' y) = (x <=' y & ~ x = y)"
and
greater_def_ExtPartialOrder [rule_format] :
"ALL (x :: Real). ALL (y :: Real). (x >' y) = (y <' x)"

declare EMSCB_rep_pos [simp]
declare EMSCB_center [simp]
declare EMSCB_rep_0 [simp]
declare MS_pos [simp]
declare MS_zero [simp]
declare MS_pos_definite [simp]
declare MS_triangle [simp]
declare one_greater_zero [simp]
declare zero_leq_one [simp]
declare half_plus_minus [simp]
declare sub_leq [simp]
declare half_leq_zero [simp]
declare Real_minus_half [simp]
declare Real_half_monot [simp]
declare Real_divide_dom [simp]
declare Real_half_idef [simp]
declare completeness [simp]
declare Real_inj_0 [simp]
declare FWO_plus_right [simp]
declare FWO_plus_left [simp]
declare Field_unary_minus_idef [simp]
declare refl [simp]
declare min_inf_relation [simp]
declare max_sup_relation [simp]
declare ga_comm_min [simp]
declare ga_comm_max [simp]
declare ga_assoc_min [simp]
declare ga_assoc_max [simp]
declare ga_left_comm_min [simp]
declare ga_left_comm_max [simp]
declare ga_comm_inf [simp]
declare ga_comm_sup [simp]

theorem C_non_null :
"ALL (x :: ClosedBall). ALL (y :: ClosedBall). x C y --> x C x"
using C_def
by (auto)

setup "Header.record \"C_non_null\""

theorem C_sym :
"ALL (x :: ClosedBall). ALL (y :: ClosedBall). x C y --> y C x"
using C_def
by (auto)

setup "Header.record \"C_sym\""

lemma impLemma : "[| A; A==>B; B-->D|] ==> D"
by auto

lemma reflLemma : "x=y ==> x <=' y"
using refl by auto

lemma MS_triangle_rev :
"d(x, z) <=' (d(x, y) +' d(z, y))"
by (simp add: MS_symm)

lemma EMSCB_rep_pos1 : "rep (closedBall(x, r)) y \<Longrightarrow> r >' 0'' \<longrightarrow> d(x, y) <=' r"
by auto

lemma C_id_lemma : "!!x y xa.
       ALL z. (EX s. rep z s & rep x s) = (EX s. rep z s & rep y s)
       ==> rep x xa ==> rep y xa"
apply (erule contrapos_pp)
apply (subst not_all)
apply (insert Ax4 [THEN allI, of "%x. x"])
apply (frule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (erule exE)+
apply (subst not_iff)
apply (case_tac "ta >' 0''")
apply (rule_tac x="closedBall(xa, half (d(za, xa) -' ta))" in exI)
apply(auto)
apply(drule EMSCB_rep_pos1)+
apply(rule_tac P="d(za, xa) <=' ta" in notE)
apply(assumption)
apply(rule half_leq)
apply(rule trans)
apply(rule conjI)
defer
apply(rule add_monotone)
apply(rule conjI)
apply(erule mp)
back
apply(insert sub_leq)
apply(rule half_gt_zero)
apply(rule sub_leq)
apply(assumption+)

apply(rule_tac x="xa" in exI)
apply simp
apply(rule EMSCB_rep_pos [THEN iffD2])
apply(rule half_gt_zero)
apply(rule sub_leq)
apply(assumption)
apply simp
apply(rule half_leq_zero)
apply(drule sub_leq)
apply(simp add: greater_def_ExtPartialOrder
                less_def_ExtPartialOrder)
apply(rule trans)
apply(rule conjI)
defer
apply(rule MS_triangle_rev)
apply(rule reflLemma)
apply(rule MS_symm)
done

theorem C_id :
"ALL (x :: ClosedBall).
 ALL (y :: ClosedBall).
 (ALL (z :: ClosedBall). (z C x) = (z C y)) --> x = y"
apply (auto simp add: C_def)
apply (rule EMSCB_rep_inj)
apply (rule ext)
apply (auto)
apply (rule_tac x="x" in C_id_lemma)
apply(auto)
apply (rule_tac x="y" in C_id_lemma)
apply(auto)
done

setup "Header.record \"C_id\""

theorem C_non_triv : "EX (x :: ClosedBall). x C x"
apply (simp add: C_def)
apply (rule exI)+
apply (rule EMSCB_rep_pos [THEN iffD2])
apply(rule one_greater_zero)
apply(rule iffD2)
apply(rule arg_cong)
back
back
defer
apply(rule zero_leq_one)
apply auto
done

setup "Header.record \"C_non_triv\""

end

author: spechub

repo: Hets-lib

save_path: github-repos/isabelle/spechub-Hets-lib


text:
section "Soundness of the declarative semantics wrt. operational"

theory DenotSoundFSet
  imports SmallStepLam BigStepLam ChangeEnv
begin

subsection "Substitution preserves denotation"

lemma subst_app: "subst x v (EApp e1 e2) = EApp (subst x v e1) (subst x v e2)"
  by auto

lemma subst_prim: "subst x v (EPrim f e1 e2) = EPrim f (subst x v e1) (subst x v e2)"
  by auto

lemma subst_lam_eq: "subst x v (ELam x e) = ELam x e" by auto

lemma subst_lam_neq: "y \<noteq> x \<Longrightarrow> subst x v (ELam y e) = ELam y (subst x v e)" by simp

lemma subst_if: "subst x v (EIf e1 e2 e3) = EIf (subst x v e1) (subst x v e2) (subst x v e3)"
  by auto

lemma subst_cons: "subst x v (ECons e1 e2) = ECons (subst x v e1) (subst x v e2)"
  by auto

lemma subst_car: "subst x v (ECar e) = ECar (subst x v e)"
  by auto

lemma subst_cdr: "subst x v (ECdr e) = ECdr (subst x v e)"
  by auto

lemma substitution:
  fixes \<Gamma>::env and A::val
  assumes wte: "B \<in> E e \<Gamma>'" and wtv: "A \<in> E v []"
    and gp: "\<Gamma>' \<approx> (x,A)#\<Gamma>" and v: "is_val v"
  shows "B \<in> E (subst x v e) \<Gamma>"
  using wte wtv gp v
proof (induction arbitrary: v A B \<Gamma> x rule: E.induct)
  case (1 n \<rho>)
  then show ?case by auto
next
  case (2 x \<rho> v A B \<Gamma> x')
  then show ?case
    apply (simp only: env_eq_def)
    apply (cases "x = x'")
     apply simp apply clarify
     apply (rule env_strengthen)
      apply (rule e_sub)
       apply auto
    done
next
  case (3 x e \<rho> v A B \<Gamma> x')
  then show ?case
    apply (case_tac "x' = x") apply (simp only: subst_lam_eq)
     apply (rule env_strengthen) apply assumption apply (simp add: env_eq_def)
    apply (simp only: subst_lam_neq) apply (erule e_lam_elim)
    apply (rule e_lam_intro)
     apply assumption apply clarify apply (erule_tac x=v1 in allE) apply (erule_tac x=v2 in allE)
    apply clarify
    apply (subgoal_tac "(x,v1)#\<rho> \<approx> (x',A)#(x,v1)#\<Gamma>")
     prefer 2 apply (simp add: env_eq_def)
    apply blast
    done
next
  case (4 e1 e2 \<rho>)
  then show ?case
    apply (simp only: subst_app)
    apply (erule e_app_elim)
    apply (rule e_app_intro)
        apply auto
    done
next
  case (5 f e1 e2 \<rho>)
  then show ?case
    apply (simp only: subst_prim) apply (erule e_prim_elim) apply simp
    apply (rule_tac x=n1 in exI) apply (rule conjI)
     apply force
    apply (rule_tac x=n2 in exI)
    apply auto
    done
next
  case (6 e1 e2 e3 \<rho>)
  then show ?case
    apply (simp only: subst_if) apply (erule e_if_elim) apply (rename_tac n)
    apply simp
    apply (case_tac "n = 0") apply (rule_tac x=0 in exI)
     apply force
    apply (rule_tac x=n in exI) apply simp done
next
  case (7 e1 e2 \<rho>)
  then show ?case
    apply (simp only: subst_cons) apply (erule e_cons_elim)
    apply simp apply (metis e_sub le_any_pair_inv) done
next
  case (8 e \<rho>)
  then show ?case
    apply (simp only: subst_car) apply fastforce done
next
  case (9 e \<rho>)
  then show ?case
    apply (simp only: subst_cdr) apply fastforce done
qed

subsection "Reduction preserves denotation"

lemma subject_reduction: fixes e::exp assumes v: "v \<in> E e \<rho>" and r: "e \<longrightarrow> e'" shows "v \<in> E e' \<rho>"
  using r v
proof (induction arbitrary: v \<rho> rule: reduce.induct)
   case (beta v x e v' \<rho>)
   then show ?case apply (simp only: is_val_def)
     apply (erule e_app_elim) apply (erule e_lam_elim) apply clarify
     apply (rename_tac f v2 v2' v3' f')
     apply (erule_tac x=v2' in allE) apply (erule_tac x=v3' in allE) apply clarify
     apply (subgoal_tac "v3' \<in> E (subst x v e) \<rho>") prefer 2 apply (rule substitution)
         apply (subgoal_tac "v3' \<in> E e ((x,v2)#\<rho>)") prefer 2 apply (rule raise_env)
           apply assumption apply (simp add: env_le_def) prefer 2 apply (rule env_strengthen)
          apply assumption apply force prefer 2 apply (subgoal_tac "(x,v2)#\<rho> \<approx> (x,v2)#\<rho>") prefer 2
         apply (simp add: env_eq_def) apply assumption apply assumption
      apply simp
     apply simp
     apply (rule e_sub)
      apply assumption
     apply (rule val_le_trans)
      apply blast
     apply force
     done
 next
   case (car e e' v \<rho>)
   then show ?case by auto
 next
   case (cdr e e' v \<rho>)
   then show ?case by auto
 next
   case (car_v v1 v2 v \<rho>)
   then show ?case by (metis e_car_elim e_cons_elim e_sub vpair_le_inv)
 next
   case (cdr_v v1 v2 v \<rho>)
   then show ?case by (metis e_cdr_elim e_cons_elim e_sub vpair_le_inv)
qed force+

theorem preservation: assumes v: "v \<in> E e \<rho>" and rr: "e \<longrightarrow>* e'" shows "v \<in> E e' \<rho>"
  using rr v subject_reduction by (induction arbitrary: \<rho> v) auto

lemma canonical_nat: assumes v: "VNat n \<in> E v \<rho>" and vv: "isval v" shows "v = ENat n"
  using v vv by (cases v) auto

lemma canonical_fun: assumes v: "VFun f \<in> E v \<rho>" and vv: "isval v" shows "\<exists> x e. v = ELam x e"
  using v vv by (cases v) auto

lemma canonical_pair: assumes v: "VPair v1 v2 \<in> E v \<rho>" and vv: "isval v" shows
"\<exists> v1' v2'. v = ECons v1' v2'" using v vv by (cases v) auto

subsection "Progress"

theorem progress: assumes v: "v \<in> E e \<rho>" and r: "\<rho> = []" and fve: "FV e = {}"
  shows "is_val e \<or> (\<exists> e'. e \<longrightarrow> e')"
  using v r fve
proof (induction arbitrary: v rule: E.induct)
  case (4 e1 e2 \<rho>)
  show ?case
    apply (rule e_app_elim) using 4(3) apply assumption
    apply (cases "is_val e1")
     apply (cases "is_val e2")
      apply (frule canonical_fun) apply force apply (erule exE)+ apply simp apply (rule disjI2)
      apply (rename_tac x e)
      apply (rule_tac x="subst x e2 e" in exI)
      apply (rule beta) apply simp
    using 4 apply simp
     apply blast
    using 4 apply simp
    apply blast done
next
  case (5 f e1 e2 \<rho>)
   show ?case
     apply (rule e_prim_elim) using 5(3) apply assumption
     using 5 apply (case_tac "isval e1")
      apply (case_tac "isval e2")
       apply (subgoal_tac "e1 = ENat n1") prefer 2 using canonical_nat apply blast
       apply (subgoal_tac "e2 = ENat n2") prefer 2 using canonical_nat apply blast
       apply force
      apply force
     apply force done
next
  case (6 e1 e2 e3 \<rho>)
  show ?case
    apply (rule e_if_elim)
    using 6(4) apply assumption
    apply (cases "isval e1")
     apply (rename_tac n)
     apply (subgoal_tac "e1 = ENat n") prefer 2 apply (rule canonical_nat) apply blast apply blast
     apply (rule disjI2) apply (case_tac "n = 0") apply force apply force
    apply (rule disjI2)
    using 6 apply (subgoal_tac "\<exists> e1'. e1 \<longrightarrow> e1'") prefer 2 apply force
    apply clarify apply (rename_tac e1')
    apply (rule_tac x="EIf e1' e2 e3" in exI)
    apply (rule if_cond) apply assumption
    done
next
  case (7 e1 e2 \<rho>)
  show ?case
    apply (rule e_cons_elim)
     apply(cases "is_val e1")
      apply(cases "is_val e2") apply (simp add: valpair) apply force apply force
     apply blast
    using 7 apply simp
    apply (meson cons_left cons_right valpair) done
next
  case (8 e \<rho>)
  show ?case
    apply (rule e_car_elim) using 8(2) apply assumption
    apply (cases "is_val e") apply (frule canonical_pair) apply force apply (erule exE)+
     apply simp apply (rule disjI2) apply (meson car_v is_val_def isval_cons_inv)
    apply (metis "8.IH" "8.prems"(2) "8.prems"(3) FV.simps(8) car) done
next
  case (9 e \<rho>)
  show ?case
    apply (rule e_cdr_elim) using 9(2) apply assumption
    apply (cases "is_val e") apply (frule canonical_pair) apply force apply (erule exE)+
     apply simp apply (rule disjI2) apply (meson cdr_v is_val_def isval_cons_inv)
    apply (metis "9.IH" "9.prems"(2) "9.prems"(3) FV.simps(9) cdr) done
qed auto

subsection "Logical relation between values and big-step values"

fun good_entry :: "name \<Rightarrow> exp \<Rightarrow> benv \<Rightarrow> (val \<times> bval set) \<times> (val \<times> bval set) \<Rightarrow> bool \<Rightarrow> bool" where
  "good_entry x e \<rho> ((v1,g1),(v2,g2)) r = ((\<forall> v \<in> g1. \<exists> v'. (x,v)#\<rho> \<turnstile> e \<Down> v' \<and> v' \<in> g2) \<and> r)"

primrec good :: "val \<Rightarrow> bval set" where
  Gnat: "good (VNat n) = { BNat n }" |
  Gfun: "good (VFun f) = { vc. \<exists> x e \<rho>. vc = BClos x e \<rho>
          \<and> (ffold (good_entry x e \<rho>) True (fimage (map_prod (\<lambda>v. (v,good v)) (\<lambda>v. (v,good v))) f)) }" |
  Gpair: "good (VPair v1 v2) = { vp. \<exists> bv1 bv2. vp = BPair bv1 bv2
          \<and> bv1 \<in> (good v1) \<and> bv2 \<in> (good v2)}"

inductive good_env :: "benv \<Rightarrow> env \<Rightarrow> bool" where
  genv_nil[intro!]: "good_env [] []" |
  genv_cons[intro!]: "\<lbrakk> v \<in> good v'; good_env \<rho> \<rho>' \<rbrakk> \<Longrightarrow> good_env ((x,v)#\<rho>) ((x,v')#\<rho>')"

inductive_cases
  genv_any_nil_inv: "good_env \<rho> []" and
  genv_any_cons_inv: "good_env \<rho> (b#\<rho>')"

lemma lookup_good:
  assumes l: "lookup \<rho>' x = Some A" and EE: "good_env \<rho> \<rho>'"
  shows "\<exists> v. lookup \<rho> x = Some v \<and> v \<in> good A"
  using l EE
proof (induction \<rho>' arbitrary: x A \<rho>)
  case Nil
  show ?case apply (rule genv_any_nil_inv) using Nil by auto
next
  case (Cons a \<rho>')
  show ?case
    apply (rule genv_any_cons_inv)
     using Cons apply force
    apply (rename_tac x') apply clarify
    using Cons apply (case_tac "x = x'")
     apply force
    apply force
    done
qed

abbreviation good_prod :: "val \<times> val \<Rightarrow> (val \<times> bval set) \<times> (val \<times> bval set)" where
  "good_prod \<equiv> map_prod (\<lambda>v. (v,good v)) (\<lambda>v. (v,good v))"

lemma good_fun_def2:
  "good_fun f x e \<rho> = ffold (good_entry x e \<rho> \<circ> good_prod) True f"
proof -
  interpret ge: comp_fun_commute "(good_entry x e \<rho>) \<circ> good_prod"
    unfolding comp_fun_commute_def by auto
  show "good_fun f x e \<rho>
         = ffold ((good_entry x e \<rho>) \<circ> good_prod) True f"
     using good_prod_inj[of "f"] good_fun_def
        ffold_fimage[of good_prod "f" "good_entry x e \<rho>" True] by auto
qed

lemma gfun_elim: "w \<in> good (VFun f) \<Longrightarrow> \<exists> x e \<rho>. w = BClos x e \<rho> \<and> good_fun f x e \<rho>"
  using good_fun_def by auto

lemma gfun_mem_iff: "good_fun f x e \<rho> = (\<forall> v1 v2. (v1,v2) \<in> fset f \<longrightarrow>
    (\<forall> v \<in> good v1. \<exists> v'. (x,v)#\<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))"
proof (induction f arbitrary: x e \<rho>)
  case empty
  interpret ge: comp_fun_commute "(good_entry x e \<rho>)"
    unfolding comp_fun_commute_def by auto
  from empty show ?case using good_fun_def2 by simp
next
  case (insert p f)
  interpret ge: comp_fun_commute "(good_entry x e \<rho>) \<circ> good_prod"
    unfolding comp_fun_commute_def by auto
  have "good_fun (finsert p f) x e \<rho>
         = ffold ((good_entry x e \<rho>) \<circ> good_prod) True (finsert p f)" by (simp add: good_fun_def2)
  also from insert(1) have "... = ((good_entry x e \<rho>) \<circ> good_prod) p
                  (ffold ((good_entry x e \<rho>) \<circ> good_prod) True f)" by simp
  finally have 1: "good_fun (finsert p f) x e \<rho>
      = ((good_entry x e \<rho>) \<circ> good_prod) p (ffold ((good_entry x e \<rho>) \<circ> good_prod) True f)" .
  show ?case
  proof
    assume 2: "good_fun (finsert p f) x e \<rho>"
    show "\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow>
       (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)"
    proof clarify
      fix v1 v2 v assume 3: "(v1, v2) \<in> fset (finsert p f)" and 4: "v \<in> good v1"
      from 3 have "(v1,v2) = p \<or> (v1,v2) \<in> fset f" by auto
      from this show "\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2"
      proof
        assume v12_p: "(v1,v2) = p"
        from 1 v12_p[THEN sym] 2 4 show ?thesis by simp
      next
        assume v12_f: "(v1,v2) \<in> fset f"
        from 1 2 have 5: "good_fun f x e \<rho>" apply simp
          apply (cases "(good_prod p)") by (auto simp: good_fun_def2)
        from v12_f 5 4 insert(2)[of x e \<rho>] show ?thesis by auto
      qed
    qed
  next
    assume 2: "\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow>
       (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)"
    have 3: "good_entry x e \<rho> (good_prod p) True"
      apply (cases p) apply simp apply clarify
    proof -
      fix v1 v2 v
      assume p: "p = (v1,v2)" and v_v1: "v \<in> good v1"
      from p have "(v1,v2) \<in> fset (finsert p f)" by simp
      from this 2 v_v1 show "\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2" by blast
    qed
    from insert(2) 2 have 4: "good_fun f x e \<rho>" by auto
    have "(good_entry x e \<rho> \<circ> good_prod) p
     (ffold (good_entry x e \<rho> \<circ> good_prod) True f)"
      apply simp apply (cases "good_prod p")
      apply (rename_tac a b c)
      apply (case_tac a) apply simp
      apply (rule conjI) prefer 2 using 4 good_fun_def2 apply force
      using 3 apply force done
    from this 1 show "good_fun (finsert p f) x e \<rho>"
       unfolding good_fun_def by simp
  qed
qed

lemma gfun_mem: "\<lbrakk> (v1,v2) \<in> fset f; good_fun f x e \<rho> \<rbrakk>
      \<Longrightarrow> \<forall> v \<in> good v1. \<exists> v'. (x,v)#\<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2"
  using gfun_mem_iff by blast

lemma gfun_intro: "(\<forall> v1 v2.(v1,v2)\<in>fset f\<longrightarrow>(\<forall>v\<in>good v1.\<exists> v'.(x,v)#\<rho> \<turnstile> e \<Down> v'\<and>v'\<in>good v2))
  \<Longrightarrow> good_fun f x e \<rho>" using gfun_mem_iff[of f x e \<rho>] by simp

lemma good_pair: "w \<in> good (VPair v1 v2) \<Longrightarrow> \<exists> b1 b2. w = BPair b1 b2 \<and> b1 \<in> good v1 \<and> b2 \<in> good v2"
  by simp

lemma sub_good: fixes v::val assumes wv: "w \<in> good v" and vp_v: "v' \<sqsubseteq> v" shows "w \<in> good v'"
  using wv vp_v
proof (induction v arbitrary: v' w)
  case (VNat n)
  then show ?case by blast
next
  case (VFun t1)
  from vp_v VFun obtain t2 where b: "v' = VFun t2" and t2_t1: "fset t2 \<subseteq> fset t1" by auto
  from wv VFun obtain x e \<rho> where w: "w = BClos x e \<rho>" by auto
  from w wv VFun have gt1: "good_fun t1 x e \<rho>" by (simp add: good_fun_def)
  have gt2: "good_fun t2 x e \<rho>" apply (rule gfun_intro) apply clarify
  proof -
    fix v1 v2 w1
    assume v12: "(v1,v2) \<in> fset t2" and w1_v1: "w1 \<in> good v1"
    from v12 t2_t1 have v12_t1: "(v1,v2) \<in> fset t1" by blast
    from gt1 v12_t1 w1_v1 show "\<exists>v'. (x, w1) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2"
      by (simp add: gfun_mem)
  qed
  from gt2 b w show ?case by (simp add: good_fun_def)
next
  case (VPair v1 v2)
  from VPair obtain v1' v2' where vp: "v' = VPair v1' v2'" and
    v1_v1: "v1' \<sqsubseteq> v1" and v2_v2: "v2' \<sqsubseteq> v2" by blast

  from VPair(3) good_pair obtain b1 b2 where w: "w = BPair b1 b2" by blast

  from VPair Gpair w have bv1_v1: "b1 \<in> good v1" and bv2_v2: "b2 \<in> good v2"
     apply blast using VPair.prems(1) w by auto

  from w bv1_v1 v1_v1 VPair(1) have 1: "b1 \<in> good v1'" by blast
  from w bv2_v2 v2_v2 VPair(2) have 2: "b2 \<in> good v2'" by blast

  from 1 2 show ?case by (simp add: vp w)
qed

subsection "Denotational semantics sound wrt. big-step"

lemma denot_terminates: assumes vp_e: "v' \<in> E e \<rho>'" and ge: "good_env \<rho> \<rho>'"
  shows "\<exists> v. \<rho> \<turnstile> e \<Down> v \<and> v \<in> good v'"
  using vp_e ge
proof (induction arbitrary: v' \<rho> rule: E.induct)
  case (1 n \<rho>) -- "ENat"
  then show ?case by auto
next -- "EVar"
  case (2 x \<rho> v' \<rho>')
  from 2 obtain v1 where lx_vpp: "lookup \<rho> x = Some v1" and vp_v1: "v' \<sqsubseteq> v1" by auto
  from lx_vpp 2(2) obtain v2 where lx: "lookup \<rho>' x = Some v2" and v2_v1: "v2 \<in> good v1"
    using lookup_good[of \<rho> x v1 \<rho>'] by blast
  from lx have x_v2: "\<rho>' \<turnstile> EVar x \<Down> v2" by auto
  from v2_v1 vp_v1 have v2_vp: "v2 \<in> good v'" using sub_good by blast
  from x_v2 v2_vp show ?case by blast
next -- "ELam"
  case (3 x e \<rho> v' \<rho>')
  have 1: "\<rho>' \<turnstile> ELam x e \<Down> BClos x e \<rho>'" by auto
  have 2: "BClos x e \<rho>' \<in> good v'"
  proof -
    from 3(2) obtain t where vp: "v' = VFun t" and
      body: "\<forall>v1 v2. (v1, v2) \<in> fset t \<longrightarrow> v2 \<in> E e ((x, v1) # \<rho>)" by blast
    have gt: "good_fun t x e \<rho>'" apply (rule gfun_intro) apply clarify
    proof -
      fix v1 v2 w1 assume v12_t: "(v1,v2) \<in> fset t" and w1_v1: "w1 \<in> good v1"
      from v12_t body have v2_Ee: "v2 \<in> E e ((x, v1) # \<rho>)" by blast
      from 3(3) w1_v1 have ge: "good_env ((x,w1)#\<rho>') ((x,v1)#\<rho>)" by auto
      from v12_t v2_Ee ge 3(1)[of v1 v2 t v2]
      show "\<exists>v'. (x, w1) # \<rho>' \<turnstile> e \<Down> v' \<and> v' \<in> good v2" by blast
    qed
    from vp gt show ?thesis unfolding good_fun_def by simp
  qed
  from 1 2 show ?case by blast
next -- "EApp"
  case (4 e1 e2 \<rho> v' \<rho>')
  from 4(3) show ?case
  proof
    fix t v2 and v2'::val and v3' assume t_Ee1: "VFun t \<in> E e1 \<rho>" and v2_Ee2: "v2 \<in> E e2 \<rho>" and
      v23_t: "(v2',v3') \<in> fset t" and v2p_v2: "v2' \<sqsubseteq> v2" and vp_v3p: "v' \<sqsubseteq> v3'"
    from 4(1) t_Ee1 4(4) obtain w1 where e1_w1: "\<rho>' \<turnstile> e1 \<Down> w1" and
      w1_t: "w1 \<in> good (VFun t)" by blast
    from 4(2) v2_Ee2 4(4) obtain w2 where e2_w2: "\<rho>' \<turnstile> e2 \<Down> w2" and w2_v2: "w2 \<in> good v2" by blast
    from w1_t obtain x e \<rho>1 where w1: "w1 = BClos x e \<rho>1" and gt: "good_fun t x e \<rho>1"
      by (auto simp: good_fun_def)
    from w2_v2 v2p_v2 have w2_v2p: "w2 \<in> good v2'" by (rule sub_good)
    from v23_t gt w2_v2p obtain w3 where e_w3: "(x,w2)#\<rho>1 \<turnstile> e \<Down> w3" and w3_v3p: "w3 \<in> good v3'"
      using gfun_mem[of v2' v3' t x e \<rho>1] by blast
    from w3_v3p vp_v3p have w3_vp: "w3 \<in> good v'" by (rule sub_good)
    from e1_w1 e2_w2 w1 e_w3 w3_vp show "\<exists>v. \<rho>' \<turnstile> EApp e1 e2 \<Down> v \<and> v \<in> good v'" by blast
  qed
next -- "EPrim"
  case (5 f e1 e2 \<rho> v' \<rho>')
  from 5(3) show ?case
  proof
    fix n1 n2 assume n1_e1: "VNat n1 \<in> E e1 \<rho>" and n2_e2: "VNat n2 \<in> E e2 \<rho>" and
      vp: "v' = VNat (f n1 n2)"
    from 5(1)[of "VNat n1" \<rho>'] n1_e1 5(4) have e1_w1: "\<rho>' \<turnstile> e1 \<Down> BNat n1" by auto
    from 5(2)[of "VNat n2" \<rho>'] n2_e2 5(4) have e2_w2: "\<rho>' \<turnstile> e2 \<Down> BNat n2" by auto
    from e1_w1 e2_w2 have 1: "\<rho>' \<turnstile> EPrim f e1 e2 \<Down> BNat (f n1 n2)" by blast
    from vp have 2: "BNat (f n1 n2) \<in> good v'" by auto
    from 1 2 show "\<exists>v. \<rho>' \<turnstile> EPrim f e1 e2 \<Down> v \<and> v \<in> good v'" by auto
  qed
next -- "EIf"
  case (6 e1 e2 e3 \<rho> v' \<rho>')
  from 6(4) show ?case
  proof
    fix n assume n_e1: "VNat n \<in> E e1 \<rho>" and els: "n = 0 \<longrightarrow> v' \<in> E e3 \<rho>" and
      thn: "n \<noteq> 0 \<longrightarrow> v' \<in> E e2 \<rho>"
    from 6(1)[of "VNat n" \<rho>'] n_e1 6(5) have e1_w1: "\<rho>' \<turnstile> e1 \<Down> BNat n" by auto
    show "\<exists>v. \<rho>' \<turnstile> EIf e1 e2 e3 \<Down> v \<and> v \<in> good v'"
    proof (cases "n = 0")
      case True
      from 6(2)[of n v' \<rho>'] True els 6(5) obtain w3 where
        e3_w3: "\<rho>' \<turnstile> e3 \<Down> w3" and w3_vp: "w3 \<in> good v'" by blast
      from e1_w1 True e3_w3 w3_vp show ?thesis by blast
    next
      case False
      from 6(3)[of n v' \<rho>'] False thn 6(5) obtain w2 where
        e2_w2: "\<rho>' \<turnstile> e2 \<Down> w2" and w2_vp: "w2 \<in> good v'" by blast
      from e1_w1 False e2_w2 have "\<rho>' \<turnstile> EIf e1 e2 e3 \<Down> w2"
        using eval_if1[of \<rho>' e1 n e2 w2 e3] by simp
      from this w2_vp show ?thesis by (rule_tac x=w2 in exI) simp
    qed
  qed
next -- "ECons"
  case (7 e1 e2 \<rho> v' \<rho>')
  show ?case using "7.IH"(1) "7.IH"(2) "7.prems"(1) "7.prems"(2) by fastforce
next -- "ECar"
  case (8 e \<rho> v' \<rho>')
  then show ?case by  (smt e_car_elim eval_car good.simps(3) mem_Collect_eq sub_good)
next -- "ECdr"
  case (9 e \<rho> v' \<rho>')
  then show ?case by (smt e_cdr_elim eval_cdr good.simps(3) mem_Collect_eq sub_good)
qed

theorem sound_wrt_op_sem:
  assumes E_e_n: "E e [] = E (ENat n) []" and fv_e: "FV e = {}" shows "e \<Down> ONat n"
proof -
  have "VNat n \<in> E (ENat n) []" by simp
  with E_e_n have 1: "VNat n \<in> E e []" by simp
  have 2: "good_env [] []" by auto
  from 1 2 obtain v where e_v: "[] \<turnstile> e \<Down> v" and v_n: "v \<in> good (VNat n)" using denot_terminates by blast
  from v_n have v: "v = BNat n" by auto
  from e_v fv_e obtain v' ob where e_vp: "e \<longrightarrow>* v'" and
    vp_ob: "observe v' ob" and v_ob: "bs_observe v ob" using sound_wrt_small_step by blast
  from e_vp vp_ob v_ob v show ?thesis unfolding run_def by (case_tac ob) auto
qed

end

author: cderici

repo: denotational-semantics-LC-with-pairs