Theory Interpreter

text‹
Interpreter.thy defines a simple programming language over interval-valued variables and executable
semantics (interpreter) for that language. We then prove that the interpretation of interval terms
is a sound over-approximation of a real-valued semantics of the same language.

Our language is a version of first order dynamic logic-style regular programs.
We use a finite identifier space for compatibility with Differential-Dynamic-Logic, where identifier
finiteness is required to treat program states as Banach spaces to enable differentiation.
›
(* Author:     Rose Bohrer *)
theory Interpreter
imports
  Complex_Main
  Finite_String
  Interval_Word32
begin

section‹Syntax›
text‹Our term language supports variables, polynomial arithmetic, and extrema. This choice was made
   based on the needs of the original paper and could be extended if necessary.›
datatype  trm =
  Var fin_string
| Const lit
| Plus trm trm
| Times trm trm
| Neg trm
| Max trm trm
| Min trm trm
| Abs trm

text‹Our statement language is nondeterministic first-order regular programs.
 This coincides with the discrete subset of hybrid programs from the dL entry.

Our assertion language are the formulas of first-order dynamic logic›
datatype prog =
  Assign fin_string "trm"     (infixr ‹:=› 10)
| AssignAny fin_string                
| Test "formula"              (‹?›)
| Choice "prog" "prog"        (infixl ‹∪∪› 10)
| Sequence "prog"  "prog"     (infixr ‹;;› 8)
| Loop "prog"                 (‹_**›)

and formula =
  Geq "trm" "trm"
| Not "formula"                        (‹!›)
| And "formula" "formula"              (infixl ‹&&› 8)
| Exists fin_string "formula"
| Diamond "prog" "formula"               (‹(⟨ _ ⟩ _)› 10)
    
text‹Derived forms›
definition Or :: "formula ⇒ formula ⇒ formula" (infixl ‹||› 7)
where or_simp[simp]:"Or P Q = Not (And (Not P) (Not Q))"

definition Equals :: "trm ⇒ trm ⇒ formula"
where equals_simp[simp]:"Equals θ θ' = (And (Geq θ θ') (Geq θ' θ))"

definition Greater :: "trm ⇒ trm ⇒ formula"
where greater_simp[simp]:"Greater θ θ' = Not (Geq θ' θ)"

definition Leq :: "trm ⇒ trm ⇒ formula"
where leq_simp[simp]:"Leq θ θ' = (Geq θ' θ)"

definition Less :: "trm ⇒ trm ⇒ formula"
where less_simp[simp]:"Less θ θ' = (Not (Geq θ θ'))"

section ‹Semantics›
text‹ States over reals vs. word intervals which contain them›
type_synonym rstate = "fin_string ⇒ real"
type_synonym wstate = "(fin_string + fin_string) ⇒ word"

definition wstate::"wstate ⇒ prop"
where wstate_def[simp]:"wstate ν ≡ (⋀i. word (ν (Inl i)) ∧ word (ν (Inr i)))"

text‹Interpretation of a term in a state›
inductive rtsem :: "trm ⇒ rstate ⇒ real  ⇒ bool"  (‹([_]_ ↓ _)› 10)
  where 
  rtsem_Const:"Rep_bword w ≡⇩E r ⟹ ([Const w]ν ↓ r)"
| rtsem_Var:"([Var x]ν ↓ ν x)"
| rtsem_Plus:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ ([Plus θ⇩1 θ⇩2]ν ↓ (r1 + r2))"
| rtsem_Times:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ ([Times θ⇩1 θ⇩2]ν ↓ (r1 * r2))"
| rtsem_Max:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ ([Max θ⇩1 θ⇩2]ν ↓ (max r1 r2))"
| rtsem_Min:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ ([Min θ⇩1 θ⇩2]ν ↓ (min r1 r2))"
| rtsem_Abs:"⟦([θ⇩1]ν ↓ r1)⟧ ⟹ ([Abs θ⇩1]ν ↓ (abs r1))"
| rtsem_Neg:"([θ]ν ↓ r) ⟹ ([Neg θ]ν ↓ -r)"

inductive_simps 
    rtsem_Const_simps[simp] : "([(Const w)]ν ↓ r)"
and rtsem_Var_simps[simp] : "([Var x]ν ↓ r)"
and rtsem_PlusU_simps[simp] : "([Plus θ⇩1 θ⇩2]ν ↓ r)"
and rtsem_TimesU_simps[simp] : "([Times θ⇩1 θ⇩2]ν ↓ r)"
and rtsem_Max_simps[simp] : "([Max θ⇩1 θ⇩2] ν ↓ r)"
and rtsem_Min_simps[simp] : "([Min θ⇩1 θ⇩2] ν ↓ r)"
and rtsem_Abs_simps[simp] : "([Abs θ] ν ↓ r)"
and rtsem_Neg_simps[simp] : "([Neg θ] ν ↓ r)"

