Theory DEAKDerivedRules

theory DEAKDerivedRules
imports Main "calculus/src/isabelle/DEAK_SE" NatToString
begin

(* The Id rule where for every formula f, f ⇩S ⊢⇩S f ⇩S is derivable *)
lemma Id:
  fixes f :: Formula
  shows "loc ⊢d f ⇩S ⊢⇩S f ⇩S"
apply(induct f)
apply (rule_tac derivable.FboxA_R)
apply (rule_tac derivable.FboxA_L)
apply simp
apply (rule_tac derivable.FdiamA_L)
apply (rule_tac derivable.FdiamA_R)
apply simp
apply (rule_tac derivable.BboxA_R)
apply (rule_tac derivable.BboxA_L)
apply simp
apply (rule_tac derivable.BdiamA_L)
apply (rule_tac derivable.BdiamA_R)
apply simp
apply (rule_tac derivable.FboxK_R)
apply (rule_tac derivable.FboxK_L)
apply simp
apply (rule_tac derivable.FdiamK_L)
apply (rule_tac derivable.FdiamK_R)
apply simp
apply (rule_tac derivable.BboxK_R)
apply (rule_tac derivable.BboxK_L)
apply simp
apply (rule_tac derivable.BdiamK_L)
apply (rule_tac derivable.BdiamK_R)
apply simp
apply (rule_tac derivable.Id)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.And_R)
apply simp
apply simp
apply (rule_tac derivable.ImpL_R)
apply (rule_tac derivable.ImpL_L)
apply simp
apply simp
apply (rule_tac derivable.DImpL_L)
apply (rule_tac derivable.DImpL_R)
apply simp
apply simp
apply (rule_tac derivable.DImpR_L)
apply (rule_tac derivable.DImpR_R)
apply simp
apply simp
apply (rule_tac derivable.Or_R)
apply (rule_tac derivable.Or_L)
apply simp
apply simp
apply (rule_tac derivable.ImpR_R)
apply (rule_tac derivable.ImpR_L)
apply simp
apply simp
apply (rule_tac derivable.One_L)
apply (rule_tac derivable.One_R)
apply (rule_tac derivable.Top_L)
apply (rule_tac derivable.Top_R)
apply (rule_tac derivable.Bot_R)
apply (rule_tac derivable.Bot_L)
done

definition disj :: "Formula list ⇒ Formula" ("⋁⇩F _" 300) where
"disj list = foldr (Formula_Or) list ⊥⇩F"

lemma disj_unfold_1: "(⋁⇩F (x#list)) = x ∨⇩F (⋁⇩F list)" unfolding disj_def by simp

definition conj :: "Formula list ⇒ Formula" ("⋀⇩F _" 300) where
"conj list = foldr (Formula_And) list ⊤⇩F"

lemma conj_unfold_1: "(⋀⇩F (x#list)) = x ∧⇩F (⋀⇩F list)" unfolding conj_def by simp

lemma conj_unfold_1a: "(⋀⇩F (map f (x#list))) = (f x) ∧⇩F (⋀⇩F map f list)" unfolding conj_def by simp

lemma conj_unfold_2:
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d (⋀⇩F (list1@list2)) ⇩S ⊢⇩S ((⋀⇩F list1) ∧⇩F (⋀⇩F list2)) ⇩S"
apply (induct list1)
apply(subst conj_def)+
apply simp
apply (rule_tac derivable.C_L)
apply (rule_tac derivable.And_R)
apply (rule Id)
apply (rule_tac derivable.IW_L)
apply (rule_tac derivable.Top_R)
proof goal_cases
  case (1 a list1)
  have 2: "(a # list1) @ list2 = a # (list1 @ list2)" by simp
  show ?case unfolding 2
  apply(subst conj_unfold_1)
  apply(subst conj_unfold_1)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.And_R)

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule_tac f="(⋀⇩F list1) ∧⇩F (⋀⇩F list2)" in derivable.SingleCut)
  using cut apply simp
  using 1 apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule_tac Id)

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.And_R)

  apply (rule_tac f="(⋀⇩F list1) ∧⇩F (⋀⇩F list2)" in derivable.SingleCut)
  using cut apply simp
  using 1 apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  apply (rule_tac Id)

  by (rule_tac Id)
