datatype form = VAR "num"
  | FALSE
  | DISJ "form" "form"
  | NOT "form"
  | DIAM "form"

record 'a frame =
  world :: "'a ⇒ bool"
  rel :: "'a ⇒ 'a ⇒ bool"


record 'a model = "'a frame" +
  valt :: "num ⇒ 'a ⇒ bool"

fun satis :: "'a model ⇒ 'a ⇒ form ⇒ bool"
where
"satis M w (VAR p) ⟷ (valt M p w ∧ world M w)"
| "satis M w FALSE ⟷ False"
| "satis M w (NOT f) ⟷ world M w ∧ ¬ satis M w f"
| "satis M w (DISJ f1 f2) ⟷ satis M w f1 ∨ satis M w f2"
| "satis M w (DIAM f) ⟷ world M w ∧ (∃ v. rel M w v ∧ world M v ∧ satis M v f)"


lemma satis_in_worlds: "satis M w f ⟹ world M w"
proof (induct rule:form.induct)
  case (DISJ x1a x2)
 then show ?case by auto (* not sure if this works, but auto is roughly simp + blast *)
next
  case (DIAM x)
  then show ?case
  by fastforce
qed simp_all

definition BOX_def : "BOX f = NOT (DIAM (NOT f))"

definition AND_def : "AND f1 f2 = NOT (DISJ (NOT f1) (NOT f2))"

definition TRUE_def : "TRUE = NOT FALSE"

fun subst :: "(num ⇒ form) ⇒ form ⇒ form"
  where
   "subst s FALSE = FALSE"
  | "subst s (VAR p) = s p"
  | "subst s (DISJ f1 f2) = DISJ (subst s f1) (subst s f2)"
  | "subst s (NOT f) = NOT (subst s f)"
  | "subst s (DIAM f) = DIAM (subst s f)"

lemma subst_BOX[simp] : "subst f (BOX form) = BOX (subst f form)"
  by (simp add: BOX_def)

lemma satis_AND : "satis M w (AND f1 f2) ⟷ satis M w f1 ∧ satis M w f2"
proof -
  show ?thesis apply (simp add: AND_def)
    by (meson satis_in_worlds)
qed

definition satis_set_def :
"satis_set M w Σ ≡ (⋀a. a ∈ Σ ⟹ satis M w a)"

(*

val demodalize_def = Define`
demodalize FALSE = FALSE /\
demodalize (VAR p) = VAR p /\
demodalize (DISJ form1 form2) = DISJ (demodalize form1) (demodalize form2) /\
demodalize (NOT form) = NOT (demodalize form) /\
demodalize (DIAM form) = demodalize form`;

*)

fun demodalize :: "form ⇒ form"
  where
    "demodalize FALSE = FALSE"
  | "demodalize (VAR p) = VAR p"
  | "demodalize (DISJ form1 form2) = DISJ (demodalize form1) (demodalize form2)"
  | "demodalize (NOT form) = NOT (demodalize form)"
  | "demodalize (DIAM form) = demodalize form"

thm HOL.eq_reflection

fun propform :: "form ⇒ bool"
  where
   "propform FALSE = True"
 | "propform (VAR p) = True"
 | "propform (DISJ f1 f2) = (propform f1 ∧ propform f2)"
 | "propform (NOT f) = propform f"
 | "propform (DIAM f) = False"

definition IMP_def : "IMP f1 f2 = DISJ (NOT f1) f2"

fun peval :: "(num ⇒ bool) ⇒ form ⇒ bool" where
   "peval σ (VAR p) = σ p"
 | "peval σ (DISJ f1 f2) = (peval σ f1 ∨ peval σ f2)"
 | "peval σ FALSE = False"
 | "peval σ (NOT f) = (¬ peval σ f)"
 | "peval σ (DIAM f) = False"

definition ptaut_def : "ptaut f ⟷ propform f ∧ (∀σ. peval σ f)"

inductive Kproof :: "form list ⇒ bool" where
   "Kproof []"
 | "Kproof p ∧ List.member p (IMP f1 f2) ∧ List.member p f1 ⟹ Kproof (p @ [f2])"
 | "Kproof p ∧ List.member p f ⟹ Kproof (p @ [subst σ f])"
 | "Kproof p ∧ List.member p f ⟹ Kproof (p @ [BOX f])"
 | "Kproof p ⟹ Kproof (p @ [IMP (BOX (IMP form1 form2)) (IMP (BOX form1) (BOX form2))])"
 | "Kproof p ⟹  Kproof (p @ [IMP (DIAM form) (NOT (BOX (NOT form)))])"
 | "Kproof p ∧ ptaut f ⟹ Kproof (p @ [f])"




