Quelle  Monitor.thy

(*<*)
theory Monitor
  imports Checker_Code
begin
(*>*)

section ‹Unverified Explanation-Producing Monitoring Algorithm›

fun merge_part2_raw :: "('a ==> 'b ==> 'c) ==> ('d set × 'a) list ==> ('d set × 'b) list ==> ('d set × 'c) list" where
  "merge_part2_raw f [] _ = []"  
| "merge_part2_raw f ((P1, v1) # part1) part2 =
    (let part12 = List.map_filter (λ(P2, v2). if P1 ∩ P2 ≠ {} then Some(P1 ∩ P2, f v1 v2) else None) part2 in
     let part2not1 = List.map_filter (λ(P2, v2). if P2 - P1 ≠ {} then Some(P2 - P1, v2) else None) part2 in
     part12 @ (merge_part2_raw f part1 part2not1))"

fun merge_part3_raw :: "('a ==> 'b ==> 'c ==> 'e) ==> ('d set × 'a) list ==> ('d set × 'b) list ==> ('d set × 'c) list ==> ('d set × 'e) list" where
  "merge_part3_raw f [] _ _ = []" 
| "merge_part3_raw f _ [] _ = []" 
| "merge_part3_raw f _ _ [] = []"
| "merge_part3_raw f part1 part2 part3 = merge_part2_raw (λpt3 f'. f' pt3) part3 (merge_part2_raw f part1 part2)"

lemma partition_on_empty_iff: 
  "partition_on X P ==> P = {} ⟷ X = {}"
  "partition_on X P ==> P ≠ {} ⟷ X ≠ {}"
  by (auto simp: partition_on_def)

lemma wf_part_list_filter_inter: 
  defines "inP1 P1 f v1 part2
    ≡ List.map_filter (λ(P2, v2). if P1 ∩ P2 ≠ {} then Some(P1 ∩ P2, f v1 v2) else None) part2"
  assumes "partition_on X (set (map fst ((P1, v1) # part1)))"
    and "partition_on X (set (map fst part2))"
  shows "partition_on P1 (set (map fst (inP1 P1 f v1 part2)))"
    and "distinct (map fst ((P1, v1) # part1)) ==> distinct (map fst (part2)) ==>
    distinct (map fst (inP1 P1 f v1 part2))"
proof (rule partition_onI)
  show "∪ (set (map fst (inP1 P1 f v1 part2))) = P1"
  proof -
    have "∃P2. (P1 ∩ P2 ≠ {} ⟶ (∃v2. (P2, v2) ∈ set part2) ∧ x ∈ P2) ∧ P1 ∩ P2 ≠ {}"
      if "∪ (fst ` set part2) = P1 ∪ ∪ (fst ` set part1)" and "x ∈ P1" for x
      using that by (metis (no_types, lifting) Int_iff UN_iff Un_Int_eq(3) empty_iff prod.collapse)
    with partition_onD1[OF assms(2)] partition_onD1[OF assms(3)] show ?thesis
      by (auto simp: map_filter_def inP1_def split: if_splits)
  qed
  show "∧A1 A2. A1 ∈ set (map fst (inP1 P1 f v1 part2)) ==>
    A2 ∈ set (map fst (inP1 P1 f v1 part2)) ==> A1 ≠ A2 ==> disjnt A1 A2" 
    using partition_onD2[OF assms(2)] partition_onD2[OF assms(3)]
    by (force simp: disjnt_iff map_filter_def disjoint_def inP1_def split: if_splits)
  show "{} ∉ set (map fst (inP1 P1 f v1 part2))" 
    using assms
    by (auto simp: map_filter_def split: if_splits)
  show "distinct (map fst ((P1, v1) # part1)) ==> distinct (map fst part2) ==>
    distinct (map fst (inP1 P1 f v1 part2))"
    using partition_onD2[OF assms(3), unfolded disjoint_def, simplified, rule_format]
    by (clarsimp simp: inP1_def map_filter_def distinct_map inj_on_def Ball_def) blast
qed

lemma wf_part_list_filter_minus: 
  defines "notinP2 P1 f v1 part2
    ≡ List.map_filter (λ(P2, v2). if P2 - P1 ≠ {} then Some(P2 - P1, v2) else None) part2"
  assumes "partition_on X (set (map fst ((P1, v1) # part1)))"
    and "partition_on X (set (map fst part2))"
  shows "partition_on (X - P1) (set (map fst (notinP2 P1 f v1 part2)))"
    and "distinct (map fst ((P1, v1) # part1)) ==> distinct (map fst (part2)) ==>
      distinct (map fst (notinP2 P1 f v1 part2))"
proof (rule partition_onI)
  show "∪ (set (map fst (notinP2 P1 f v1 part2))) = X - P1"
  proof -
    have "∃P2. ((∃x∈P2. x ∉ P1) ⟶ (∃v2. (P2, v2) ∈ set part2)) ∧ (∃x∈P2. x ∉ P1) ∧ x ∈ P2"
      if "∪ (fst ` set part2) = P1 ∪ ∪ (fst ` set part1)" "x ∉ P1" "(P1', v1) ∈ set part1" "x ∈ P1'" for x P1' v1
      using that by (metis (no_types, lifting) UN_iff Un_iff fst_conv prod.collapse)
    with partition_onD1[OF assms(2)] partition_onD1[OF assms(3)] show ?thesis
      by (auto simp: map_filter_def subset_eq split_beta notinP2_def split: if_splits)
  qed
  show "∧A1 A2. A1 ∈ set (map fst (notinP2 P1 f v1 part2)) ==>
    A2 ∈ set (map fst (notinP2 P1 f v1 part2)) ==> A1 ≠ A2 ==> disjnt A1 A2" 
    using partition_onD2[OF assms(3)]
    by (auto simp: disjnt_def map_filter_def disjoint_def notinP2_def Ball_def Bex_def image_iff split: if_splits)
  show "{} ∉ set (map fst (notinP2 P1 f v1 part2))" 
    using assms
    by (auto simp: map_filter_def split: if_splits)
  show "distinct (map fst ((P1, v1) # part1)) ==> distinct (map fst part2) ==>
    distinct (map fst ((notinP2 P1 f v1 part2)))"
    using partition_onD2[OF assms(3), unfolded disjoint_def]
    by (clarsimp simp: notinP2_def map_filter_def distinct_map inj_on_def Ball_def Bex_def image_iff) blast
