(*--"\<^bold>C\<^bold>O\<^bold>U\<^bold>N\<^bold>T\<^bold>E\<^bold>R\<^bold>X (cTest)"*)

theory cTest
imports Complex_Main
begin

typedecl sT

consts inP :: "sT => sT => bool" (infixl "\<in>\<^isub>\<iota>" 55)

abbreviation niP :: "sT => sT => bool" (infixl "\<notin>\<^isub>\<iota>"  55) where
  "niP p q == \<not>(p \<in>\<^isub>\<iota> q)"

axiomatization where
  Ax_x\<^isup>N: "(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> x \<in>\<^isub>\<iota> s) \<longleftrightarrow> r = s"

consts emS :: "sT" ("\<emptyset>")

axiomatization where
  Ax_emS: "(x \<notin>\<^isub>\<iota> \<emptyset>)"
  
consts paS :: "sT => sT => sT"

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
  translations
  "\<lbrace>r,s\<rbrace>" == "CONST paS r s"
  
axiomatization  where
  Ax_paS: "x \<in>\<^isub>\<iota> \<lbrace>r,s\<rbrace> \<longleftrightarrow> (x = r \<or> x = s)"

theorem paS_is_unique:
  "(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> (x = p \<or> x = q)) \<longleftrightarrow> r = \<lbrace>p,q\<rbrace>"
  by(metis Ax_x\<^isup>N Ax_paS)
  
definition siS :: "sT => sT" where
  "siS r = paS r r"
  notation
  siS  ("(\<lbrace>(_)\<rbrace>)")
  
theorem siS_is_unique:
  "(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> x = s) \<longleftrightarrow> r = \<lbrace>s\<rbrace>"
  by(metis
    siS_def
    paS_is_unique)
  
consts seS :: "sT => (sT => bool) => sT"

syntax
  "_seS" :: "sT => (sT => bool) => sT" ("(\<lbrace>(_./ _)\<rbrace>)")
  translations
  "\<lbrace>q. P\<rbrace>" == "CONST seS q P"

axiomatization where
  Ax_seS: "\<forall>q::sT. \<forall>P::(sT => bool). x \<in>\<^isub>\<iota> \<lbrace>q. P\<rbrace> \<longleftrightarrow> (x \<in>\<^isub>\<iota> q \<and> P x)"

function PT :: "sT => bool" where
  "PT x = (x \<notin>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>)"
  by(auto)
  
theorem PT_formula :
  "PT x = (x \<notin>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>)"
  sorry  

theorem
  "\<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<in>\<^isub>\<iota> \<lbrace> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<rbrace>  \<and> PT \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<longrightarrow> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<in>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>"
  by(metis 
    Ax_seS 
    siS_is_unique 
    PT_formula)
--"Metis: The assumptions are inconsistent"

(*
For phi(x) = x \<notin>\<^isub>\<iota> u, state the following axiom per the normal axiom scheme,
as if it let u occur in phi(x):
      \<forall>q.\<exists>u.\<forall>x. (x \<in>\<^isub>\<iota> q \<and> x \<notin>\<^isub>\<iota> u) \<longleftrightarrow> x \<in>\<^isub>\<iota> u.
Now, let q = \<lbrace>\<emptyset>\<rbrace> and u = \<emptyset>. So
      (\<emptyset> \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> \<emptyset> \<notin>\<^isub>\<iota> \<emptyset>) \<longrightarrow> \<emptyset> \<in>\<^isub>\<iota> \<emptyset>.
ISAR:
axiomatization where
  PT_axiom: 
  "\<forall>q.\<exists>u.\<forall>x. (x \<in>\<^isub>\<iota> q \<and> x \<notin>\<^isub>\<iota> u) \<longleftrightarrow> x \<in>\<^isub>\<iota> u"
theorem 
  "(\<emptyset> \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> \<emptyset> \<notin>\<^isub>\<iota> \<emptyset>) \<longrightarrow> \<emptyset> \<in>\<^isub>\<iota> \<emptyset>" 
  by(metis (full_types) PT_axiom)
theorem 
  "(a \<in>\<^isub>\<iota> \<lbrace>a\<rbrace> \<and> a \<notin>\<^isub>\<iota> a) \<longrightarrow> a \<in>\<^isub>\<iota> a" 
  by(metis (full_types) PT_axiom)
*)  

(*
function consist_test_1 :: "sT => bool" where
  "consist_test_1 x = (x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1))"
  by(auto)
  
theorem consist_test_1_formula :
  "consist_test_1 x = (x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1))"
  sorry
  
theorem consist_test_1_iff:
  "\<forall>x. x \<in>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1) \<longleftrightarrow> (x \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> consist_test_1 x)"
  apply simp
  by(metis 
    Ax_seS 
    consist_test_1_formula)
  
theorem
  "\<forall>x. ~(x \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> consist_test_1 x)"
  apply(simp)
  by(metis 
    Ax_seS 
    consist_test_1_formula)
  
theorem
  "\<forall>x. x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1)"
  by(metis 
    Ax_seS 
    consist_test_1_formula)
*)

end
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"