theory sTs__sFOLdt
imports Complex_Main
begin

typedecl sT

consts inS :: "sT => sT => bool"

datatype sFOLdt =
  In sT sT
| Eq sT sT
| Forall sT sFOLdt 

type_synonym env = "(sT => sT)"

definition sID :: "sT => sT" where
  "sID s = s"
  
fun sFOLf :: "env => sFOLdt => bool" where
  "sFOLf E (In x y) = inS x y"

value "sFOLf sID (In x y)"

fun sFOLf1 :: "env => sFOLdt => bool" where
  "sFOLf1 E (In x y) = inS x y"
| "sFOLf1 E (Eq x y) = (E x = E y)"

value "sFOLf1 sID (In x y)"

fun sFOLf2 :: "env => sFOLdt => bool" where
  "sFOLf2 E (In x y) = inS x y"
| "sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"

value "sFOLf2 sID (In x y)"

end