qed

lemma conj_unfold_2b:
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d ((⋀⇩F list1) ∧⇩F (⋀⇩F list2)) ⇩S ⊢⇩S (⋀⇩F (list1@list2)) ⇩S"
apply(induct list1)
apply(subst conj_def)+
apply simp
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac Id)
proof goal_cases
  case (1 a list1)
  have 2: "(a # list1) @ list2 = a # (list1 @ list2)" by simp
  show ?case unfolding 2
  apply(subst conj_unfold_1)
  apply(subst conj_unfold_1)

  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.And_R)

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)

  apply (rule_tac derivable.W_impL_L)
  apply (rule_tac derivable.Comma_impL_disp)

  apply (rule_tac f="(⋀⇩F list1) ∧⇩F (⋀⇩F list2)" in derivable.SingleCut)
  using cut apply simp
  apply (rule_tac derivable.And_R)
  apply (rule_tac Id)
  apply (rule_tac Id)

  using 1 apply simp

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)

  apply (rule_tac derivable.W_impR_R)
  by (rule_tac Id)
qed

lemma conj_fold:
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d (⋀⇩F map (λx. f x ∧⇩F f' x) l) ⇩S ⊢⇩S ((⋀⇩F map f l) ∧⇩F (⋀⇩F map f' l)) ⇩S"
apply(induct l)
apply simp
apply(subst conj_def)+
apply simp
apply (rule_tac derivable.Top_L)
apply (rule_tac derivable.C_L)
apply (rule_tac derivable.And_R)
apply (rule_tac derivable.Top_R)
apply (rule_tac derivable.Top_R)
apply(subst conj_unfold_1a)+

apply (rule_tac f="(f a ∧⇩F f' a) ∧⇩F ((⋀⇩F map f l) ∧⇩F (⋀⇩F map f' l))" in derivable.SingleCut)
using cut apply simp
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.And_R)
apply simp
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.And_R)
apply (rule_tac Id)
apply (rule_tac Id)

apply (rule_tac derivable.C_L)
apply (rule_tac derivable.And_R)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.And_R)
apply (rule_tac derivable.And_L)

apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac Id)

apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac Id)

apply (rule_tac derivable.And_L)
apply (rule_tac derivable.And_R)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac Id)

apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac Id)
done

lemma conj_impl_fold:
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d ((⋀⇩F map f list) ⇩S) ;⇩S ((⋀⇩F map (λy. f y →⇩F f' y) list) ⇩S) ⊢⇩S (⋀⇩F map f' list) ⇩S"
apply(induct list)
apply simp
apply(subst conj_def)+
apply simp
apply (rule_tac derivable.IW_L)
apply (rule_tac derivable.Top_R)

apply(subst conj_unfold_1a)+

apply (rule_tac derivable.C_L)
apply (rule_tac derivable.And_R)
defer
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac derivable.Comma_impL_disp)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac derivable.ImpR_L)
apply (rule_tac Id)
apply (rule_tac Id)

apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac derivable.Comma_impL_disp)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac derivable.Comma_impR_disp)
by simp

lemma conj_der1: "loc ⊢d ( f )⇩S ⊢⇩S X ⟹ f ∈ set list ⟹ loc ⊢d ( ⋀⇩F list )⇩S ⊢⇩S X"
apply(induct list)
proof (simp, goal_cases)
  case (1 a list)
  thus ?case
  apply(cases "f ∈ set list")
  apply simp
  apply (subst conj_unfold_1)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply simp
  proof goal_cases
    case 1 
    then have "f = a" by simp
    thus ?case
    apply (subst conj_unfold_1)
    apply (rule_tac derivable.And_L)
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac derivable.W_impR_R)
    using 1 Id by simp
  qed
qed

