theory SimpleTypedSet
imports FOL
begin

declare [[eta_contract = false]]

typedecl e
typedecl s

arities e :: "term"
arities s :: "term"

consts
  "empty" :: s ("{}")
  insert :: "[e, s]\<Rightarrow>s"
  "member" :: "[e, s]\<Rightarrow>o"
  "lesseq" :: "[s, s]\<Rightarrow>o" (infixl "<=" 50)
  Collect :: "[e\<Rightarrow>o]\<Rightarrow>s" 
  "Minus" :: "[s, s]\<Rightarrow>s" (infixl "-" 65)
  "Int" :: "[s, s]\<Rightarrow>s" (infixl "\<inter>" 70)
  "Un" :: "[s, s]\<Rightarrow>s" (infixl "\<union>" 65)
  Compl :: "s\<Rightarrow>s"

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 => s"    ("(1{_./ _})")
translations
  "{x. P}" == "CONST Collect (%x. P)"

hide_const (open) member

syntax
  "op ̃~:" :: "[e,s]\<Rightarrow>o" ("(_/ ~: _)" [50, 51] 50)
  "@Finset" :: "args \<Rightarrow> s" ("{(_)}")

translations
  "x~: y" == "\<not>(x : y)"
  "{x, xs}" == "CONST insert(x,{xs})"
  "{x}" == "CONST insert(x,{})"
  "{x. P}" == "CONST Collect(\<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 " :: "[s, s]\<Rightarrow>o" ("op <=")
  " _setle " :: "[s, s]\<Rightarrow>o" ("(_/ <= _)" [50, 51] 50)
  " _setless " :: "[s, s]\<Rightarrow>o" ("op <")
  " _setless " :: "[s, s]\<Rightarrow>o" ("(_/ < _)" [50, 51] 50)

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

translations
  "op \<subseteq>" == "op <= :: [s,s] \<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}"
  insert_def : "insert(a, B)\<equiv>{x. x=a} \<union> B"
  Compl_def: "Compl(A)\<equiv>{x.\<not>x\<in>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