Theory MLSSmf_Defs

theory MLSSmf_Defs
  imports Main
begin

section ‹Syntax of MLSSmf›

datatype (vars_term: 'v, funs_term: 'f) MLSSmf_term =
  Empty nat (‹∅m _›) | is_Var: Varm 'v |
  Union "('v, 'f) MLSSmf_term" "('v, 'f) MLSSmf_term" (infix ‹⊔m› 64) |
  Inter "('v, 'f) MLSSmf_term" "('v, 'f) MLSSmf_term" (infix ‹⊓m› 65) |
  Diff "('v, 'f) MLSSmf_term" "('v, 'f) MLSSmf_term" (infix ‹-m› 66) |
  Singlem "('v, 'f) MLSSmf_term" |
  App 'f "('v, 'f) MLSSmf_term"

fun var_list_term :: "('v, 'f) MLSSmf_term ⇒ 'v list" where
  "var_list_term (∅m _) = []"
| "var_list_term (Varm x) = [x]"
| "var_list_term (t1 ⊔m t2) = var_list_term t1 @ var_list_term t2"
| "var_list_term (t1 ⊓m t2) = var_list_term t1 @ var_list_term t2"
| "var_list_term (t1 -m t2) = var_list_term t1 @ var_list_term t2"
| "var_list_term (Singlem t) = var_list_term t"
| "var_list_term (App f t) = var_list_term t"
lemma set_var_list_term[simp]: "set (var_list_term t) = vars_term t"
  by (induction t) auto

fun fun_list_term :: "('v, 'f) MLSSmf_term ⇒ 'f list" where
  "fun_list_term (App f t) = f # fun_list_term t"
| "fun_list_term (t1 ⊔m t2) = fun_list_term t1 @ fun_list_term t2"
| "fun_list_term (t1 ⊓m t2) = fun_list_term t1 @ fun_list_term t2"
| "fun_list_term (t1 -m t2) = fun_list_term t1 @ fun_list_term t2"
| "fun_list_term (Singlem t) = fun_list_term t"
| "fun_list_term _ = []"
lemma set_fun_list_term[simp]: "set (fun_list_term t) = funs_term t"
  by (induction t) auto