qed

lemma wf_part_list_tail: 
  assumes "partition_on X (set (map fst ((P1, v1) # part1)))"
    and "distinct (map fst ((P1, v1) # part1))"
  shows "partition_on (X - P1) (set (map fst part1))"
    and "distinct (map fst part1)"
proof (rule partition_onI)
  show "∪ (set (map fst part1)) = X - P1"
    using partition_onD1[OF assms(1)] partition_onD2[OF assms(1)] assms(2)
    by (auto simp: disjoint_def image_iff)
  show "∧A1 A2. A1 ∈ set (map fst part1) ==> A2 ∈ set (map fst part1) ==> A1 ≠ A2 ==> disjnt A1 A2" 
    using partition_onD2[OF assms(1)]
    by (clarsimp simp: disjnt_def disjoint_def)
      (smt (verit, ccfv_SIG) Diff_disjoint Int_Diff Int_commute fst_conv)
  show "{} ∉ set (map fst part1)" 
    using partition_onD3[OF assms(1)]
    by (auto simp: map_filter_def split: if_splits)
  show "distinct (map fst (part1))"
    using assms(2)
    by auto
qed

lemma partition_on_append: "partition_on X (set xs) ==> partition_on Y (set ys) ==> X ∩ Y = {} ==>
  partition_on (X ∪ Y) (set (xs @ ys))"
  by (auto simp: partition_on_def intro!: disjoint_union)

lemma wf_part_list_merge_part2_raw: 
  "partition_on X (set (map fst part1)) ∧ distinct (map fst part1) ==>
   partition_on X (set (map fst part2)) ∧ distinct (map fst part2) ==>
   partition_on X (set (map fst (merge_part2_raw f part1 part2)))
    ∧ distinct (map fst (merge_part2_raw f part1 part2))"
proof(induct f part1 part2 arbitrary: X rule: merge_part2_raw.induct)
  case (2 f P1 v1 part1 part2)
  let ?inP1 = "List.map_filter (λ(P2, v2). if P1 ∩ P2 ≠ {} then Some (P1 ∩ P2, f v1 v2) else None) part2"
    and ?notinP1 = "List.map_filter (λ(P2, v2). if P2 - P1 ≠ {} then Some (P2 - P1, v2) else None) part2"
  have "P1 ∪ X = X"
    using "2.prems"
    by (auto simp: partition_on_def)
  have wf_part1: "partition_on (X - P1) (set (map fst part1))"
    "distinct (map fst part1)"
    using wf_part_list_tail "2.prems" by auto
  moreover have wf_notinP1: "partition_on (X - P1) (set (map fst ?notinP1))" 
    "distinct (map fst (?notinP1))"
    using wf_part_list_filter_minus[OF 2(2)[THEN conjunct1]] 
      "2.prems" by auto
  ultimately have IH: "partition_on (X - P1) (set (map fst (merge_part2_raw f part1 (?notinP1))))"
    "distinct (map fst (merge_part2_raw f part1 (?notinP1)))"
    using "2.hyps"[OF refl refl] by auto
  moreover have wf_inP1: "partition_on P1 (set (map fst ?inP1))" "distinct (map fst ?inP1)"
    using wf_part_list_filter_inter[OF 2(2)[THEN conjunct1]]
      "2.prems" by auto
  moreover have "(fst ` set ?inP1) ∩ (fst ` set (merge_part2_raw f part1 (?notinP1))) = {}"
    using IH(1)[THEN partition_onD1]
    by (fastforce simp: map_filter_def split: prod.splits if_splits)
  ultimately show ?case 
    using partition_on_append[OF wf_inP1(1) IH(1)] ‹P1 ∪ X = X› wf_inP1(2) IH(2)
    by simp
qed simp

lemma wf_part_list_merge_part3_raw: 
  "partition_on X (set (map fst part1)) ∧ distinct (map fst part1) ==>
   partition_on X (set (map fst part2)) ∧ distinct (map fst part2) ==>
   partition_on X (set (map fst part3)) ∧ distinct (map fst part3) ==>
   partition_on X (set (map fst (merge_part3_raw f part1 part2 part3)))
    ∧ distinct (map fst (merge_part3_raw f part1 part2 part3))"