definition set_less :: "real set ⇒ real set ⇒ bool" (infix ‹<⇩S› 10)
where "set_less A B ≡ (∀ x y. x ∈ A ∧ y ∈ B ⟶ x < y)"

definition set_geq :: "real set ⇒ real set ⇒ bool" (infix ‹≥⇩S› 10)
where "set_geq A B ≡ (∀ x y. x ∈ A ∧ y ∈ B ⟶ x ≥ y)"

text‹Interpretation of an assertion in a state›
inductive rfsem :: "formula ⇒ rstate ⇒ bool ⇒ bool" (‹([_]_) ⇂ _› 20)
where 
  rGreaterT:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r1 > r2 ⟹ ([Greater θ⇩1 θ⇩2] ν ⇂ True)"
| rGreaterF:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r2 ≥ r1 ⟹ ([Greater θ⇩1 θ⇩2] ν ⇂ False)"
| rGeqT:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r1 ≥ r2 ⟹ ([Geq θ⇩1 θ⇩2] ν ⇂ True)"
| rGeqF:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r2 > r1 ⟹ ([Geq θ⇩1 θ⇩2] ν ⇂ False)"
| rEqualsT:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r1 = r2 ⟹ ([Equals θ⇩1 θ⇩2] ν ⇂ True)"
| rEqualsF:"⟦([θ⇩1]ν ↓ r1); ([θ⇩2]ν ↓ r2)⟧ ⟹ r1 ≠ r2 ⟹ ([Equals θ⇩1 θ⇩2] ν ⇂ False)"
| rAndT:"⟦([φ]ν ⇂ True); ([ψ]ν ⇂ True)⟧ ⟹ ([And φ ψ]ν ⇂ True)"
| rAndF1:"([φ]ν ⇂ False) ⟹ ([And φ ψ]ν ⇂ False)"
| rAndF2:"([ψ]ν ⇂ False) ⟹ ([And φ ψ]ν ⇂ False)"
| rOrT1:"([φ]ν ⇂ True) ⟹ ([Or φ ψ]ν ⇂ True)"
| rOrT2:"([ψ]ν ⇂ True) ⟹ ([Or φ ψ]ν ⇂ True)"
| rOrF:"⟦([φ]ν ⇂ False) ;([ψ]ν ⇂ False)⟧ ⟹ ([And φ ψ]ν ⇂ False)"
| rNotT:"([φ]ν ⇂ False) ⟹ ([(Not φ)]ν ⇂ True)"
| rNotF:"([φ]ν ⇂ True) ⟹ ([(Not φ)]ν ⇂ False)"

inductive_simps
    rfsem_Greater_simps[simp]: "([Greater θ⇩1 θ⇩2]ν ⇂ b)"
and rfsem_Geq_simps[simp]: "([Geq θ⇩1 θ⇩2]ν ⇂ b)"
and rfsem_Equals_simps[simp]: "([Equals θ⇩1 θ⇩2]ν ⇂ b)"
and rfsem_And_simps[simp]: "([And φ  ψ]ν ⇂ b)"
and rfsem_Or_simps[simp]: "([(Or φ ψ)]ν ⇂ b)"
and rfsem_Not_simps[simp]: "([Not φ]ν ⇂ b)"

text‹Interpretation of a program is a transition relation on states›
inductive rpsem :: "prog ⇒ rstate ⇒  rstate ⇒ bool" (‹([_]_) ⇃ _› 20)
where
  rTest[simp]:"⟦([φ]ν ⇂ True); ν = ω⟧ ⟹ ([? φ]ν ⇃ ω)"
| rSeq[simp]:"⟦([α]ν ⇃ μ); ([β]μ ⇃ ω)⟧ ⟹ ([α;; β]ν ⇃ ω)"
| rAssign[simp]:"⟦([θ]ν ↓ r); ω = (ν (x := r))⟧ ⟹ ([Assign x θ]ν ⇃ ω)"
| rChoice1[simp]:"([α]ν ⇃ ω) ⟹ ([Choice α β]ν ⇃ ω)"
| rChoice2[simp]:"([β]ν ⇃ ω) ⟹ ([Choice α β]ν ⇃ ω)"

inductive_simps
    rpsem_Test_simps[simp]: "([? φ]ν ⇃ b)"
and rpsem_Seq_simps[simp]: "([α;; β]ν ⇃ b)"
and rpsem_Assign_simps[simp]: "([Assign x θ]ν ⇃ b)"
and rpsem_Choice_simps[simp]: "([Choice α β]ν ⇃ b)"

