Theory Divrg

Up to index of Isabelle/HOL/sHowe

Divrg =  Dyn +

consts

divrg :: "(uexp) set"

syntax 
"@divrg" :: "uexp => bool"


translations
"divrg e"  == "e : divrg"

coinductive divrg
intrs

div1 "[|cloexp e1; cloexp e2; divrg e1|] ==> divrg (e1 $ e2)"
div2 "[|e1 >> lam x. E x ; abstr E; cloexp e2; divrg (E e2)|] ==> divrg (e1 $ e2)"


constdefs

        omega :: uexp 
        "omega == (lam x . x $ x) $ (lam x . x $ x)"



end

theorem divrg_cloexp:

  divrg p ==> cloexp p

theorem omega_diverges:

  divrg omega

theorem divrg_Abs_E:

  divrg (bLam E) ==> P

theorem divrg_App_E:

  [| divrg (e $ e1);
     !!e1a e2. [| e = e1a & e1 = e2; cloexp e1a; cloexp e2; divrg e1a |] ==> P;
     !!E e1a e2.
        [| e = e1a & e1 = e2; e1a >> bLam E; abstr E; cloexp e2; divrg (E e2) |]
        ==> P |]
  ==> P

theorem converges_imp_not_divrg:

  converges s ==> s ~: divrg

theorem divrg_imp_not_converges:

  divrg s ==> ¬ converges s