theory NSet
imports IFOL
begin

declare [[eta_contract = false]]

typedecl i

type_synonym set = i

arities i :: "term"

consts
  "zero" :: i ("0")
  "one" :: i ("1")
  "empty" :: set ("{}")
  insert :: "[i, set]\<Rightarrow>set"
  "member" :: "[i, set]\<Rightarrow>o"
  "lesseq" :: "[set, set]\<Rightarrow>o" (infixl "<=" 50)
  Collect :: "[i\<Rightarrow>o]\<Rightarrow>set" 
  INTER :: "[set, i\<Rightarrow>set]\<Rightarrow>set"
  UNION :: "[set, i\<Rightarrow>set]\<Rightarrow>set"
  "Minus" :: "[set, set]\<Rightarrow>set" (infixl "-" 65)
  "Int" :: "[set, set]\<Rightarrow>set" (infixl "\<inter>" 70)
  "Un" :: "[set, set]\<Rightarrow>set" (infixl "\<union>" 65)
  Compl :: "set\<Rightarrow>set"
  Pow :: "set\<Rightarrow>set"
  UNIV :: set
  Ball :: "[set, i\<Rightarrow>o]\<Rightarrow>o"
  Bex :: "[set, i\<Rightarrow>o]\<Rightarrow>o"

notation
  member ("op :") and
  member ("(_/ : _)" [51,51] 50)

notation (xsymbols)
  member      ("op \<in>") and
  member      ("(_/ \<in> _)" [51, 51] 50)

notation (HTML output)
  member      ("op \<in>") and
  member      ("(_/ \<in> _)" [51, 51] 50)

syntax
  "_Coll" :: "pttrn => o => set"    ("(1{_./ _})")
translations
  "{x. P}" == "CONST Collect (%x. P)"

hide_const (open) member

syntax
  "_Ball"       :: "pttrn => set => o => o"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
  "_Bex"        :: "pttrn => set => o => o"      ("(3EX _:_./ _)" [0, 0, 10] 10)

syntax (HOL)
  "_Ball"       :: "pttrn => set => o => o"      ("(3! _:_./ _)" [0, 0, 10] 10)
  "_Bex"        :: "pttrn => set => o => o"      ("(3? _:_./ _)" [0, 0, 10] 10)

syntax (xsymbols)
  "_Ball"       :: "pttrn => set => o => o"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
  "_Bex"        :: "pttrn => set => o => o"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)

syntax (HTML output)
  "_Ball"       :: "pttrn => set => o => o"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
  "_Bex"        :: "pttrn => set => o => o"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)

translations
  "ALL x:A. P" == "CONST Ball(A (%x. P))"
  "EX x:A. P" == "CONST Bex(A (%x. P))"

syntax
  "op ̃~:" :: "[i,set]\<Rightarrow>o" ("(_/ ~: _)" [50, 51] 50)
(*  "@Collect" :: "[pttrn, o]\<Rightarrow>set" ("(1{_./ _})") *)
  "@Finset" :: "args \<Rightarrow> set" ("{(_)}")
(*  "op Int" :: "[set, set]\<Rightarrow>set" (infixl "\<inter>" 70)
  "op Un" :: "[set, set]\<Rightarrow>set" (infixl "\<union>" 65)*)
  "@INTER" :: "[pttrn, set, set]\<Rightarrow>set" ("(3INT _:_./ _)" 10)
  "@UNION" :: "[pttrn, set, set]\<Rightarrow>set" ("(3UN _:_./ _)" 10)
  "_Ball" :: "pttrn \<Rightarrow> set \<Rightarrow> o \<Rightarrow>o" ("(3ALL _:_./ _)" [0, 0, 10] 10)
  "_Bex" :: "[pttrn, set, o]\<Rightarrow>o" ("(3EX _:_./ _)" [0, 0, 10] 10)

translations
  "NSet.UNIV" == "NSet.Compl({})"
  "x~: y" == "\<not>(x : y)"
  "{x, xs}" == "NSet.insert(x,{xs})"
  "{x}" == "NSet.insert(x,{})"
  "{x. P}" == "NSet.Collect(\<lambda>x. P)"
  "INT x:A. B" == "NSet.INTER(A, (\<lambda>x. B))"
  "UN x:A. B" == "NSet.UNION(A, (\<lambda>x. B))"
  "ALL x:A. P" == "CONST NSet.Ball(A, (\<lambda>x. P))"
  "EX x:A. P" == "CONST NSet.Bex(A, (\<lambda>x. P))"