text‹Upper bound of arbitrary term›
fun wtsemU :: "trm ⇒ wstate ⇒  word * word " (‹([_]<>_)› 20)
where "([Const r]<>ν) = (Rep_bword r::word, Rep_bword r)"
| wVarU:"([Var x]<>ν) = (ν (Inl x), ν (Inr x))"
| wPlusU:"([Plus θ⇩1 θ⇩2]<> ν) = 
  (let (l1, u1) = [θ⇩1]<> ν in 
   let (l2, u2) = [θ⇩2]<> ν in
   (pl l1 l2, pu u1 u2))"
| wTimesU:"([(Times θ⇩1 θ⇩2)]<> ν) = 
  (let (l1, u1) = [θ⇩1]<> ν in 
   let (l2, u2) = [θ⇩2]<> ν in
   (tl l1 u1 l2 u2, tu l1 u1 l2 u2))"
| wMaxU:"([(Max θ⇩1 θ⇩2)]<> ν) = 
  (let (l1, u1) = [θ⇩1]<> ν in 
   let (l2, u2) = [θ⇩2]<> ν in
  (wmax l1 l2, wmax u1 u2))"
| wMinU:"([(Min θ⇩1 θ⇩2)]<> ν) = 
  (let (l1, u1) = [θ⇩1]<> ν in 
   let (l2, u2) = [θ⇩2]<> ν in
  (wmin l1 l2, wmin u1 u2))"
| wNegU:"([(Neg θ)]<> ν) =
  (let (l, u) = [θ]<> ν in
   (wneg u, wneg l))"
| wAbsU:"([(Abs θ⇩1)]<> ν) = 
  (let (l1, u1) = [θ⇩1]<> ν in 
  (wmax l1 (wneg u1), wmax u1 (wneg l1)))"

inductive wfsem :: "formula ⇒ wstate ⇒ bool ⇒ bool" (‹([[_]]_ ↓ _)› 20)
where 
  wGreaterT:"wgreater (fst ([θ⇩1]<>ν)) (snd ([θ⇩2]<>ν)) ⟹  ([[(Greater θ⇩1 θ⇩2)]]ν ↓ True)"
| wGreaterF:"wgeq (fst ([θ⇩2]<>ν)) (snd ([θ⇩1]<>ν)) ⟹  ([[(Greater θ⇩1 θ⇩2)]]ν ↓ False)"
| wGeqT:"wgeq (fst ([θ⇩1]<> ν)) (snd ([θ⇩2]<>ν)) ⟹  ([[(Geq θ⇩1 θ⇩2)]]ν ↓ True)"
| wGeqF:"wgreater (fst ([θ⇩2]<>ν)) (snd ([θ⇩1]<>ν)) ⟹  ([[(Geq θ⇩1 θ⇩2)]]ν ↓ False)"
| wEqualsT:"⟦(fst ([θ⇩2]<>ν) = snd ([θ⇩2]<>ν)); (snd ([θ⇩2]<>ν) = snd ([θ⇩1]<>ν)); 
             (snd ([θ⇩1]<>ν) = fst ([θ⇩1]<>ν)); (fst ([θ⇩2]<>ν) ≠ NEG_INF); 
             (fst ([θ⇩2]<>ν) ≠ POS_INF)⟧ 
         ⟹ ([[Equals θ⇩1 θ⇩2]] ν ↓ True)"
| wEqualsF1:"wgreater (fst ([θ⇩1]<> ν)) (snd ([θ⇩2]<>ν)) ⟹  ([[Equals θ⇩1 θ⇩2]] ν ↓ False)"
| wEqualsF2:"wgreater (fst ([θ⇩2]<> ν)) (snd ([θ⇩1]<>ν)) ⟹  ([[Equals θ⇩1 θ⇩2]] ν ↓ False)"
| wAndT:"⟦[[φ]]ν ↓ True; [[ψ]]ν ↓ True⟧ ⟹ ([[And φ ψ]]ν ↓ True)"
| wAndF1:"[[φ]]ν ↓ False ⟹ ([[And φ ψ]]ν ↓ False)"
| wAndF2:"[[ψ]]ν ↓ False ⟹ ([[And φ ψ]]ν ↓ False)"
| wOrT1:"([[φ]]ν ↓ True) ⟹ ([[Or φ ψ]]ν ↓ True)"
| wOrT2:"([[ψ]]ν ↓ True) ⟹ ([[Or φ ψ]]ν ↓ True)"
| wOrF:"⟦[[φ]]ν ↓ False; [[ψ]]ν ↓ False⟧ ⟹ ([[And φ ψ]]ν ↓ False)"
| wNotT:"([[φ]]ν ↓ False) ⟹ ([[Not φ]]ν ↓ True)"
| wNotF:"([[φ]]ν ↓ True) ⟹ ([[Not φ]]ν ↓ False)"

inductive_simps
    wfsem_Gr_simps[simp]: "([[Le θ⇩1 θ⇩2]]ν ↓ b)"