lemma conj_der1b: " ∀f ∈ set list. loc ⊢d X  ⊢⇩S ( f )⇩S ⟹ loc ⊢d X ⊢⇩S ( ⋀⇩F list )⇩S"
apply(induct list)
apply simp 
using IW_L Top_R conj_def apply simp
proof (simp, goal_cases)
  case (1 a list)
  show ?case
  apply(subst conj_unfold_1)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.And_R)
  defer
  using 1 apply simp
  using 1 using IW_L Top_R conj_def by fastforce
qed

lemma conj_der2_aux: 
  fixes l'
  shows "⋀ l. set l' ⊆ set l ⟹ loc ⊢d ( ⋀⇩F l )⇩S ⊢⇩S ( ⋀⇩F l' )⇩S"
apply(induct l')
apply(subst (2) conj_def)
apply simp
apply (rule_tac derivable.IW_L)
apply (rule_tac derivable.Top_R)
proof (simp, goal_cases)
  case (1 a l' l)
  then have "loc ⊢d (⋀⇩F l) ⇩S ⊢⇩S (⋀⇩F l') ⇩S" by simp
  thus ?case
  apply (rule_tac derivable.C_L)
  apply (subst conj_unfold_1)
  apply (rule_tac derivable.And_R)
  apply simp
  apply(rule_tac f=a in conj_der1)
  apply (rule Id)
  using 1 by simp
qed

lemma conj_der2: 
  fixes l'
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  and "loc ⊢d ( ⋀⇩F l' )⇩S ⊢⇩S X"
  shows "⋀ l. set l' ⊆ set l ⟹ loc ⊢d ( ⋀⇩F l )⇩S ⊢⇩S X"
using assms(2) proof (induct l')
case Nil 
  have 1: "(⋀⇩F []) = ⊤⇩F" unfolding conj_def by simp
  with Nil have "loc ⊢d ⊤⇩F ⇩S ⊢⇩S X" by simp
  then have "loc ⊢d I⇩S ⊢⇩S X"
  apply (rule_tac f="⊤⇩F" in derivable.SingleCut)
  using cut apply simp
  apply (rule_tac derivable.Top_R)
  by simp
  thus ?case
  apply (rule_tac derivable.IW_L)
  by simp
next
case (Cons x xs)
  show ?case
  apply (rule_tac f="(⋀⇩F (x#xs))" in derivable.SingleCut)
  using cut apply simp
  using conj_der2_aux cut Cons.prems(1) apply blast
  using Cons by simp
qed

lemma conj_der2b: 
  fixes l'
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  and "loc ⊢d X ⊢⇩S ( ⋀⇩F l )⇩S"
  shows "⋀ l'. set l' ⊆ set l ⟹ loc ⊢d X ⊢⇩S ( ⋀⇩F l' )⇩S"
using assms(2) 
apply (induct l)
apply simp

apply (rule_tac f="(⋀⇩F a # l)" in derivable.SingleCut)
  using cut apply simp
apply simp
using conj_der2_aux cut apply blast
done

lemma conj_box_distrib : 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d ( ⋀⇩F map (Formula_FboxK (nat_to_string i)) l )⇩S ⊢⇩S fboxK⇩F (nat_to_string i) ( ⋀⇩F l )⇩S" 
proof (induct l)
case Nil
  have 1: "map (Formula_FboxK (nat_to_string i)) [] = []" by simp
  have 2: "foldr op ∧⇩F [] ⊤⇩F = ⊤⇩F" by simp
  thus ?case
  unfolding conj_def
  unfolding 1 2
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.Back_forw_K2)
  apply (rule_tac derivable.IW_L)
  by (rule_tac derivable.Top_R)
next
case (Cons x xs)
  have 1: "map (Formula_FboxK (nat_to_string i)) (x # xs) = (fboxK⇩F nat_to_string i x) # (map (Formula_FboxK (nat_to_string i)) xs)" by simp
  show ?case
  apply (subst conj_unfold_1)
  unfolding 1
  apply (subst conj_unfold_1)
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Back_forw_K2)
  apply (rule_tac derivable.K_mon_L)
  apply (rule_tac derivable.And_R)

  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac f="fboxK⇩F nat_to_string i (⋀⇩F xs)" in derivable.SingleCut)
  using cut apply simp
  using Cons apply simp
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac Id)

  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac derivable.FboxK_L)
  by (rule_tac Id)