proof(induct f part1 part2 part3 arbitrary: X rule: merge_part3_raw.induct)
  case (4 f v va vb vc vd ve)
  have "partition_on X (set (map fst (v # va))) ∧ distinct (map fst (vb # vc))"
    using 4 by blast
  moreover have "partition_on X (set (map fst (vb # vc))) ∧ distinct (map fst (vb # vc))"
    using 4 by blast
  ultimately have "partition_on X (set (map fst (merge_part2_raw f (v # va) (vb # vc))))
  ∧ distinct (map fst (merge_part2_raw f (v # va) (vb # vc)))"
    using wf_part_list_merge_part2_raw[of X "(v # va)" "(vb # vc)" f] 4
    by fastforce
  moreover have "partition_on X (set (map fst (vd # ve))) ∧ distinct (map fst (vd # ve))"
    using 4 by blast
  ultimately show ?case 
    using wf_part_list_merge_part2_raw[of X "(vd # ve)" "(merge_part2_raw f (v # va) (vb # vc))" "(λpt3 f'. f' pt3)"]
    by simp
qed auto

lift_definition merge_part2 :: "('a ==> 'a ==> 'a) ==> ('d, 'a) part ==> ('d, 'a) part ==> ('d, 'a) part" is merge_part2_raw
  by (rule wf_part_list_merge_part2_raw)

lift_definition merge_part3 :: "('a ==> 'a ==> 'a ==> 'a) ==> ('d, 'a) part ==> ('d, 'a) part ==> ('d, 'a) part ==> ('d, 'a) part" is merge_part3_raw
  by (rule wf_part_list_merge_part3_raw)

definition proof_app :: "('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof" (infixl ‹⊕› 65) where
  "p ⊕ q = (case (p, q) of
   (Inl (SHistorically i li sps), Inl q) ==> Inl (SHistorically (i+1) li (sps @ [q]))
 | (Inl (SAlways i hi sps), Inl q) ==> Inl (SAlways (i-1) hi (q # sps))
 | (Inl (SSince sp2 sp1s), Inl q) ==> Inl (SSince sp2 (sp1s @ [q]))
 | (Inl (SUntil sp1s sp2), Inl q) ==> Inl (SUntil (q # sp1s) sp2)
 | (Inr (VSince i vp1 vp2s), Inr q) ==> Inr (VSince (i+1) vp1 (vp2s @ [q]))
 | (Inr (VOnce i li vps), Inr q) ==> Inr (VOnce (i+1) li (vps @ [q]))
 | (Inr (VEventually i hi vps), Inr q) ==> Inr (VEventually (i-1) hi (q # vps))
 | (Inr (VSinceInf i li vp2s), Inr q) ==> Inr (VSinceInf (i+1) li (vp2s @ [q]))
 | (Inr (VUntil i vp2s vp1), Inr q) ==> Inr (VUntil (i-1) (q # vp2s) vp1)
 | (Inr (VUntilInf i hi vp2s), Inr q) ==> Inr (VUntilInf (i-1) hi (q # vp2s)))"

definition proof_incr :: "('n, 'd) proof ==> ('n, 'd) proof" where
  "proof_incr p = (case p of
   Inl (SOnce i sp) ==> Inl (SOnce (i+1) sp)
 | Inl (SEventually i sp) ==> Inl (SEventually (i-1) sp)
 | Inl (SHistorically i li sps) ==> Inl (SHistorically (i+1) li sps)
 | Inl (SAlways i hi sps) ==> Inl (SAlways (i-1) hi sps)
 | Inr (VSince i vp1 vp2s) ==> Inr (VSince (i+1) vp1 vp2s)
 | Inr (VOnce i li vps) ==> Inr (VOnce (i+1) li vps)
 | Inr (VEventually i hi vps) ==> Inr (VEventually (i-1) hi vps)
 | Inr (VHistorically i vp) ==> Inr (VHistorically (i+1) vp)
 | Inr (VAlways i vp) ==> Inr (VAlways (i-1) vp)
 | Inr (VSinceInf i li vp2s) ==> Inr (VSinceInf (i+1) li vp2s)
 | Inr (VUntil i vp2s vp1) ==> Inr (VUntil (i-1) vp2s vp1)
 | Inr (VUntilInf i hi vp2s) ==> Inr (VUntilInf (i-1) hi vp2s))"

definition min_list_wrt :: "(('n, 'd) proof ==> ('n, 'd) proof ==> bool) ==> ('n, 'd) proof list ==> ('n, 'd) proof" where
  "min_list_wrt r xs = hd [x ← xs. ∀y ∈ set xs. r x y]"

definition do_neg :: "('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_neg p = (case p of
  Inl sp ==> [Inr (VNeg sp)]
| Inr vp ==> [Inl (SNeg vp)])"

definition do_or :: "('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_or p1 p2 = (case (p1, p2) of
  (Inl sp1, Inl sp2) ==> [Inl (SOrL sp1), Inl (SOrR sp2)]
| (Inl sp1, Inr _ ) ==> [Inl (SOrL sp1)]
| (Inr _ , Inl sp2) ==> [Inl (SOrR sp2)]
| (Inr vp1, Inr vp2) ==> [Inr (VOr vp1 vp2)])"

definition do_and :: "('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_and p1 p2 = (case (p1, p2) of
  (Inl sp1, Inl sp2) ==> [Inl (SAnd sp1 sp2)]
| (Inl _ , Inr vp2) ==> [Inr (VAndR vp2)]
| (Inr vp1, Inl _ ) ==> [Inr (VAndL vp1)]
| (Inr vp1, Inr vp2) ==> [Inr (VAndL vp1), Inr (VAndR vp2)])"

definition do_imp :: "('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_imp p1 p2 = (case (p1, p2) of
  (Inl _ , Inl sp2) ==> [Inl (SImpR sp2)]
| (Inl sp1, Inr vp2) ==> [Inr (VImp sp1 vp2)]
| (Inr vp1, Inl sp2) ==> [Inl (SImpL vp1), Inl (SImpR sp2)]
| (Inr vp1, Inr _ ) ==> [Inl (SImpL vp1)])"

definition do_iff :: "('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_iff p1 p2 = (case (p1, p2) of
  (Inl sp1, Inl sp2) ==> [Inl (SIffSS sp1 sp2)]
| (Inl sp1, Inr vp2) ==> [Inr (VIffSV sp1 vp2)]
| (Inr vp1, Inl sp2) ==> [Inr (VIffVS vp1 sp2)]
| (Inr vp1, Inr vp2) ==> [Inl (SIffVV vp1 vp2)])"

definition do_exists :: "'n ==> ('n, 'd::{default,linorder}) proof + ('d, ('n, 'd) proof) part ==> ('n, 'd) proof list" where
  "do_exists x p_part = (case p_part of
  Inl p ==> (case p of
    Inl sp ==> [Inl (SExists x default sp)]
  | Inr vp ==> [Inr (VExists x (trivial_part vp))])
| Inr part ==> (if (∃x∈Vals part. isl x) then
                map (λ(D,p). map_sum (SExists x (Min D)) id p) (filter (λ(_, p). isl p) (subsvals part))
              else
                [Inr (VExists x (map_part projr part))]))"

definition do_forall :: "'n ==> ('n, 'd::{default,linorder}) proof + ('d, ('n, 'd) proof) part ==> ('n, 'd) proof list" where
  "do_forall x p_part = (case p_part of
  Inl p ==> (case p of
    Inl sp ==> [Inl (SForall x (trivial_part sp))]
  | Inr vp ==> [Inr (VForall x default vp)])
| Inr part ==> (if (∀x∈Vals part. isl x) then
                [Inl (SForall x (map_part projl part))]
              else
                map (λ(D,p). map_sum id (VForall x (Min D)) p) (filter (λ(_, p). ¬isl p) (subsvals part))))"

definition do_prev :: "nat ==> I ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_prev i I t p = (case (p, t < left I) of
  (Inl _ , True) ==> [Inr (VPrevOutL i)]
| (Inl sp, False) ==> (if mem t I then [Inl (SPrev sp)] else [Inr (VPrevOutR i)])
| (Inr vp, True) ==> [Inr (VPrev vp), Inr (VPrevOutL i)]
| (Inr vp, False) ==> (if mem t I then [Inr (VPrev vp)] else [Inr (VPrev vp), Inr (VPrevOutR i)]))"

definition do_next :: "nat ==> I ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_next i I t p = (case (p, t < left I) of
  (Inl _ , True) ==> [Inr (VNextOutL i)]
| (Inl sp, False) ==> (if mem t I then [Inl (SNext sp)] else [Inr (VNextOutR i)])
| (Inr vp, True) ==> [Inr (VNext vp), Inr (VNextOutL i)]
| (Inr vp, False) ==> (if mem t I then [Inr (VNext vp)] else [Inr (VNext vp), Inr (VNextOutR i)]))"

definition do_once_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_once_base i a p' = (case (p', a = 0) of
  (Inl sp', True) ==> [Inl (SOnce i sp')]
| (Inr vp', True) ==> [Inr (VOnce i i [vp'])]
| ( _ , False) ==> [Inr (VOnce i i [])])"