and wfsem_And_simps[simp]: "([[And φ ψ]]ν ↓ b)"
and wfsem_Or_simps[simp]: "([[Or φ ψ]]ν ↓ b)"
and wfsem_Not_simps[simp]: "([[Not φ]]ν ↓ b)"
and wfsem_Equals_simps[simp]: "([[Equals θ⇩1 θ⇩2]]ν ↓ b)"

text‹Program semantics›
inductive wpsem :: "prog ⇒  wstate ⇒ wstate ⇒ bool" (‹([[_]]_ ↓ _)› 20)
where
  wTest:"([[φ]]ν ↓ True) ⟹ ν = ω ⟹ ([[? φ]] ν ↓ ω)"
| wSeq:"([[α]]ν ↓ μ) ⟹ ([[β]] μ ↓ ω) ⟹ ([[α;; β]] ν ↓ ω)"
| wAssign:"ω = ((ν ((Inr x) := snd([θ]<>ν))) ((Inl x) := fst([θ]<>ν))) ⟹ ([[Assign x θ]] ν ↓ ω)"
| wChoice1[simp]:"([[α]]ν ↓ ω) ⟹ ([[Choice α β]]ν ↓ ω)"
| wChoice2[simp]:"([[β]]ν ↓ ω) ⟹ ([[Choice α β]]ν ↓ ω)"

inductive_simps
    wpsem_Test_simps[simp]: "([[Test φ]]ν ↓ b)"
and wpsem_Seq_simps[simp]: "([[α;; β]]ν ↓ b)"
and wpsem_Assign_simps[simp]: "([[Assign x θ]]ν ↓ b)"
and wpsem_Choice_simps[simp]: "([[Choice α β]]ν ↓ b)"

lemmas real_max_mono =  Lattices.linorder_class.max.mono  
lemmas real_minus_le_minus = Groups.ordered_ab_group_add_class.neg_le_iff_le

text‹Interval state consists of upper and lower bounds for each real variable›
inductive represents_state::"wstate ⇒ rstate ⇒ bool" (infix ‹REP› 10)
where REPI:"(⋀x. (ν (Inl x) ≡⇩L ν' x) ∧ (ν (Inr x) ≡⇩U ν' x)) ⟹ (ν REP ν')"

inductive_simps repstate_simps:"ν REP ν'"

section‹Soundness proofs›
text‹Interval term valuation soundly contains real valuation›
lemma trm_sound:
  fixes θ::"trm"
  shows "([θ]ν' ↓ r) ⟹ (ν REP ν') ⟹   ([θ]<>ν) ≡⇩P r"
proof (induction rule: rtsem.induct)
 case rtsem_Const 
   fix w r ν'
   show "Rep_bword w ≡⇩E r ⟹ ν REP ν' ⟹ [Const w]<>ν ≡⇩P r"
     using repU_def repL_def repP_def repe.simps rep_simps repstate_simps 
     by auto
next
 case rtsem_Var
   fix x ν'
   show "ν REP ν' ⟹ [Var x]<>ν ≡⇩P ν' x"
   by(auto simp add: repU_def repL_def repP_def repe.simps rep_simps repstate_simps)
next
 case rtsem_Plus
   fix θ⇩1 :: "trm" and ν':: "rstate" and r1 and θ⇩2 :: "trm" and  r2
   assume rep:"ν REP ν'"
   assume eval1:"[θ⇩1]ν' ↓ r1"
   assume "(ν REP ν' ⟹ [θ⇩1]<>ν ≡⇩P r1)"
   then have IH1:"[θ⇩1]<>ν ≡⇩P r1" using rep by auto
   assume eval2:"[θ⇩2]ν' ↓ r2"
   assume "(ν REP ν' ⟹ [θ⇩2]<>ν ≡⇩P r2)"
   then have IH2:"[θ⇩2]<>ν ≡⇩P r2" using rep by auto
   obtain l1 u1 l2 u2 where 
        lu1:"(l1, u1) = ([θ⇩1]<> ν)" 
    and lu2:"(l2, u2) = ([θ⇩2]<> ν)"
    using IH1 IH2 repP_def by auto
   from lu1 and lu2 have
        lu1':"([θ⇩1]<> ν) = (l1, u1)" 
    and lu2':"([θ⇩2]<> ν) = (l2, u2)"
    by auto
  have l1:"l1 ≡⇩L r1" using IH1 lu1 unfolding repP_def by auto
  have u1:"u1 ≡⇩U r1" using IH1 lu1 unfolding repP_def by auto
  have l2:"l2 ≡⇩L r2" using IH2 lu2 unfolding repP_def by auto
  have u2:"u2 ≡⇩U r2" using IH2 lu2 unfolding repP_def by auto
  then have "([(Plus θ⇩1 θ⇩2)]<>ν) = (pl l1 l2, pu u1 u2)"  
   using lu1' lu2' by auto
  have lBound:"(pl l1 l2 ≡⇩L r1 + r2)"
    using l1 l2 pl_lemma by auto
  have uBound:"(pu u1 u2 ≡⇩U r1 + r2)"
    using pu_lemma[OF u1 u2] by auto
  have "(pl l1 l2, pu u1 u2) ≡⇩P (r1 + r2)"
    unfolding repP_def Let_def using lBound uBound by auto
  then show"[Plus θ⇩1 θ⇩2]<>ν ≡⇩P r1 + r2"
    using lu1' lu2' by auto
