Theory Closed

Up to index of Isabelle/HOL/sHowe

(*
Closed and open terms

*)


Closed = UnLam +

consts



iwff :: "((var list)  * uexp) set"



syntax 


"@iwff"  :: "var list => uexp => bool"   ("((_) |--/ (_))" [50,50] 50)



translations



"l |--  e"  == "(l,e) : iwff "



constdefs

  wff :: (var list) => uexp => bool   ("((_) |-/ (_))" [50,50] 50)
 " env |- t == isexp t & (!n. newFor  n t | n mem env)"

  cloexp ::  uexp  => bool
  "cloexp p ==  isexp p &  Expr.closed p"

  open ::  uexp  => bool
  "open p ==  isexp  p &  ~ Expr.closed p"

 udflt :: uexp
"udflt == (lam x. x)" 


   cloAbstr ::  (uexp => uexp) => bool

  "cloAbstr E ==  abstr E &  cloexp (lam x. E x)"

rules

wff_iwff "(env |- s) = (env |-- s)"
sub_biSub  "[| abstr N; y  # env1 |- N (VAR y)|]  ==>   biSubst N n a (VAR y) =  N (VAR y) "

inductive iwff
intrs

  clo_VAR " (n mem env) ==> env |--  (VAR n)" 
clo_App "[| env |--  e1; env |--  e2|] ==> env |--  (e1 $ e2)"
clo_Abs "[|abstr E; !n. (n # env) |--  (E (VAR n))|] ==> env |--  (lam x .  E x)"


end

theorem cloexp_isexp:

  cloexp t ==> isexp t

theorem cloexp_App:

  [| cloexp s; cloexp t |] ==> cloexp (s $ t)

theorem clo_sub:

  [| cloAbstr E; cloexp p |] ==> cloexp (E p)

theorem cloexp_udflt:

  cloexp (lam x. x)

theorem wff_to_iwff:

  l |- e ==> l |-- e

theorem iwff_to_wff:

  l |-- e ==> l |- e

theorem wff_Nil_cloexp:

  ([] |- s) = cloexp s

theorem wff_Nil_cloexp1:

  [] |- s ==> cloexp s

theorem wff_Nil_cloexp2:

  cloexp s ==> [] |- s

theorem iwff_Nil_cloexp2:

  cloexp s ==> [] |-- s

theorem iwff_Nil_cloexp1:

  [] |-- s ==> cloexp s

theorem wff_isexp:

  env |- s ==> isexp s

theorem wff_weak:

  list |- s ==> a # list |- s

theorem wff_closed_subst:

  [| a # list |- s; cloexp p |] ==> list |- subst s a p

theorem subst_App:

  [| isexp s; isexp t |] ==> subst (s $ t) n = (%x. subst s n x $ subst t n x)

theorem subst_App1:

  [| isexp s; isexp t |] ==> subst (s $ t) n p = subst s n p $ subst t n p

theorem subst_lam:

  abstr e ==> subst (lam y. e y) n = (%x. lam y. biSubst e n x y)

theorem cloexp_subst_id:

  cloexp s ==> subst s n p = s