definition do_once :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_once i a p p' = (case (p, a = 0, p') of
  (Inl sp, True, Inr _ ) ==> [Inl (SOnce i sp)]
| (Inl sp, True, Inl (SOnce _ sp')) ==> [Inl (SOnce i sp'), Inl (SOnce i sp)]
| (Inl _ , False, Inl (SOnce _ sp')) ==> [Inl (SOnce i sp')]
| (Inl _ , False, Inr (VOnce _ li vps')) ==> [Inr (VOnce i li vps')]
| (Inr _ , True, Inl (SOnce _ sp')) ==> [Inl (SOnce i sp')]
| (Inr vp, True, Inr vp') ==> [(Inr vp') ⊕ (Inr vp)]
| (Inr _ , False, Inl (SOnce _ sp')) ==> [Inl (SOnce i sp')]
| (Inr _ , False, Inr (VOnce _ li vps')) ==> [Inr (VOnce i li vps')])"

definition do_eventually_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_eventually_base i a p' = (case (p', a = 0) of
  (Inl sp', True) ==> [Inl (SEventually i sp')]
| (Inr vp', True) ==> [Inr (VEventually i i [vp'])]
| ( _ , False) ==> [Inr (VEventually i i [])])"

definition do_eventually :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_eventually i a p p' = (case (p, a = 0, p') of
  (Inl sp, True, Inr _ ) ==> [Inl (SEventually i sp)]
| (Inl sp, True, Inl (SEventually _ sp')) ==> [Inl (SEventually i sp'), Inl (SEventually i sp)]
| (Inl _ , False, Inl (SEventually _ sp')) ==> [Inl (SEventually i sp')]
| (Inl _ , False, Inr (VEventually _ hi vps')) ==> [Inr (VEventually i hi vps')]
| (Inr _ , True, Inl (SEventually _ sp')) ==> [Inl (SEventually i sp')]
| (Inr vp, True, Inr vp') ==> [(Inr vp') ⊕ (Inr vp)]
| (Inr _ , False, Inl (SEventually _ sp')) ==> [Inl (SEventually i sp')]
| (Inr _ , False, Inr (VEventually _ hi vps')) ==> [Inr (VEventually i hi vps')])"

definition do_historically_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_historically_base i a p' = (case (p', a = 0) of
  (Inl sp', True) ==> [Inl (SHistorically i i [sp'])]
| (Inr vp', True) ==> [Inr (VHistorically i vp')]
| ( _ , False) ==> [Inl (SHistorically i i [])])"

definition do_historically :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_historically i a p p' = (case (p, a = 0, p') of
  (Inl _ , True, Inr (VHistorically _ vp')) ==> [Inr (VHistorically i vp')]
| (Inl sp, True, Inl sp') ==> [(Inl sp') ⊕ (Inl sp)]
| (Inl _ , False, Inl (SHistorically _ li sps')) ==> [Inl (SHistorically i li sps')]
| (Inl _ , False, Inr (VHistorically _ vp')) ==> [Inr (VHistorically i vp')]
| (Inr vp, True, Inl _ ) ==> [Inr (VHistorically i vp)]
| (Inr vp, True, Inr (VHistorically _ vp')) ==> [Inr (VHistorically i vp), Inr (VHistorically i vp')]
| (Inr _ , False, Inl (SHistorically _ li sps')) ==> [Inl (SHistorically i li sps')]
| (Inr _ , False, Inr (VHistorically _ vp')) ==> [Inr (VHistorically i vp')])"

