Theory Negation_Type

section‹Negation Type›
theory Negation_Type
imports Main
begin

text‹Store some @{typ 'a} and remember symbolically whether you mean just @{term a} or @{term "¬ a"}.›

text‹Only negated or non-negated literals›
datatype 'a negation_type = Pos 'a | Neg 'a

fun getPos :: "'a negation_type list ⇒ 'a list" where
  "getPos [] = []" |
  "getPos ((Pos x)#xs) = x#(getPos xs)" |
  "getPos (_#xs) = getPos xs"

fun getNeg :: "'a negation_type list ⇒ 'a list" where
  "getNeg [] = []" |
  "getNeg ((Neg x)#xs) = x#(getNeg xs)" |
  "getNeg (_#xs) = getNeg xs"


lemma getPos_append: "getPos (as@bs) = getPos as @ getPos bs"
  by(induct as rule: getPos.induct) simp+

lemma getNeg_append: "getNeg (as@bs) = getNeg as @ getNeg bs"
  by(induct as rule: getNeg.induct) simp+

text‹If there is @{typ "'a negation_type"}, then apply a @{term map} only to @{typ 'a}.
I.e. keep @{term Neg} and @{term Pos}›
fun NegPos_map :: "('a ⇒ 'b) ⇒ 'a negation_type list ⇒ 'b negation_type list" where
  "NegPos_map _ [] = []" |
  "NegPos_map f ((Pos a)#as) = (Pos (f a))#NegPos_map f as" |
  "NegPos_map f ((Neg a)#as) = (Neg (f a))#NegPos_map f as"

text‹Example›
lemma "NegPos_map (λx::nat. x+1) [Pos 0, Neg 1] = [Pos 1, Neg 2]" by eval

lemma getPos_NegPos_map_simp: "(getPos (NegPos_map X (map Pos src))) = map X src"
  by(induction src) (simp_all)
lemma getNeg_NegPos_map_simp: "(getNeg (NegPos_map X (map Neg src))) = map X src"
  by(induction src) (simp_all)
lemma getNeg_Pos_empty: "(getNeg (NegPos_map X (map Pos src))) = []"
  by(induction src) (simp_all)
lemma getNeg_Neg_empty: "(getPos (NegPos_map X (map Neg src))) = []"
  by(induction src) (simp_all)
lemma getPos_NegPos_map_simp2: "(getPos (NegPos_map X src)) = map X (getPos src)"
  by(induction src rule: getPos.induct) (simp_all)
lemma getNeg_NegPos_map_simp2: "(getNeg (NegPos_map X src)) = map X (getNeg src)"
  by(induction src rule: getPos.induct) (simp_all)
lemma getPos_id: "getPos (map Pos xs) = xs"
  by(induction xs) (simp_all)
lemma getNeg_id: "getNeg (map Neg xs) = xs"
  by(induction xs) (simp_all)
lemma getPos_empty2: "(getPos (map Neg src)) = []"
  by(induction src) (simp_all)
lemma getNeg_empty2: "(getNeg (map Pos src)) = []"
  by(induction src) (simp_all)

lemmas NegPos_map_simps = getPos_NegPos_map_simp getNeg_NegPos_map_simp getNeg_Pos_empty getNeg_Neg_empty getPos_NegPos_map_simp2 
                          getNeg_NegPos_map_simp2 getPos_id getNeg_id getPos_empty2 getNeg_empty2
                          
lemma NegPos_map_map_Neg: "NegPos_map C (map Neg as) = map Neg (map C as)"
  by(induction as) (simp_all)
lemma NegPos_map_map_Pos: "NegPos_map C (map Pos as) = map Pos (map C as)"
  by(induction as) (simp_all)

lemma NegPos_map_append: "NegPos_map C (as @ bs) = NegPos_map C as @ NegPos_map C bs"
  by(induction as rule: getNeg.induct) (simp_all)

lemma getPos_set: "Pos a ∈ set x ⟷ a ∈ set (getPos x)"
 apply(induction x rule: getPos.induct)
 apply(auto)
 done
lemma getNeg_set: "Neg a ∈ set x ⟷ a ∈ set (getNeg x)"
 apply(induction x rule: getPos.induct)
 apply(auto)
 done
lemma getPosgetNeg_subset: "set x ⊆ set x' ⟷  set (getPos x) ⊆ set (getPos x') ∧ set (getNeg x) ⊆ set (getNeg x')"
  apply(induction x rule: getPos.induct)
  apply(simp)
  apply(simp add: getPos_set)
  apply(rule iffI)
  apply(simp_all add: getPos_set getNeg_set)
done
lemma set_Pos_getPos_subset: "Pos ` set (getPos x) ⊆ set x"
 apply(induction x rule: getPos.induct)
 apply(simp_all)
 apply blast+
done
lemma set_Neg_getNeg_subset: "Neg ` set (getNeg x) ⊆ set x"
 apply(induction x rule: getNeg.induct)
 apply(simp_all)
 apply blast+
done
lemmas NegPos_set = getPos_set getNeg_set getPosgetNeg_subset set_Pos_getPos_subset set_Neg_getNeg_subset
hide_fact getPos_set getNeg_set getPosgetNeg_subset set_Pos_getPos_subset set_Neg_getNeg_subset


lemma negation_type_forall_split: "(∀is∈set Ms. case is of Pos i ⇒ P i | Neg i ⇒ Q i) ⟷ (∀i∈set (getPos Ms). P i) ∧ (∀i∈set (getNeg Ms). Q i)"
  apply(rule)
   apply(simp split: negation_type.split_asm)
   using NegPos_set(1) NegPos_set(2) apply force
  apply(simp split: negation_type.split)
  using NegPos_set(1) NegPos_set(2) by fastforce

fun invert :: "'a negation_type ⇒ 'a negation_type" where
  "invert (Pos x) = Neg x" |
  "invert (Neg x) = Pos x"

lemma invert_invert_id: "invert ∘ invert = id"
  apply(clarsimp simp add: fun_eq_iff, rename_tac x, case_tac x)
   by simp+

end