Theory Environment_Functor

theory Environment_Functor imports
  Applicative_Lifting.Applicative_Environment
begin

subsection ‹The environment functor›

type_synonym ('i, 'a) envir = "'i ⇒ 'a"

lemma const_apply [simp]: "const x i = x"
by(simp add: const_def)

context includes applicative_syntax begin

lemma ap_envir_apply [simp]: "(f ⋄ x) i = f i (x i)"
by(simp add: apf_def)

definition all_envir :: "('i, bool) envir ⇒ bool"
where "all_envir p ⟷ (∀x. p x)"

lemma all_envirI [Pure.intro!, intro!]: "(⋀x. p x) ⟹ all_envir p"
by(simp add: all_envir_def)

lemma all_envirE [Pure.elim 2, elim]: "all_envir p ⟹ (p x ⟹ thesis) ⟹ thesis"
by(simp add: all_envir_def)

lemma all_envirD: "all_envir p ⟹ p x"
by(simp add: all_envir_def)


definition pred_envir :: "('a ⇒ bool) ⇒ ('i, 'a) envir ⇒ bool"
where "pred_envir p f = all_envir (const p ⋄ f)"

lemma pred_envir_conv: "pred_envir p f ⟷ (∀x. p (f x))"
by(auto simp add: pred_envir_def)

lemma pred_envirI [Pure.intro!, intro!]: "(⋀x. p (f x)) ⟹ pred_envir p f"
by(auto simp add: pred_envir_def)

lemma pred_envirD: "pred_envir p f ⟹ p (f x)"
by(auto simp add: pred_envir_def)

lemma pred_envirE [Pure.elim 2, elim]: "pred_envir p f ⟹ (p (f x) ⟹ thesis) ⟹ thesis"
by(simp add: pred_envir_conv)

lemma pred_envir_mono: "⟦ pred_envir p f; ⋀x. p (f x) ⟹ q (g x) ⟧ ⟹ pred_envir q g"
by blast

definition rel_envir :: "('a ⇒ 'b ⇒ bool) ⇒ ('i, 'a) envir ⇒ ('i, 'b) envir ⇒ bool"
where "rel_envir p f g ⟷ all_envir (const p ⋄ f ⋄ g)"

lemma rel_envir_conv: "rel_envir p f g ⟷ (∀x. p (f x) (g x))"
by(auto simp add: rel_envir_def)

lemma rel_envir_conv_rel_fun: "rel_envir = rel_fun (=)"
by(simp add: rel_envir_conv rel_fun_def fun_eq_iff)

lemma rel_envirI [Pure.intro!, intro!]: "(⋀x. p (f x) (g x)) ⟹ rel_envir p f g"
by(auto simp add: rel_envir_def)

lemma rel_envirD: "rel_envir p f g ⟹ p (f x) (g x)"
by(auto simp add: rel_envir_def)

lemma rel_envirE [Pure.elim 2, elim]: "rel_envir p f g ⟹ (p (f x) (g x) ⟹ thesis) ⟹ thesis"
by(simp add: rel_envir_conv)

lemma rel_envir_mono: "⟦ rel_envir p f g; ⋀x. p (f x) (g x) ⟹ q (f' x) (g' x) ⟧ ⟹ rel_envir q f' g'"
by blast

lemma rel_envir_mono1: "⟦ pred_envir p f; ⋀x. p (f x) ⟹ q (f' x) (g' x) ⟧ ⟹ rel_envir q f' g'"
by blast

lemma pred_envir_mono2: "⟦ rel_envir p f g; ⋀x. p (f x) (g x) ⟹ q (f' x) ⟧ ⟹ pred_envir q f'"
by blast

end

end