definition do_always_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_always_base i a p' = (case (p', a = 0) of
  (Inl sp', True) ==> [Inl (SAlways i i [sp'])]
| (Inr vp', True) ==> [Inr (VAlways i vp')]
| ( _ , False) ==> [Inl (SAlways i i [])])"

definition do_always :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_always i a p p' = (case (p, a = 0, p') of
  (Inl _ , True, Inr (VAlways _ vp')) ==> [Inr (VAlways i vp')]
| (Inl sp, True, Inl sp') ==> [(Inl sp') ⊕ (Inl sp)]
| (Inl _ , False, Inl (SAlways _ hi sps')) ==> [Inl (SAlways i hi sps')]
| (Inl _ , False, Inr (VAlways _ vp')) ==> [Inr (VAlways i vp')]
| (Inr vp, True, Inl _ ) ==> [Inr (VAlways i vp)]
| (Inr vp, True, Inr (VAlways _ vp')) ==> [Inr (VAlways i vp), Inr (VAlways i vp')]
| (Inr _ , False, Inl (SAlways _ hi sps')) ==> [Inl (SAlways i hi sps')]
| (Inr _ , False, Inr (VAlways _ vp')) ==> [Inr (VAlways i vp')])"

definition do_since_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_since_base i a p1 p2 = (case (p1, p2, a = 0) of
  ( _ , Inl sp2, True) ==> [Inl (SSince sp2 [])]
| (Inl _ , _ , False) ==> [Inr (VSinceInf i i [])]
| (Inl _ , Inr vp2, True) ==> [Inr (VSinceInf i i [vp2])]
| (Inr vp1, _ , False) ==> [Inr (VSince i vp1 []), Inr (VSinceInf i i [])]
| (Inr vp1, Inr sp2, True) ==> [Inr (VSince i vp1 [sp2]), Inr (VSinceInf i i [sp2])])"

definition do_since :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_since i a p1 p2 p' = (case (p1, p2, a = 0, p') of
  (Inl sp1, Inr _ , True, Inl sp') ==> [(Inl sp') ⊕ (Inl sp1)]