next
 case rtsem_Times
   fix θ⇩1 :: "trm" and ν' r1 and θ⇩2 :: "trm" and r2
   assume eval1:"[θ⇩1]ν' ↓ r1"
   assume eval2:"[θ⇩2]ν' ↓ r2"
   assume rep:"ν REP ν'"
   assume "(ν REP ν' ⟹ ([θ⇩1]<>ν ≡⇩P r1))"
   then have IH1:"[θ⇩1]<>ν ≡⇩P r1" using rep by auto 
   assume "(ν REP ν' ⟹ ([θ⇩2]<>ν ≡⇩P r2))"
   then have IH2:"[θ⇩2]<>ν ≡⇩P r2" using rep by auto
    obtain l1 u1 l2 u2 where 
        lu1:"([θ⇩1]<> ν) = (l1, u1) " 
    and lu2:"([θ⇩2]<> ν) = (l2, u2)"
    using IH1 IH2 repP_def by auto
  have l1:"l1 ≡⇩L r1" using IH1 lu1 unfolding repP_def by auto
  have u1:"u1 ≡⇩U r1" using IH1 lu1 unfolding repP_def by auto
  have l2:"l2 ≡⇩L r2" using IH2 lu2 unfolding repP_def by auto
  have u2:"u2 ≡⇩U r2" using IH2 lu2 unfolding repP_def by auto
  then have "([(Times θ⇩1  θ⇩2)]<>ν) = (tl l1 u1 l2 u2, tu l1 u1 l2 u2)"  
   using lu1 lu2 unfolding wTimesU Let_def by auto 
  have lBound:"(tl l1 u1 l2 u2 ≡⇩L r1 * r2)"
    using l1 u1 l2 u2 tl_lemma by auto
  have uBound:"(tu l1 u1 l2 u2 ≡⇩U r1 * r2)"
    using l1 u1 l2 u2 tu_lemma by auto
  have "(tl l1 u1 l2 u2, tu l1 u1 l2 u2) ≡⇩P (r1 * r2)"
    unfolding repP_def Let_def using lBound uBound by auto
  then show "[Times θ⇩1 θ⇩2]<>ν ≡⇩P r1 * r2"
    using lu1 lu2 by auto
next
 case rtsem_Max
   fix θ⇩1 :: "trm" and ν' r1 and θ⇩2 :: "trm" and  r2
   assume eval1:"([θ⇩1]ν' ↓ r1)"
   assume eval2:"([θ⇩2]ν' ↓ r2)"
   assume rep:"ν REP ν'"
   assume "(ν REP ν' ⟹ [θ⇩1]<>ν ≡⇩P r1)"
   then have IH1:"[θ⇩1]<>ν ≡⇩P r1" using rep by auto
   assume "(ν REP ν' ⟹ [θ⇩2]<>ν ≡⇩P r2)"
   then have IH2:"[θ⇩2]<>ν ≡⇩P r2" using rep by auto
   obtain l1 u1 l2 u2 where 
        lu1:"([θ⇩1]<> ν) = (l1, u1)" 
    and lu2:"([θ⇩2]<> ν) = (l2, u2)"
    using IH1 IH2 repP_def by auto
   from IH1 IH2 
   obtain ub1 ub2 lb1 lb2:: real 
   where urep1:"(ub1 ≥ r1) ∧ (snd ([θ⇩1]<>ν) ≡⇩E ub1)" 
   and   urep2:"(ub2 ≥ r2) ∧ (snd ([θ⇩2]<>ν) ≡⇩E ub2)"
   and   lrep1:"(lb1 ≤ r1) ∧ (fst ([θ⇩1]<>ν) ≡⇩E lb1)" 
   and   lrep2:"(lb2 ≤ r2) ∧ (fst ([θ⇩2]<>ν) ≡⇩E lb2)"
     using repP_def repU_def repL_def by auto
   have lbound:"wmax l1 l2 ≡⇩L max r1 r2"
     by (metis dual_order.trans fst_conv le_cases lrep1 lrep2 lu1 lu2 max_def repL_def wmax.elims)
   have ubound:"wmax u1 u2 ≡⇩U max r1 r2"     
     by (metis real_max_mono lu1 lu2 repU_def snd_conv urep1 urep2 wmax_lemma)
   have "([trm.Max θ⇩1 θ⇩2]<>ν) = (wmax l1 l2, wmax u1 u2)"
     using lu1 lu2 unfolding wMaxU Let_def 
     by (simp)
   then show "[trm.Max θ⇩1 θ⇩2]<>ν ≡⇩P max r1 r2"
    unfolding repP_def
    using lbound ubound lu1 lu2 by auto