qed

lemma conj_All: 
 shows "(⋀x. x ∈ set List ⟹ (loc ⊢d X ⊢⇩S (x ⇩S))) ⟹ loc ⊢d X ⊢⇩S (⋀⇩F List)⇩S"
apply (induct List arbitrary:X)
apply (subst conj_def)
apply simp 
apply (rule_tac derivable.IW_L)
apply (rule_tac derivable.Top_R)
apply (subst conj_unfold_1)
apply (rule_tac derivable.C_L)
apply (rule_tac derivable.And_R)
by simp+

lemma conj_FboxK_distrib : 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d (⋀⇩F (map (Formula_FboxK aa) list))⇩S ⊢⇩S (fboxK⇩F aa (⋀⇩F list))⇩S"
apply (induct list)
apply (subst conj_def)+
apply simp
apply (rule_tac derivable.FboxK_R)
apply (rule_tac derivable.Back_forw_K2)
apply (rule_tac derivable.IW_L)
apply (rule_tac derivable.Top_R)
proof -
case goal1 
  have conj_unfold_map: "(⋀⇩F map (Formula_FboxK aa) (a # list)) = (fboxK⇩F aa a) ∧⇩F (⋀⇩F (map (Formula_FboxK aa) list))" using conj_unfold_1 by auto
  show ?case
  apply(subst conj_unfold_1)
  apply(subst conj_unfold_map)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.Back_forw_K2)
  apply (rule_tac derivable.K_mon_L)
  apply (rule_tac derivable.And_R)
  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac f="fboxK⇩F aa (⋀⇩F list)" in derivable.SingleCut)
  using cut goal1 apply simp+
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac Id)
  by (simp add: Back_forw_K FboxK_L Id)
qed

lemma disj_lub : 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d ( ⋀⇩F map (λB. B →⇩F A) list )⇩S ⊢⇩S ((⋁⇩F list)⇩S) →⇩S (A ⇩S)" 
apply(induct list)
apply(subst conj_def)
apply(subst disj_def)
apply simp
apply (rule_tac derivable.W_impR_R)
apply (rule_tac derivable.IW_R)
apply (rule_tac derivable.Bot_L)
apply(subst conj_unfold_1a)
apply(subst disj_unfold_1)

apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.E_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.C_R)
apply (rule_tac derivable.Or_L)

apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.W_impL_L)
apply (rule_tac derivable.Comma_impL_disp)
apply (rule_tac derivable.E_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply simp

apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.Comma_impL_disp2)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac derivable.Comma_impL_disp)
apply (rule_tac derivable.E_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.ImpR_L)
apply (rule_tac Id)

apply (rule_tac Id)
done

fun k_apply :: "('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a" ("_ ⇧_ _") where 
"k_apply Fun 0 f = f" |
"k_apply Fun (Suc x) f = Fun (k_apply Fun x f)"

lemma k_apply_unfold_bis: "k_apply Fun (Suc k) f = k_apply Fun k (Fun f) "
apply(induction k)
unfolding k_apply.simps by simp+

lemma k_apply_S_Formula_FboxA_Structure_ForwA:
  fixes loc 
  shows "loc ⊢d (k_apply (Formula_FboxA a) k form)⇩S ⊢⇩S k_apply (Structure_ForwA a) k (form ⇩S) "
apply(induction k)
apply simp
apply (rule Id)
unfolding k_apply.simps
apply (rule_tac derivable.FboxA_L)
by simp

lemma k_apply_S_display_1:
  fixes loc 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d X ⊢⇩S (k_apply (Formula_FboxA a) k form)⇩S ⟷ loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k (form ⇩S) "
