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]\s"
"member" :: "[e, s]\o"
"lesseq" :: "[s, s]\o" (infixl "<=" 50)
Collect :: "[e\o]\s"
"Minus" :: "[s, s]\s" (infixl "-" 65)
"Int" :: "[s, s]\s" (infixl "\" 70)
"Un" :: "[s, s]\s" (infixl "\" 65)
Compl :: "s\s"
notation
member ("op :") and
member ("(_/ : _)" [51,51] 50)
notation (xsymbols)
member ("op \") and
member ("(_/ \ _)" [51, 51] 50)
notation (HTML output)
member ("op \") and
member ("(_/ \ _)" [51, 51] 50)
syntax
"_Coll" :: "pttrn => o => s" ("(1{_./ _})")
translations
"{x. P}" == "CONST Collect (%x. P)"
hide_const (open) member
syntax
"op ̃~:" :: "[e,s]\o" ("(_/ ~: _)" [50, 51] 50)
"@Finset" :: "args \ s" ("{(_)}")
translations
"x~: y" == "\(x : y)"
"{x, xs}" == "CONST insert(x,{xs})"
"{x}" == "CONST insert(x,{})"
"{x. P}" == "CONST Collect(\x. P)"
axiomatization where
ext: "A = B\(\x. ((x:A)\(x:B)))" and
Collect: "(t :{x. P(x)})\(P(t))"
syntax ("" output)
" _setle " :: "[s, s]\o" ("op <=")
" _setle " :: "[s, s]\o" ("(_/ <= _)" [50, 51] 50)
" _setless " :: "[s, s]\o" ("op <")
" _setless " :: "[s, s]\o" ("(_/ < _)" [50, 51] 50)
syntax (xsymbols)
" _setle " :: "[s, s]\o" ("op \")
" _setle " :: "[s, s]\o" ("(_/ \ _)" [50, 51] 50)
" _setless " :: "[s, s]\o" ("op \")
" _setless " :: "[s, s]\o" ("(_/ \ _)" [50, 51] 50)
"op ̃~:" :: "['a, s]\o" ("op \")
"op ̃~:" :: "['a, s]\o" ("(_/ \ _)" [50, 51] 50)
translations
"op \" == "op <= :: [s,s] \o"
defs
subset_def: "A <= B\\x. x\A\x\B"
empty_def: "{} \{x. False}"
Minus_def: "A - B\{x. x\A\x\B}"
Un_def: "A \ B\{x. x\A\x\B}"
Int_def : "A \ B\{x. x\A\x\B}"
insert_def : "insert(a, B)\{x. x=a} \ B"
Compl_def: "Compl(A)\{x.\x\A}"
lemma inI: "(P(t)) \(t\{x. P(x)})"
proof (rule iffD2)
show "t \ {x. P(x)} \ P(t)" by (rule Collect)
qed
lemma "inE2": "(t\{x. P(x)}) \ P(t)"
proof (rule iffD1)
show "t \ {x. P(x)} \ P(t)" by (rule Collect)
qed
lemma inE:
assumes p1: "(t\{x. P(x)})"
assumes p2: "P(t) \ R"
shows "R"
proof (rule p2)
from p1 show "P(t)" by (rule inE2)
qed
lemma equalsI: "(\ x. x\A\x\B) \ A = B"
proof (rule iffD2)
show "A=B \ (\x. x \ A \ x \ B)" by (rule ext)
qed
lemma equalsE2: "A = B \ (\ x. x\A\x\B)"
proof (rule iffD1)
show "A=B \ (\x. x \ A \ x \ B)" by (rule ext)
qed
lemma equalsE:
assumes p1: "A = B"
assumes p2: "(\ x. x\A\x\B) \ R"
shows "R"
proof (rule p2)
from p1 show "\x. x \ A \ x \ B" by (rule equalsE2)
qed
end