next
  case rtsem_Min
    fix θ⇩1 :: "trm" and ν' r1 and θ⇩2 :: "trm" and  r2
   assume eval1:"([θ⇩1]ν' ↓ r1)"
   assume eval2:"([θ⇩2]ν' ↓ r2)"
   assume rep:"ν REP ν'"
   assume "(ν REP ν' ⟹ [θ⇩1]<>ν ≡⇩P r1)"
   then have IH1:"[θ⇩1]<>ν ≡⇩P r1" using rep by auto
   assume "(ν REP ν' ⟹ [θ⇩2]<>ν ≡⇩P r2)"
   then have IH2:"[θ⇩2]<>ν ≡⇩P r2" using rep by auto
   obtain l1 u1 l2 u2 where 
        lu1:"([θ⇩1]<> ν) = (l1, u1)" 
    and lu2:"([θ⇩2]<> ν) = (l2, u2)"
    using IH1 IH2 repP_def by auto
   from IH1 IH2 
   obtain ub1 ub2 lb1 lb2:: real 
   where urep1:"(ub1 ≥ r1) ∧ (snd ([θ⇩1]<>ν) ≡⇩E ub1)" 
   and   urep2:"(ub2 ≥ r2) ∧ (snd ([θ⇩2]<>ν) ≡⇩E ub2)"
   and   lrep1:"(lb1 ≤ r1) ∧ (fst ([θ⇩1]<>ν) ≡⇩E lb1)" 
   and   lrep2:"(lb2 ≤ r2) ∧ (fst ([θ⇩2]<>ν) ≡⇩E lb2)"
     using prod.case_eq_if repP_def  repU_def repL_def by auto
   have lbound:"wmin l1 l2 ≡⇩L min r1 r2"
     by (metis fst_conv lrep1 lrep2 lu1 lu2 min.mono repL_def wmin_lemma)
   have ubound:"wmin u1 u2 ≡⇩U min r1 r2"     
     using lu1 lu2 min_le_iff_disj repU_def urep1 urep2 by auto
   have "([Min θ⇩1 θ⇩2]<>ν) = (wmin l1 l2, wmin u1 u2)"
     using lu1 lu2 unfolding wMinU Let_def by auto
  then show "[Min θ⇩1 θ⇩2]<>ν ≡⇩P min r1 r2"
    unfolding repP_def
    using lbound ubound lu1 lu2 by auto
next
  case rtsem_Neg
  fix θ :: "trm" and ν' r
  assume eval:"[θ]ν' ↓ r"
  assume rep:"ν REP ν'"
  assume "(ν REP ν' ⟹ [θ]<>ν ≡⇩P r)"
  then have IH:"[θ]<>ν ≡⇩P r" using rep by auto
  obtain l1 u1  where 
        lu:"([θ]<> ν) = (l1, u1)" 
    using IH repP_def by auto
  from IH 
  obtain ub lb:: real 
   where urep:"(ub ≥ r) ∧ (snd ([θ]<>ν) ≡⇩E ub)" 
   and   lrep:"(lb ≤ r) ∧ (fst ([θ]<>ν) ≡⇩E lb)" 
    using  repP_def repU_def repL_def by auto
  have ubound:"((wneg u1) ≡⇩L (uminus r))"
    by (metis real_minus_le_minus lu repL_def snd_conv urep wneg_lemma)
  have lbound:"((wneg l1) ≡⇩U (uminus r))"
    using real_minus_le_minus lu repU_def lrep wneg_lemma
    by (metis fst_conv)
  show "[Neg θ]<>ν ≡⇩P - r"
    unfolding repP_def Let_def using ubound lbound lu 
    by (auto)
next
  case rtsem_Abs
  fix θ :: "trm" and ν' r
  assume eval:"[θ]ν' ↓ r"
  assume rep:"ν REP ν'"
  assume "(ν REP ν' ⟹ [θ]<>ν ≡⇩P r)"
  then have IH:"[θ]<>ν ≡⇩P r" using rep by auto
  obtain l1 u1  where 
        lu:"([θ]<> ν) = (l1, u1)" 
    using IH repP_def by auto
  from IH 
  obtain ub lb:: real 
   where urep:"(ub ≥ r) ∧ (snd ([θ]<>ν) ≡⇩E ub)" 
   and   lrep:"(lb ≤ r) ∧ (fst ([θ]<>ν) ≡⇩E lb)" 
    using prod.case_eq_if repP_def  repU_def repL_def by auto
  have lbound:"wmax l1 (wneg u1) ≡⇩L (abs r)"
    apply(simp only: repL_def)
    apply(rule exI[where x="max lb (- ub)"])
    apply(rule conjI)  
    using lrep wmax_lemma lu urep wneg_lemma by auto
  have ubound:"(wmax u1 (wneg l1) ≡⇩U (abs r))"
    apply(simp only: repU_def)
    apply(rule exI[where x="max ub (- lb)"])
    using lrep wmax_lemma lu urep wneg_lemma by auto 
  show "[Abs θ]<>ν ≡⇩P abs r"
    using repP_def Let_def ubound lbound lu lu wAbsU by auto