apply rule
apply(induction k arbitrary: X)
apply simp
unfolding k_apply.simps
apply (rule_tac f="fboxA⇩F a Formula_FboxA a ⇧k form" in derivable.SingleCut)
using cut apply simp
apply simp
using k_apply_S_Formula_FboxA_Structure_ForwA
apply (simp add: k_apply_S_Formula_FboxA_Structure_ForwA FboxA_L)

apply (induct k arbitrary: X)
apply simp
unfolding k_apply.simps
proof -
case goal1
  have assms: "loc ⊢d backA⇩S a X ⊢⇩S Structure_ForwA a ⇧k form ⇩S" by (simp add: Back_forw_A goal1(1) goal1(2))
  thus ?case
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac derivable.Back_forw_A2)
  by (simp add: goal1(1))
qed

lemma k_apply_S_display_1a:
  fixes loc 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d X ⊢⇩S (k_apply (Formula_FboxA a) k form)⇩S ⟹ loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k (form ⇩S) "
using k_apply_S_display_1 using cut by blast

lemma k_apply_S_display_1b:
  fixes loc 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k (form ⇩S) ⟹ loc ⊢d X ⊢⇩S (k_apply (Formula_FboxA a) k form)⇩S"
using k_apply_S_display_1 using cut by blast

lemma k_apply_S_display_1diam:
  fixes loc 
  shows "loc ⊢d (Structure_ForwA a) ⇧k (form ⇩S) ⊢⇩S X ⟹ loc ⊢d ((Formula_FdiamA a) ⇧k form)⇩S ⊢⇩S X"
apply(induct k arbitrary:X)
unfolding k_apply.simps
apply simp
proof -
case goal1
  then have "loc ⊢d Structure_ForwA a ⇧k form ⇩S ⊢⇩S backA⇩S a X"
  apply (rule_tac derivable.Forw_back_A)
  by simp
 
  with goal1 have "loc ⊢d Formula_FdiamA a ⇧k form ⇩S ⊢⇩S backA⇩S a X" by simp
  thus ?case
  apply (rule_tac derivable.FdiamA_L)
  apply (rule_tac derivable.Forw_back_A2)
  by simp
qed

lemma k_apply_S_F_forw_diam:
  fixes loc
  shows "loc ⊢d  X ⇩S ⊢⇩S Y ⇩S ⟹ loc ⊢d Structure_ForwA a ⇧k X ⇩S ⊢⇩S Formula_FdiamA a ⇧k Y ⇩S"
apply(induct k arbitrary:X Y)
apply simp
apply simp
apply (rule_tac derivable.FdiamA_R)
by simp

lemma k_apply_S_display_2:
  fixes loc 
  shows "loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k Y ⟷ loc ⊢d k_apply (Structure_BackA a) k X ⊢⇩S Y"
apply rule
apply (induct k arbitrary: X)
apply simp
apply (metis Back_forw_A k_apply.simps(2) k_apply_unfold_bis)
apply (induct k arbitrary: X)
apply simp
by (metis Back_forw_A2 k_apply.simps(2) k_apply_unfold_bis)

lemma k_apply_S_display_2a:
  fixes loc 
  shows "loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k Y ⟹ loc ⊢d k_apply (Structure_BackA a) k X ⊢⇩S Y"
by (simp add: k_apply_S_display_2)

lemma k_apply_S_display_2b:
  fixes loc 
  shows "loc ⊢d k_apply (Structure_BackA a) k X ⊢⇩S Y ⟹ loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k Y"
by (simp add: k_apply_S_display_2)

lemma k_apply_S_display_2back:
  fixes loc 
  shows "loc ⊢d k_apply (Structure_BackA a) k X ⊢⇩S Y ⟷ loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k Y"
apply rule
apply (induct k arbitrary: X)
apply simp
using k_apply_S_display_2 apply blast
apply (induct k arbitrary: X)
apply simp
using k_apply_S_display_2 by blast

lemma k_apply_elim_diamA:
  fixes loc 
  shows "loc ⊢d forma ⇩S ⊢⇩S formb ⇩S ⟹ loc ⊢d (k_apply (Formula_FdiamA a) k forma)⇩S ⊢⇩S (k_apply (Formula_FdiamA a) k formb)⇩S "