datatype (vars_atom: 'v, funs_atom: 'f) MLSSmf_atom =
  Elem "('v, 'f) MLSSmf_term" "('v, 'f) MLSSmf_term" (infix ‹∈m› 61) |
  Equal "('v, 'f) MLSSmf_term" "('v, 'f) MLSSmf_term" (infix ‹=m› 60) |
  Inc 'f (‹inc'(_')› [60] 60) |
  Dec 'f (‹dec'(_')› [60] 60) |
  Additive 'f (‹add'(_')› [60] 60) |
  Multiplicative 'f (‹mul'(_')› [60] 60) |
  LeqF 'f 'f (infix ‹≼m› 66)

fun var_list_atom :: "('v, 'f) MLSSmf_atom ⇒ 'v list" where
  "var_list_atom (t1 ∈m t2) = var_list_term t1 @ var_list_term t2"
| "var_list_atom (t1 =m t2) = var_list_term t1 @ var_list_term t2"
| "var_list_atom _ = []"
lemma set_var_list_atom[simp]: "set (var_list_atom a) = vars_atom a"
  by (cases a) auto

fun fun_list_atom :: "('v, 'f) MLSSmf_atom ⇒ 'f list" where
  "fun_list_atom (t1 ∈m t2) = fun_list_term t1 @ fun_list_term t2"
| "fun_list_atom (t1 =m t2) = fun_list_term t1 @ fun_list_term t2"
| "fun_list_atom (inc(f)) = [f]"
| "fun_list_atom (dec(f)) = [f]"
| "fun_list_atom (add(f)) = [f]"
| "fun_list_atom (mul(f)) = [f]"
| "fun_list_atom (f ≼m g) = [f, g]"
lemma set_fun_list_atom[simp]: "set (fun_list_atom a) = funs_atom a"
  by (cases a) auto

datatype (vars_literal: 'v, funs_literal: 'f) MLSSmf_literal =
  ATm "('v, 'f) MLSSmf_atom" |
  AFm "('v, 'f) MLSSmf_atom" (* negation of atom *)

fun var_list_literal :: "('v, 'f) MLSSmf_literal ⇒ 'v list" where
  "var_list_literal (ATm a) = var_list_atom a"
| "var_list_literal (AFm a) = var_list_atom a"
lemma set_var_list_literal[simp]: "set (var_list_literal lt) = vars_literal lt"
  by (cases lt) auto

fun fun_list_literal :: "('v, 'f) MLSSmf_literal ⇒ 'f list" where
  "fun_list_literal (ATm a) = fun_list_atom a"
| "fun_list_literal (AFm a) = fun_list_atom a"
lemma set_fun_list_literal[simp]: "set (fun_list_literal lt) = funs_literal lt"
  by (cases lt) auto

type_synonym ('v, 'f) MLSSmf_clause = "('v, 'f) MLSSmf_literal list" (* conjunction of literals *)

fun vars_in_clause :: "('v, 'f) MLSSmf_clause ⇒ 'v set" where
  "vars_in_clause cl = ⋃(set (map vars_literal cl))"

fun funs_in_clause :: "('v, 'f) MLSSmf_clause ⇒ 'f set" where
  "funs_in_clause cl = ⋃(set (map funs_literal cl))"

fun var_list_clause :: "('v, 'f) MLSSmf_clause ⇒ 'v list" where
  "var_list_clause ls = remdups (concat (map var_list_literal ls))"
lemma set_var_list_clause[simp]: "set (var_list_clause ls) = vars_in_clause ls"
  by (induction ls) auto

fun fun_list_clause :: "('v, 'f) MLSSmf_clause ⇒ 'f list" where
  "fun_list_clause ls = remdups (concat (map fun_list_literal ls))"
lemma set_fun_list_clause[simp]: "set (fun_list_clause ls) = funs_in_clause ls"
  by (induction ls) auto

section ‹Definition of "normalized"›

fun is_empty_or_var :: "('v, 'f) MLSSmf_term ⇒ bool" where
  "is_empty_or_var (∅m _) = True" |
  "is_empty_or_var (Varm _) = True" |
  "is_empty_or_var _ = False"

inductive norm_literal :: "('v, 'f) MLSSmf_literal ⇒ bool" where
     inc: "norm_literal (ATm (inc(f)))" |
     dec: "norm_literal (ATm (dec(f)))" |
     add: "norm_literal (ATm (add(f)))" |
     mul: "norm_literal (ATm (mul(f)))" |
      le: "norm_literal (ATm (f ≼m g))" |
      eq: "norm_literal (ATm (Varm x =m Varm y))" |
eq_empty: "norm_literal (ATm (Varm x =m ∅m n))" |
     neq: "norm_literal (AFm (Varm x =m Varm y))" |
   union: "norm_literal (ATm (Varm x =m Varm y ⊔m Varm z))" |
    diff: "norm_literal (ATm (Varm x =m Varm y -m Varm z))" |  
  single: "norm_literal (ATm (Varm x =m Singlem (Varm y)))" |
     app: "norm_literal (ATm (Varm x =m App f (Varm y)))"

lemma norm_literal_neq:
  assumes "norm_literal lt"
      and "lt = AFm a"
    shows "∃x y. a = Varm x =m Varm y"
  using assms by (cases lt rule: norm_literal.cases) auto

fun non_func_terms_in_norm_literal :: "('v, 'f) MLSSmf_literal ⇒ ('v, 'f) MLSSmf_term set" where
  "non_func_terms_in_norm_literal (ATm (x =m y ⊔m z)) = {x, y, z}" |
  "non_func_terms_in_norm_literal (ATm (x =m y -m z)) = {x, y, z}" |
  "non_func_terms_in_norm_literal (ATm (x =m Singlem y)) = {x, y}" |
  "non_func_terms_in_norm_literal (ATm (x =m App f y)) = {x, y}" |
  "non_func_terms_in_norm_literal (ATm (x =m y)) =
   (if is_empty_or_var x then {x} else {}) ∪ (if is_empty_or_var y then {y} else {})" |
  "non_func_terms_in_norm_literal (AFm (x =m y)) =
   (if is_empty_or_var x then {x} else {}) ∪ (if is_empty_or_var y then {y} else {})" |
  "non_func_terms_in_norm_literal _ = {}"

lemma non_func_terms_in_norm_literal_is_empty_or_var:
  "norm_literal lt ⟹ t ∈ non_func_terms_in_norm_literal lt ⟹ is_empty_or_var t"
  by (cases lt rule: norm_literal.cases) auto

inductive norm_clause :: "('v, 'f) MLSSmf_clause ⇒ bool" where
  "norm_clause []" |
  "norm_clause ls ⟹ norm_literal l ⟹ norm_clause (l # ls)"

inductive_cases normE[elim]: "norm_clause (l # ls)"

lemma literal_in_norm_clause_is_norm[intro]:
  assumes "norm_clause 𝒞" 
      and "l ∈ set 𝒞"
    shows "norm_literal l"
  using assms
  by (induction 𝒞) auto

section ‹Functions for collecting variables and functions›

consts varsm :: "'a ⇒ 'b set"
adhoc_overloading
  varsm ⇌ vars_term and
  varsm ⇌ vars_atom and
  varsm ⇌ vars_literal and
  varsm ⇌ vars_in_clause

consts funsm :: "'a ⇒ 'b set"
adhoc_overloading
  funsm ⇌ funs_term and
  funsm ⇌ funs_atom and
  funsm ⇌ funs_literal and
  funsm ⇌ funs_in_clause


lemma vars_in_lt_in_cl[intro]:
  "x ∈ varsm lt ⟹ lt ∈ set 𝒞 ⟹ x ∈ varsm 𝒞"
  by (induction 𝒞) auto

lemma vars_term_finite[intro]: "finite (varsm (t::('v, 'f) MLSSmf_term))"
  by (induction t) auto

lemma vars_atom_finite[intro]: "finite (varsm (a::('v, 'f) MLSSmf_atom))"
  by (induction a) auto

lemma vars_literal_finite[intro]: "finite (varsm (lt::('v, 'f) MLSSmf_literal))"
  by (cases lt) auto

lemma vars_finite[intro]: "finite (varsm (𝒞::('v, 'f) MLSSmf_clause))"
proof (induction 𝒞)
  case Nil
  then show ?case by simp
next
  case (Cons a 𝒞)
  moreover
  have "finite (varsm a)" by blast
  moreover
  have "varsm (a # 𝒞) = (varsm a) ∪ ⋃(set (map vars_literal 𝒞))"
    by auto
  ultimately
  show ?case by force
qed

lemma funs_in_lt_in_cl[intro]:
  "x ∈ funsm lt ⟹ lt ∈ set 𝒞 ⟹ x ∈ funsm 𝒞"
  by (induction 𝒞) auto

lemma funs_term_finite[intro]: "finite (funsm (t::('v, 'f) MLSSmf_term))"
  by (induction t) auto

lemma funs_atom_finite[intro]: "finite (funsm (a::('v, 'f) MLSSmf_atom))"
  by (induction a) auto

lemma funs_literal_finite[intro]: "finite (funsm (lt::('v, 'f) MLSSmf_literal))"
  by (cases lt) auto

lemma funs_finite[intro]: "finite (funsm (𝒞::('v, 'f) MLSSmf_clause))"
proof (induction 𝒞)
  case Nil
  then show ?case by simp
next
  case (Cons a 𝒞)
  moreover
  have "finite (funsm a)" by blast
  moreover
  have "funsm (a # 𝒞) = (funsm a) ∪ ⋃(set (map funs_literal 𝒞))"
    by auto
  ultimately
  show ?case by force
qed

end