| (Inl sp1, _ , False, Inl sp') ==> [(Inl sp') ⊕ (Inl sp1)]
| (Inl sp1, Inl sp2, True, Inl sp') ==> [(Inl sp') ⊕ (Inl sp1), Inl (SSince sp2 [])]
| (Inl _ , Inr vp2, True, Inr (VSinceInf _ _ _ )) ==> [p' ⊕ (Inr vp2)]
| (Inl _ , _ , False, Inr (VSinceInf _ li vp2s')) ==> [Inr (VSinceInf i li vp2s')]
| (Inl _ , Inr vp2, True, Inr (VSince _ _ _ )) ==> [p' ⊕ (Inr vp2)]
| (Inl _ , _ , False, Inr (VSince _ vp1' vp2s')) ==> [Inr (VSince i vp1' vp2s')]
| (Inr vp1, Inr vp2, True, Inl _ ) ==> [Inr (VSince i vp1 [vp2])]
| (Inr vp1, _ , False, Inl _ ) ==> [Inr (VSince i vp1 [])]
| (Inr _ , Inl sp2, True, Inl _ ) ==> [Inl (SSince sp2 [])]
| (Inr vp1, Inr vp2, True, Inr (VSinceInf _ _ _ )) ==> [Inr (VSince i vp1 [vp2]), p' ⊕ (Inr vp2)]
| (Inr vp1, _, False, Inr (VSinceInf _ li vp2s')) ==> [Inr (VSince i vp1 []), Inr (VSinceInf i li vp2s')]
| ( _ , Inl sp2, True, Inr (VSinceInf _ _ _ )) ==> [Inl (SSince sp2 [])]
| (Inr vp1, Inr vp2, True, Inr (VSince _ _ _ )) ==> [Inr (VSince i vp1 [vp2]), p' ⊕ (Inr vp2)]
| (Inr vp1, _ , False, Inr (VSince _ vp1' vp2s')) ==> [Inr (VSince i vp1 []), Inr (VSince i vp1' vp2s')]
| ( _ , Inl vp2, True, Inr (VSince _ _ _ )) ==> [Inl (SSince vp2 [])])"

definition do_until_base :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_until_base i a p1 p2 = (case (p1, p2, a = 0) of
  ( _ , Inl sp2, True) ==> [Inl (SUntil [] sp2)]
| (Inl sp1, _ , False) ==> [Inr (VUntilInf i i [])]
| (Inl sp1, Inr vp2, True) ==> [Inr (VUntilInf i i [vp2])]
| (Inr vp1, _ , False) ==> [Inr (VUntil i [] vp1), Inr (VUntilInf i i [])]
| (Inr vp1, Inr vp2, True) ==> [Inr (VUntil i [vp2] vp1), Inr (VUntilInf i i [vp2])])"

definition do_until :: "nat ==> nat ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof list" where
  "do_until i a p1 p2 p' = (case (p1, p2, a = 0, p') of
  (Inl sp1, Inr _ , True, Inl (SUntil _ _ )) ==> [p' ⊕ (Inl sp1)]
| (Inl sp1, _ , False, Inl (SUntil _ _ )) ==> [p' ⊕ (Inl sp1)]
| (Inl sp1, Inl sp2, True, Inl (SUntil _ _ )) ==> [p' ⊕ (Inl sp1), Inl (SUntil [] sp2)]
| (Inl _ , Inr vp2, True, Inr (VUntilInf _ _ _ )) ==> [p' ⊕ (Inr vp2)]
| (Inl _ , _ , False, Inr (VUntilInf _ hi vp2s')) ==> [Inr (VUntilInf i hi vp2s')]
| (Inl _ , Inr vp2, True, Inr (VUntil _ _ _ )) ==> [p' ⊕ (Inr vp2)]
| (Inl _ , _ , False, Inr (VUntil _ vp2s' vp1')) ==> [Inr (VUntil i vp2s' vp1')]
| (Inr vp1, Inr vp2, True, Inl (SUntil _ _ )) ==> [Inr (VUntil i [vp2] vp1)]
| (Inr vp1, _ , False, Inl (SUntil _ _ )) ==> [Inr (VUntil i [] vp1)]
| (Inr vp1, Inl sp2, True, Inl (SUntil _ _ )) ==> [Inl (SUntil [] sp2)]
| (Inr vp1, Inr vp2, True, Inr (VUntilInf _ _ _ )) ==> [Inr (VUntil i [vp2] vp1), p' ⊕ (Inr vp2)]
| (Inr vp1, _ , False, Inr (VUntilInf _ hi vp2s')) ==> [Inr (VUntil i [] vp1), Inr (VUntilInf i hi vp2s')]
| ( _ , Inl sp2, True, Inr (VUntilInf _ hi vp2s')) ==> [Inl (SUntil [] sp2)]
| (Inr vp1, Inr vp2, True, Inr (VUntil _ _ _ )) ==> [Inr (VUntil i [vp2] vp1), p' ⊕ (Inr vp2)]
| (Inr vp1, _ , False, Inr (VUntil _ vp2s' vp1')) ==> [Inr (VUntil i [] vp1), Inr (VUntil i vp2s' vp1')]
| ( _ , Inl sp2, True, Inr (VUntil _ _ _ )) ==> [Inl (SUntil [] sp2)])"

fun match :: "('n, 'd) Formula.trm list ==> 'd list ==> ('n ⇀ 'd) option" where
  "match [] [] = Some Map.empty"
| "match (Formula.Const x # ts) (y # ys) = (if x = y then match ts ys else None)"
| "match (Formula.Var x # ts) (y # ys) = (case match ts ys of
      None ==> None
    | Some f ==> (case f x of
        None ==> Some (f(x ↦ y))
      | Some z ==> if y = z then Some f else None))"
| "match _ _ = None"

fun pdt_of :: "nat ==> 'n ==> ('n, 'd :: linorder) Formula.trm list ==> 'n list ==> ('n ⇀ 'd) list ==> ('n, 'd) expl" where
  "pdt_of i r ts [] V = (if List.null V then Leaf (Inr (VPred i r ts)) else Leaf (Inl (SPred i r ts)))"
| "pdt_of i r ts (x # vs) V =
     (let ds = remdups (List.map_filter (λv. v x) V);
          part = tabulate ds (λd. pdt_of i r ts vs (filter (λv. v x = Some d) V)) (pdt_of i r ts vs [])
     in Node x part)"

fun "apply_pdt1" :: "'n list ==> (('n, 'd) proof ==> ('n, 'd) proof) ==> ('n, 'd) expl ==> ('n, 'd) expl" where
  "apply_pdt1 vs f (Leaf pt) = Leaf (f pt)"
| "apply_pdt1 (z # vs) f (Node x part) =
  (if x = z then
     Node x (map_part (λexpl. apply_pdt1 vs f expl) part)
   else
     apply_pdt1 vs f (Node x part))"
| "apply_pdt1 [] _ (Node _ _) = undefined"

fun "apply_pdt2" :: "'n list ==> (('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof) ==> ('n, 'd) expl ==> ('n, 'd) expl ==> ('n, 'd) expl" where
  "apply_pdt2 vs f (Leaf pt1) (Leaf pt2) = Leaf (f pt1 pt2)"
| "apply_pdt2 vs f (Leaf pt1) (Node x part2) = Node x (map_part (apply_pdt1 vs (f pt1)) part2)"
| "apply_pdt2 vs f (Node x part1) (Leaf pt2) = Node x (map_part (apply_pdt1 vs (λpt1. f pt1 pt2)) part1)"
| "apply_pdt2 (z # vs) f (Node x part1) (Node y part2) =
    (if x = z ∧ y = z then
       Node z (merge_part2 (apply_pdt2 vs f) part1 part2)
     else if x = z then
       Node x (map_part (λexpl1. apply_pdt2 vs f expl1 (Node y part2)) part1)
     else if y = z then
       Node y (map_part (λexpl2. apply_pdt2 vs f (Node x part1) expl2) part2)
     else
       apply_pdt2 vs f (Node x part1) (Node y part2))"
| "apply_pdt2 [] _ (Node _ _) (Node _ _) = undefined"

fun "apply_pdt3" :: "'n list ==> (('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof ==> ('n, 'd) proof) ==> ('n, 'd) expl ==> ('n, 'd) expl ==> ('n, 'd) expl ==> ('n, 'd) expl" where
  "apply_pdt3 vs f (Leaf pt1) (Leaf pt2) (Leaf pt3) = Leaf (f pt1 pt2 pt3)"
| "apply_pdt3 vs f (Leaf pt1) (Leaf pt2) (Node x part3) = Node x (map_part (apply_pdt2 vs (f pt1) (Leaf pt2)) part3)" 
| "apply_pdt3 vs f (Leaf pt1) (Node x part2) (Leaf pt3) = Node x (map_part (apply_pdt2 vs (λpt2. f pt1 pt2) (Leaf pt3)) part2)"
| "apply_pdt3 vs f (Node x part1) (Leaf pt2) (Leaf pt3) = Node x (map_part (apply_pdt2 vs (λpt1. f pt1 pt2) (Leaf pt3)) part1)"
| "apply_pdt3 (w # vs) f (Leaf pt1) (Node y part2) (Node z part3) =
  (if y = w ∧ z = w then
     Node w (merge_part2 (apply_pdt2 vs (f pt1)) part2 part3)
   else if y = w then
     Node y (map_part (λexpl2. apply_pdt2 vs (f pt1) expl2 (Node z part3)) part2)
   else if z = w then
     Node z (map_part (λexpl3. apply_pdt2 vs (f pt1) (Node y part2) expl3) part3)
   else
     apply_pdt3 vs f (Leaf pt1) (Node y part2) (Node z part3))"
| "apply_pdt3 (w # vs) f (Node x part1) (Node y part2) (Leaf pt3) =
  (if x = w ∧ y = w then
     Node w (merge_part2 (apply_pdt2 vs (λpt1 pt2. f pt1 pt2 pt3)) part1 part2)
   else if x = w then
     Node x (map_part (λexpl1. apply_pdt2 vs (λpt1 pt2. f pt1 pt2 pt3) expl1 (Node y part2)) part1)
   else if y = w then
     Node y (map_part (λexpl2. apply_pdt2 vs (λpt1 pt2. f pt1 pt2 pt3) (Node x part1) expl2) part2)
   else
     apply_pdt3 vs f (Node x part1) (Node y part2) (Leaf pt3))"
| "apply_pdt3 (w # vs) f (Node x part1) (Leaf pt2) (Node z part3) =
  (if x = w ∧ z = w then
     Node w (merge_part2 (apply_pdt2 vs (λpt1. f pt1 pt2)) part1 part3)
   else if x = w then
     Node x (map_part (λexpl1. apply_pdt2 vs (λpt1. f pt1 pt2) expl1 (Node z part3)) part1)
   else if z = w then
     Node z (map_part (λexpl3. apply_pdt2 vs (λpt1. f pt1 pt2) (Node x part1) expl3) part3)
   else
     apply_pdt3 vs f (Node x part1) (Leaf pt2) (Node z part3))"
| "apply_pdt3 (w # vs) f (Node x part1) (Node y part2) (Node z part3) =
  (if x = w ∧ y = w ∧ z = w then
     Node z (merge_part3 (apply_pdt3 vs f) part1 part2 part3)
   else if x = w ∧ y = w then
     Node w (merge_part2 (apply_pdt3 vs (λpt3 pt1 pt2. f pt1 pt2 pt3) (Node z part3)) part1 part2)
   else if x = w ∧ z = w then
     Node w (merge_part2 (apply_pdt3 vs (λpt2 pt1 pt3. f pt1 pt2 pt3) (Node y part2)) part1 part3)
   else if y = w ∧ z = w then
     Node w (merge_part2 (apply_pdt3 vs (λpt1. f pt1) (Node x part1)) part2 part3)
   else if x = w then
     Node x (map_part (λexpl1. apply_pdt3 vs f expl1 (Node y part2) (Node z part3)) part1)
   else if y = w then
     Node y (map_part (λexpl2. apply_pdt3 vs f (Node x part1) expl2 (Node z part3)) part2)
   else if z = w then
     Node z (map_part (λexpl3. apply_pdt3 vs f (Node x part1) (Node y part2) expl3) part3)
   else
     apply_pdt3 vs f (Node x part1) (Node y part2) (Node z part3))"
| "apply_pdt3 [] _ _ _ _ = undefined"

fun "hide_pdt" :: "'n list ==> (('n, 'd) proof + ('d, ('n, 'd) proof) part ==> ('n, 'd) proof) ==> ('n, 'd) expl ==> ('n, 'd) expl" where
  "hide_pdt vs f (Leaf pt) = Leaf (f (Inl pt))"
| "hide_pdt [x] f (Node y part) = Leaf (f (Inr (map_part unleaf part)))"
| "hide_pdt (x # xs) f (Node y part) =
  (if x = y then
     Node y (map_part (hide_pdt xs f) part)
   else
     hide_pdt xs f (Node y part))"
| "hide_pdt [] _ _ = undefined"

context 
  fixes σ :: "('n, 'd :: {default, linorder}) trace" and
  cmp :: "('n, 'd) proof ==> ('n, 'd) proof ==> bool"
begin

function (sequential) eval :: "'n list ==> nat ==> ('n, 'd) Formula.formula ==> ('n, 'd) expl" where
  "eval vs i Formula.TT = Leaf (Inl (STT i))"
| "eval vs i Formula.FF = Leaf (Inr (VFF i))"
| "eval vs i (Eq_Const x c) = Node x (tabulate [c] (λc. Leaf (Inl (SEq_Const i x c))) (Leaf (Inr (VEq_Const i x c))))"
| "eval vs i (Formula.Pred r ts) =
  (pdt_of i r ts (filter (λx. x ∈ Formula.fv (Formula.Pred r ts)) vs) (List.map_filter (match ts) (sorted_list_of_set (snd ` {rd ∈ Γ σ i. fst rd = r}))))"
| "eval vs i (Formula.Neg φ) = apply_pdt1 vs (λp. min_list_wrt cmp (do_neg p)) (eval vs i φ)"
| "eval vs i (Formula.Or φ ψ) = apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_or p1 p2)) (eval vs i φ) (eval vs i ψ)"
| "eval vs i (Formula.And φ ψ) = apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_and p1 p2)) (eval vs i φ) (eval vs i ψ)"
| "eval vs i (Formula.Imp φ ψ) = apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_imp p1 p2)) (eval vs i φ) (eval vs i ψ)"
| "eval vs i (Formula.Iff φ ψ) = apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_iff p1 p2)) (eval vs i φ) (eval vs i ψ)"
| "eval vs i (Formula.Exists x φ) = hide_pdt (vs @ [x]) (λp. min_list_wrt cmp (do_exists x p)) (eval (vs @ [x]) i φ)"
| "eval vs i (Formula.Forall x φ) = hide_pdt (vs @ [x]) (λp. min_list_wrt cmp (do_forall x p)) (eval (vs @ [x]) i φ)"
| "eval vs i (Formula.Prev I φ) = (if i = 0 then Leaf (Inr VPrevZ)
                                   else apply_pdt1 vs (λp. min_list_wrt cmp (do_prev i I (Δ σ i) p)) (eval vs (i-1) φ))"
| "eval vs i (Formula.Next I φ) = apply_pdt1 vs (λl. min_list_wrt cmp (do_next i I (Δ σ (i+1)) l)) (eval vs (i+1) φ)"
| "eval vs i (Formula.Once I φ) =
  (if τ σ i < τ σ 0 + left I then Leaf (Inr (VOnceOut i))
   else (let expl = eval vs i φ in
        (if i = 0 then
           apply_pdt1 vs (λp. min_list_wrt cmp (do_once_base 0 0 p)) expl
         else (if right I ≥ enat (Δ σ i) then
                 apply_pdt2 vs (λp p'. min_list_wrt cmp (do_once i (left I) p p')) expl
                            (eval vs (i-1) (Formula.Once (subtract (Δ σ i) I) φ))
               else apply_pdt1 vs (λp. min_list_wrt cmp (do_once_base i (left I) p)) expl))))"
| "eval vs i (Formula.Historically I φ) =
  (if τ σ i < τ σ 0 + left I then Leaf (Inl (SHistoricallyOut i))
   else (let expl = eval vs i φ in
        (if i = 0 then
           apply_pdt1 vs (λp. min_list_wrt cmp (do_historically_base 0 0 p)) expl
         else (if right I ≥ enat (Δ σ i) then
                 apply_pdt2 vs (λp p'. min_list_wrt cmp (do_historically i (left I) p p')) expl
                            (eval vs (i-1) (Formula.Historically (subtract (Δ σ i) I) φ))
               else apply_pdt1 vs (λp. min_list_wrt cmp (do_historically_base i (left I) p)) expl))))"
| "eval vs i (Formula.Eventually I φ) =
  (let expl = eval vs i φ in
  (if right I = ∞ then undefined
   else (if right I ≥ enat (Δ σ (i+1)) then
           apply_pdt2 vs (λp p'. min_list_wrt cmp (do_eventually i (left I) p p')) expl
                            (eval vs (i+1) (Formula.Eventually (subtract (Δ σ (i+1)) I) φ))
         else apply_pdt1 vs (λp. min_list_wrt cmp (do_eventually_base i (left I) p)) expl)))"
| "eval vs i (Formula.Always I φ) =
  (let expl = eval vs i φ in
  (if right I = ∞ then undefined
   else (if right I ≥ enat (Δ σ (i+1)) then
           apply_pdt2 vs (λp p'. min_list_wrt cmp (do_always i (left I) p p')) expl
                            (eval vs (i+1) (Formula.Always (subtract (Δ σ (i+1)) I) φ))
         else apply_pdt1 vs (λp. min_list_wrt cmp (do_always_base i (left I) p)) expl)))"
| "eval vs i (Formula.Since φ I ψ) =
  (if τ σ i < τ σ 0 + left I then Leaf (Inr (VSinceOut i))
   else (let expl1 = eval vs i φ in
         let expl2 = eval vs i ψ in
         (if i = 0 then
            apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_since_base 0 0 p1 p2)) expl1 expl2
          else (if right I ≥ enat (Δ σ i) then
                  apply_pdt3 vs (λp1 p2 p'. min_list_wrt cmp (do_since i (left I) p1 p2 p')) expl1 expl2
                             (eval vs (i-1) (Formula.Since φ (subtract (Δ σ i) I) ψ))
                else apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_since_base i (left I) p1 p2)) expl1 expl2))))"
| "eval vs i (Formula.Until φ I ψ) =
  (let expl1 = eval vs i φ in
   let expl2 = eval vs i ψ in
   (if right I = ∞ then undefined
    else (if right I ≥ enat (Δ σ (i+1)) then
            apply_pdt3 vs (λp1 p2 p'. min_list_wrt cmp (do_until i (left I) p1 p2 p')) expl1 expl2
                             (eval vs (i+1) (Formula.Until φ (subtract (Δ σ (i+1)) I) ψ))
          else apply_pdt2 vs (λp1 p2. min_list_wrt cmp (do_until_base i (left I) p1 p2)) expl1 expl2)))"
| "eval vs i (Formula.MatchP I r) = undefined"
| "eval vs i (Formula.MatchF I r) = undefined"
  by pat_completeness auto

fun dist where
  "dist i (Formula.Once _ _) = i"
| "dist i (Formula.Historically _ _) = i"
| "dist i (Formula.Eventually I _) = LTP σ (case right I of ∞ ==> 0 | enat b ==> (τ σ i + b)) - i"
| "dist i (Formula.Always I _) = LTP σ (case right I of ∞ ==> 0 | enat b ==> (τ σ i + b)) - i"
| "dist i (Formula.Since _ _ _) = i"
| "dist i (Formula.Until _ I _) = LTP σ (case right I of ∞ ==> 0 | enat b ==> (τ σ i + b)) - i"
| "dist _ _ = undefined"

lemma i_less_LTP: "τ σ (Suc i) ≤ b + τ σ i ==> i < LTP σ (b + τ σ i)"
  by (metis Suc_le_lessD i_le_LTPi_add le_iff_add)

termination eval
  by (relation "measures [λ(_, _, φ). size φ, λ(_, i, φ). dist i φ]")
    (auto simp: add.commute le_diff_conv i_less_LTP intro!: diff_less_mono2)

end

end