apply (induct k)
apply simp
using FdiamA_L FdiamA_R by auto

lemma k_apply_DiamBot: 
  fixes loc
  shows "loc ⊢d ( k_apply ( Formula_FdiamA A ) k ⊥⇩F ) ⇩S ⊢⇩S I⇩S "
apply (induct k)
unfolding k_apply.simps
apply (rule_tac derivable.Bot_L)
apply (rule_tac derivable.FdiamA_L)
apply (rule_tac derivable.Forw_back_A2)
apply (rule_tac derivable.A_nec_R)
by simp

lemma k_apply_DiamBot_Is: 
  fixes loc
  shows "loc ⊢d ( k_apply ( Formula_FdiamA A ) k ⊥⇩F ) ⇩S ⊢⇩S I⇩S"
apply (induct k)
unfolding k_apply.simps
apply (rule_tac derivable.Bot_L)
apply (rule_tac derivable.FdiamA_L)
apply (rule_tac derivable.Forw_back_A2)
apply (rule_tac derivable.A_nec_R)
by simp

lemma k_apply_BoxDiam: 
  fixes loc
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d ( k_apply ( Formula_FboxA A ) k p ) ∧⇩F ( k_apply ( Formula_FdiamA A ) k q) ⇩S ⊢⇩S ( k_apply ( Formula_FdiamA A ) k ( p∧⇩Fq ) ) ⇩S "
apply (induct k)
apply simp
apply (rule Id)

apply (subst k_apply.simps)+
apply (rule_tac f="Formula_FdiamA A ( ((Formula_FboxA A) ⇧k p )∧⇩F ((Formula_FdiamA A) ⇧k q))" in derivable.SingleCut)
using cut apply simp
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.FdiamA_L)
apply (rule_tac derivable.Forw_back_A2)
apply (rule_tac derivable.A_FS_R)
apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.Forw_back_A)
apply (rule_tac derivable.FdiamA_R)
apply (rule_tac derivable.And_R)
defer
apply (rule_tac derivable.Back_forw_A)
apply (rule_tac derivable.FboxA_L)
apply (rule Id)
defer
apply (rule Id)

apply (rule_tac derivable.FdiamA_L)
apply (rule_tac derivable.FdiamA_R)
by simp

lemma k_apply_S_FS:
  fixes loc 
  shows "loc ⊢d X ⊢⇩S (k_apply (Structure_ForwA a) k Y) →⇩S (k_apply (Structure_ForwA a) k Z) ⟹ loc ⊢d X ⊢⇩S k_apply (Structure_ForwA a) k (Y →⇩S Z)"
apply(induct k arbitrary: X Y Z)
apply simp
apply simp
using Back_forw_A Back_forw_A2 FS_A_R by blast

lemma k_apply_S_Atom:
  fixes loc 
  assumes cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d X ⇩F ⇩S ⊢⇩S forwA⇩S b (k_apply (Structure_ForwA a) k (X ⇩F ⇩S))"
apply (rule_tac f="fboxA⇩F b (X ⇩F)" in derivable.SingleCut)
using cut apply blast
apply (rule_tac derivable.FboxA_R)
apply (rule_tac derivable.Atom)
apply simp

apply (rule_tac derivable.FboxA_L)
apply(induct k arbitrary: X a b)
apply simp
apply (rule_tac Atom)
apply simp+
apply (rule_tac derivable.Back_forw_A2)
apply (rule_tac f="X ⇩F" in derivable.SingleCut)
using cut apply simp
apply (rule_tac Atom)
by simp+

lemma k_apply_F_FboxA:
  fixes loc 
  shows "loc ⊢d X ⇩S ⊢⇩S (Formula_FboxA a X) ⇩S ⟹ loc ⊢d (k_apply (Formula_FboxA a) k X) ⇩S ⊢⇩S (k_apply (Formula_FboxA a) (Suc k) X) ⇩S"