axiomatization where
  ext: "A = B\<longleftrightarrow>(\<forall>x. ((x:A)\<longleftrightarrow>(x:B)))" and
  Collect: "(t :{x. P(x)})\<longleftrightarrow>(P(t))"

syntax ("" output)
  " _setle " :: "[set, set]\<Rightarrow>o" ("op <=")
  " _setle " :: "[set, set]\<Rightarrow>o" ("(_/ <= _)" [50, 51] 50)
  " _setless " :: "[set, set]\<Rightarrow>o" ("op <")
  " _setless " :: "[set, set]\<Rightarrow>o" ("(_/ < _)" [50, 51] 50)

syntax (xsymbols)
  " _setle " :: "[set, set]\<Rightarrow>o" ("op \<subseteq>")
  " _setle " :: "[set, set]\<Rightarrow>o" ("(_/ \<subseteq> _)" [50, 51] 50)
  " _setless " :: "[set, set]\<Rightarrow>o" ("op \<subset>")
  " _setless " :: "[set, set]\<Rightarrow>o" ("(_/ \<subset> _)" [50, 51] 50)
  "op ̃~:" :: "['a, set]\<Rightarrow>o" ("op \<notin>")
  "op ̃~:" :: "['a, set]\<Rightarrow>o" ("(_/ \<notin> _)" [50, 51] 50)

translations
  "op \<subseteq>" == "op <= :: [set,set] \<Rightarrow>o"

defs
  subset_def: "A <= B\<equiv>\<forall>x. x\<in>A\<longrightarrow>x\<in>B"
  empty_def: "{} \<equiv>{x. False}"
  Minus_def: "A - B\<equiv>{x. x\<in>A\<and>x\<notin>B}"
  Un_def: "A \<union> B\<equiv>{x. x\<in>A\<or>x\<in>B}"
  Int_def : "A \<inter> B\<equiv>{x. x\<in>A\<and>x\<in>B}"
  Ball_def: "Ball(A, P)\<equiv>(\<forall>x. x\<in>A\<longrightarrow>P(x))"
  Bex_def: "Bex(A, P)\<equiv>(\<exists>x. x\<in>A\<and>P(x))"
  Compl_def: "Compl(A)\<equiv>{x.\<not>x\<in>A}"
  INTER_def: "INTER(A, B)\<equiv>{y. ALL x:A. y\<in>B(x)}"
  UNION_def: "UNION(A, B)\<equiv> {y. EX x:A. y\<in>B(x)}"
  insert_def : "insert(a, B)\<equiv>{x. x=a} \<union> B"
  Pow_def: "Pow(A)\<equiv>{B. B<= A}"

lemma inI: "(P(t)) \<Longrightarrow>(t\<in>{x. P(x)})"
proof (rule iffD2)
  show "t \<in> {x. P(x)} \<longleftrightarrow> P(t)" by (rule Collect)
qed

lemma "inE2": "(t\<in>{x. P(x)}) \<Longrightarrow> P(t)"
proof (rule iffD1)
  show "t \<in> {x. P(x)} \<longleftrightarrow> P(t)" by (rule Collect)
qed

lemma inE: 
assumes p1: "(t\<in>{x. P(x)})" 
assumes p2: "P(t) \<Longrightarrow> R"
shows "R"
proof (rule p2)
  from p1 show "P(t)" by (rule inE2)
qed

lemma equalsI: "(\<forall> x. x\<in>A\<longleftrightarrow>x\<in>B) \<Longrightarrow> A = B"
proof (rule iffD2)
  show "A=B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)" by (rule ext)
qed

lemma equalsE2: "A = B \<Longrightarrow> (\<forall> x. x\<in>A\<longleftrightarrow>x\<in>B)"
proof (rule iffD1)
  show "A=B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)" by (rule ext)
qed

lemma equalsE: 
assumes p1: "A = B" 
assumes p2: "(\<forall> x. x\<in>A\<longleftrightarrow>x\<in>B) \<Longrightarrow> R" 
shows "R"
proof (rule p2)
  from p1 show "\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B" by (rule equalsE2)
qed

end