qed

text‹Every word represents some real›
lemma word_rep:"⋀bw::bword. ∃r::real. Rep_bword bw ≡⇩E r"
proof -
  fix bw
  obtain w where weq:"w = Rep_bword bw" by auto
  have negInfCase:"w = NEG_INF ⟹ ?thesis bw"
   apply(rule exI[where x="-((2 ^ 31) -1)"])
    using weq by (auto simp add: repe.simps)
  have posInfCase:"w = POS_INF ⟹ ?thesis bw"
    apply(rule exI[where x="((2 ^ 31) -1)"])
    using weq by (auto simp add: repe.simps)
  have boundU:"w ≠ NEG_INF ⟹ w ≠ POS_INF ⟹ sint (Rep_bword bw) < sint POS_INF"
    using Rep_bword [of bw]
    by (auto simp: less_le weq [symmetric] dest: sint_dist)
  have boundL:"w ≠ NEG_INF ⟹ w ≠ POS_INF ⟹ sint NEG_INF < sint (Rep_bword bw)"
    using Rep_bword [of bw]
    by (auto simp: less_le weq [symmetric] dest: sint_dist)
  have intCase:"w ≠ NEG_INF ⟹ w ≠ POS_INF ⟹ ?thesis bw"
    apply(rule exI[where x=" (real_of_int (sint (Rep_bword bw)))"])
    apply(rule repINT)
    using boundU boundL by(auto)
  then show "?thesis bw"
    apply(cases "w = POS_INF")
     apply(cases "w = NEG_INF")
      using posInfCase intCase negInfCase by auto
  qed

text‹Every term has a value›
lemma eval_tot:"(∃r. ([θ::trm]ν' ↓ r))"
proof (induction "θ")
qed (auto simp add: Min_def word_rep bword_neg_one_def, blast?)

text‹Interval formula semantics soundly implies real semantics›
lemma fml_sound:
  fixes φ::"formula" and ν::"wstate"
  shows "(wfsem φ ν b) ⟹  (ν REP ν') ⟹ (rfsem φ ν'  b)"