apply(induct k)
unfolding k_apply.simps
apply simp
apply (rule_tac derivable.FboxA_R)
apply (rule_tac derivable.FboxA_L)
by simp

lemma Swapout_R_1:
  fixes loc
  assumes "RelAKA rel ∈ set loc" and "rel alpha a = [beta]"
  shows "loc ⊢d Y ⊢⇩S forwK⇩S a forwA⇩S beta X ⟹ loc ⊢d ;;⇩S [Y] ⊢⇩S forwA⇩S alpha forwK⇩S a X"
apply (rule derivable.Swapout_R)
using assms by auto

lemma Bot_imp_all: "loc ⊢d ⊥⇩F ⇩S ⊢⇩S X"
apply (rule_tac derivable.IW_R)
apply (rule_tac derivable.Bot_L)
done

lemma Swapout_R_2aux:
  fixes loc
  assumes refl_rel: "RelAKA rel ∈ set loc" and "rel alpha a = [alpha]"
  shows "loc ⊢d Y  ⊢⇩S  (Structure_ForwA alpha) ⇧k (forwK⇩S a forwA⇩S alpha X)  ⟹ loc ⊢d Y ⊢⇩S Structure_ForwA alpha ⇧(Suc k) (forwK⇩S a X)"
apply(induct k arbitrary: X Y)
apply simp
apply (rule_tac derivable.I_impR2)
apply (rule_tac derivable.Bigcomma_Nil_L)
apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.Bigcomma_Cons_L)
apply (rule_tac rel=rel and beta=alpha in Swapout_R_1)
using assms apply (simp,simp, simp)

apply(rule_tac k_apply_S_display_2b)
apply(subst k_apply.simps)
apply (rule_tac derivable.Back_forw_A)
apply (rule_tac derivable.I_impR2)
apply (rule_tac derivable.Bigcomma_Nil_L)
apply (rule_tac derivable.Comma_impR_disp)
apply (rule_tac derivable.Bigcomma_Cons_L)
apply (rule_tac rel=rel and beta=alpha in Swapout_R_1)
using assms apply (simp,simp)
apply(rule_tac k_apply_S_display_2a)
by simp

lemma Swapout_R_2:
  fixes loc
  assumes refl_rel: "RelAKA rel ∈ set loc" and "rel alpha a = [alpha]"
  and cut: "⋀f. CutFormula f ∈ set loc"
  shows "loc ⊢d (fboxK⇩F a (Formula_FboxA alpha ⇧k X))⇩S  ⊢⇩S Structure_ForwA alpha ⇧k (forwK⇩S a X ⇩S)"
apply(induct k arbitrary: X)
apply(subst k_apply.simps)+
apply (rule_tac FboxK_L)
apply (rule_tac Id)
proof - 
case goal1 
  have cut_f: "loc ⊢d Formula_FboxA alpha ⇧k fboxK⇩F a fboxA⇩F alpha X ⇩S ⊢⇩S Structure_ForwA alpha ⇧k forwK⇩S a forwA⇩S alpha X ⇩S"
  apply (induct k)
  apply(subst k_apply.simps)+
  apply (rule_tac FboxK_L)
  apply (rule_tac FboxA_L)
  apply (rule_tac Id)
  apply(subst k_apply.simps)+
  apply (rule_tac FboxA_L)
  by simp
  
  have subst1: "fboxA⇩F alpha Formula_FboxA alpha ⇧k X = Formula_FboxA alpha ⇧k fboxA⇩F alpha X" by (metis k_apply.simps(2) k_apply_unfold_bis)
  show ?case
  apply(subst k_apply.simps)
  
  apply (rule_tac Swapout_R_2aux)
  using assms apply (simp,simp)
  apply(subst subst1)
  apply(rule_tac f="Formula_FboxA alpha ⇧k fboxK⇩F a fboxA⇩F alpha X" in derivable.SingleCut)
  using cut apply simp
  defer
  using cut_f apply simp
  apply(rule_tac k_apply_S_display_1b)
  using cut apply simp
  using goal1 FboxK_R k_apply_S_display_2back by blast
qed
end