value "demodalize (IMP (BOX (IMP form1 form2)) (IMP (BOX form1) (BOX form2)))"

lemma demodalize_IMP : "demodalize (IMP f1 f2) = IMP (demodalize f1) (demodalize f2)"
proof -
  show ?thesis
  by (simp add: IMP_def)
qed

lemma ptaut_MP : assumes a1 : "ptaut (IMP f1 f2)" and a2: "ptaut f1" shows b: "ptaut f2"
proof -
  show ?thesis using a1 a2 by (simp add: IMP_def ptaut_def)
qed

find_theorems "List.member (a @ [b])"




definition valid_frame_state_def:
"valid_frame_state Fr w phi ≡ (⋀M. frame.truncate M = Fr ⟹ satis M w phi)"


lemma propform_demodalize : "propform (demodalize f)"
  sorry

lemma demodalize_subst: "demodalize (subst f form) = demodalize (subst f (demodalize form))"
  sorry

lemma peval_demodalize_subst_eq:
    "propform form ⟹
     (peval σ (demodalize (subst f form))
    ≡ peval (peval σ o demodalize o f) form)"
proof (induct rule:form.induct) qed simp_all

(*
lemma peval_demodalize_subst_eq :
 " propform form ⟹
  (peval σ (demodalize (subst f form)) \<equiv> peval (peval σ o demodalize o f) form)"
  sorry*)
thm disjE

lemma demodalize_BOX : "demodalize (BOX form) = NOT (NOT (demodalize form))"
  by (simp add: BOX_def)

lemma peval_not_not: "peval σ (NOT (NOT f)) = peval σ f"
  by simp

lemma ptaut_not_not: "ptaut f ⟹ ptaut (NOT (NOT f))"
  by (simp add: ptaut_def)


lemma demodalize_ax1_ptaut : "ptaut (demodalize (IMP (BOX (IMP form1 form2)) (IMP (BOX form1) (BOX form2))))"
proof -
  show ?thesis unfolding ptaut_def apply (simp add: propform_demodalize)
    by (simp add: IMP_def demodalize_BOX)
qed

lemma demodalize_ax2_ptaut : "ptaut (demodalize (IMP (DIAM form) (NOT (BOX (NOT form)))))"
proof -
  show ?thesis unfolding ptaut_def apply (simp add: propform_demodalize)
  by (simp add: IMP_def demodalize_BOX)
qed

lemma demodalize_ax3_ptaut : "ptaut (demodalize (IMP (NOT (BOX (NOT form))) (DIAM form)))"
proof -
  show ?thesis unfolding ptaut_def apply (simp add: propform_demodalize)
  by (simp add: IMP_def demodalize_BOX)
qed



lemma exercise_1_6_2 : "Kproof p ⟹ List.member p f ⟹ ptaut (demodalize f)"
proof (induction arbitrary: f rule: Kproof.induct)
  case 1
  then show ?case
  using member_rec(2) by force
next
  case a:(2 p f1 f2)
  hence a1 : "List.member p f ∨ f = f2"
    by (metis in_set_member rotate1.simps(2) set_ConsD set_rotate1)
  then
  show ?case
    by (metis a.IH demodalize_IMP ptaut_MP)
next
  case a : (3 p f σ g)
  hence a1 : "List.member p g ∨ g = subst σ f"
   by (metis member_def rotate1.simps(2) set_ConsD set_rotate1)
  show ?case apply (rule disjE [OF "a1"]) sorry

next
  case c4: (4 p f0 f)
  hence a2: "List.member p f ∨ f = BOX f0"
  by (metis in_set_member rotate1.simps(2) set_ConsD set_rotate1)
  show ?case apply (rule disjE[OF "a2"])
  proof -
    assume dj1: "List.member p f" show ?case using c4 dj1 by simp
  next
    assume dj2: "f = BOX f0"
    have "ptaut (demodalize f0)" using c4 dj2 by blast
    then show ?case using dj2
      by (simp add: demodalize_BOX ptaut_not_not)
  qed
next
  case (5 p form1 form2)
  then show ?case sorry
next
  case (6 p form)
  then show ?case sorry
next
  case (7 p f)
  then show ?case sorry
qed

  case (5 p form1 form2)
  then show ?case
    using demodalize_ax1_ptaut by (force simp: List.member_def)

  case (5 p form1 form2)
  then consider
    (f_IMP) "f = IMP (BOX (IMP form1 form2))
        (IMP (BOX form1) (BOX form2))" |
    (pf) "List.member p f"
    by (auto simp: List.member_def)
  then show ?case
  proof cases
    case pf
    then show ?thesis using 5 by auto
  next
    case f_IMP
    then show ?thesis
      using demodalize_ax1_ptaut by force
  qed