proof (induction arbitrary: ν' rule: wfsem.induct)
case (wGreaterT t1 v t2 w)
  assume wle:"wgreater (fst ([t1]<>v)) (snd ([t2]<>v))"
  assume rep:"v REP w" 
  obtain r1 and r2 where eval1:"[t1]w ↓ r1" and  eval2:"[t2]w ↓ r2"
    using eval_tot[of t1 w] eval_tot[of t2 w] by (auto)
  note rep1 = trm_sound[of t1 w r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 w r2, where ν=v, OF eval2 rep]
  show "[Greater t1 t2]w ⇂ True"
    apply(rule rGreaterT[where ?r1.0 = r1, where ?r2.0 = r2]) 
    prefer 3
    apply(rule wgreater_lemma[where ?w1.0="fst([t1]<> v)", where ?w2.0="snd([t2]<> v)"])
    using rep1 rep2 wle repP_def repL_def repU_def  eval1 eval2 
    by ((simp add: prod.case_eq_if | blast)+)
next
  case (wGreaterF t2 v t1 v')
  assume wl:"wgeq (fst ([t2]<>v)) (snd ([t1]<>v))"
  assume rep:"v REP v'"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
    eval2:"rtsem t2 v' r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v']  by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Greater t1 t2]v' ⇂ False"
    apply(rule rGreaterF [of t1 v' r1 t2 r2])
    apply(rule eval1)
     apply(rule eval2)
    apply(rule wgeq_lemma[where ?w1.0="fst([t2]<> v)", where ?w2.0="snd([t1]<> v)"])
    using rep1 rep2 repP_def wgeq_lemma wl rep
    by auto
next
  case (wGeqT t1 v t2 v')
  assume a1:"wgeq (fst ([t1]<>v)) (snd ([t2]<>v))"
  assume rep:"v REP v'"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
    eval2:"rtsem t2 v' r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v']  by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Geq t1 t2]v' ⇂ True"
    apply(rule rGeqT)
      apply(rule eval1)
    apply(rule eval2)
  using wgeq_lemma eval1 eval2 rep1 rep2 unfolding repP_def Let_def
  using wgreater_lemma prod.case_eq_if a1
  by auto
next
  case (wGeqF t2 v t1 v')
  assume a1:"wgreater (fst ([t2]<>v)) (snd ([t1]<>v))"
  assume rep:"v REP v'"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
    eval2:"rtsem t2 v'  r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v'] by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Geq t1 t2]v' ⇂ False"
    apply(rule rGeqF, rule eval1, rule eval2)
  using wgeq_lemma eval1 eval2 rep1 rep2 unfolding repP_def Let_def
  using wgreater_lemma rGreaterF prod.case_eq_if a1 rGreaterF by auto
next
  case (wEqualsT t2 v t1 v')
  assume eq1:"fst ([t2]<>v) = snd ([t2]<>v)"
  assume eq2:"snd ([t2]<>v) = snd ([t1]<>v)"
  assume eq3:"snd ([t1]<>v) = fst ([t1]<>v)"
  assume rep:"v REP v'"  
  assume neq1:"fst ([t2]<>v) ≠ NEG_INF"
  assume neq2:"fst ([t2]<>v) ≠ POS_INF"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
        eval2:"rtsem t2 v'  r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v'] by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Equals t1 t2]v' ⇂ True"
    apply(rule rEqualsT, rule eval1, rule eval2)
    using eq1 eq2 eq3 eval1 eval2 rep1 rep2
    unfolding repP_def Let_def repL_def repU_def repe.simps using neq1 neq2 by auto
next
  case (wEqualsF1 t1 v t2 v')
  assume wle:"wgreater (fst ([t1]<>v)) (snd ([t2]<>v))"
  assume rep:"v REP v'"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
    eval2:"rtsem t2 v'  r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v'] by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Equals t1 t2]v' ⇂ False"
  apply(rule rEqualsF, rule eval1, rule eval2)
    using wgeq_lemma eval1 eval2 rep1 rep2 wgreater_lemma rGreaterF  prod.case_eq_if wle
    unfolding repP_def
    by (metis (no_types, lifting) less_irrefl) 
next
  case (wEqualsF2 t2 v t1 v')
  assume wle:"wgreater (fst ([t2]<>v)) (snd ([t1]<>v))"
  assume rep:"v REP v'"
  obtain r1 r2:: real
  where eval1:"(rtsem t1 v' r1)" and  
    eval2:"rtsem t2 v'  r2"
    using eval_tot[of t1 v'] eval_tot[of t2 v'] by (auto)
  note rep1 = trm_sound[of t1 v' r1, where ν=v, OF eval1 rep]
  note rep2 = trm_sound[of t2 v' r2, where ν=v, OF eval2 rep]
  show "[Equals t1 t2]v' ⇂ False"
    apply(rule rEqualsF, rule eval1, rule eval2)
    using wgeq_lemma eval1 eval2 rep1 rep2  wgreater_lemma rGreaterF prod.case_eq_if wle
    unfolding repP_def
    by (metis (no_types, lifting) less_irrefl)
qed (auto)
  
lemma rep_upd:"ω = (ν(Inr x := snd([θ]<>ν)))(Inl x := fst([θ]<>ν))
⟹ ν REP ν' ⟹ ([θ::trm]ν' ↓ r) ⟹ ω REP ν'(x := r)"
  apply(rule REPI)
  apply(rule conjI)
   apply(unfold repL_def)
   using trm_sound prod.case_eq_if repP_def repstate_simps repL_def 
   apply(metis (no_types, lifting) Inl_Inr_False fun_upd_apply sum.inject(1))
  using repP_def repstate_simps repU_def
  apply(auto simp add: repU_def)
  by (metis (full_types) surjective_pairing trm_sound)

text‹Interval program semantics soundly contains real semantics existentially›
theorem interval_program_sound:
  fixes α::"prog"
  shows "([[α]] ν ↓ ω)  ⟹ ν REP ν' ⟹ (∃ω'. (ω REP ω') ∧ ([α] ν' ⇃ ω'))"
proof (induction arbitrary: ν' rule: wpsem.induct)
  case (wTest φ ν ω ν') 
  assume sem:"[[φ]]ν ↓ True"
  and eq:"ν = ω"
  and rep:"ν REP ν'"
  show ?case 
    apply(rule exI[where x=ν'])
    using sem rep by (auto simp add: eq fml_sound rep)
next
  case (wAssign ω ν x θ ν') 
  assume eq:"ω = ν(Inr x := snd ([θ]<>ν), Inl x := fst ([θ]<>ν))"
  and rep:"ν REP ν'"
  obtain r::real where eval:"([θ::trm]ν' ↓ r)" using eval_tot  by auto
  show ?case 
    apply(rule exI[where x="ν'(x := r)"])
    apply(rule conjI)
    apply(rule rep_upd[OF eq rep eval])
    apply auto
    apply(rule exI[where x=r])
    by (auto simp add: eval)
next case (wSeq α ν μ β ω ν') then show ?case by (simp, blast)
next case (wChoice1 a v w b v') then show ?case by auto
next case (wChoice2 a v w b v') then show ?case by auto
qed

end