Quelle BNF_Fixpoint_Base.thy Sprache: Isabelle

(*  Title:      HOL/BNF_Fixpoint_Base.thy
    Author:     Lorenz Panny, TU Muenchen
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Martin Desharnais, TU Muenchen
    Copyright   2012, 2013, 2014

Shared fixpoint operations on bounded natural functors.
*)

section \<open>Shared Fixpoint Operations on Bounded Natural Functors\<close>

theory BNF_Fixpoint_Base
imports BNF_Composition Basic_BNFs
begin

lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)"
  by standard simp_all

lemma predicate2D_conj: "P \ Q \ R \ R \ (P x y \ Q x y)"
  by blast

lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
  by blast

lemma case_unit_Unity: "(case u of () \ f) = f"
  by (cases u) (hypsubst, rule unit.case)

lemma case_prod_Pair_iden: "(case p of (x, y) \ (x, y)) = p"
  by simp

lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x"
  by simp

lemma pointfree_idE: "f \ g = id \ f (g x) = x"
  unfolding comp_def fun_eq_iff by simp

lemma o_bij:
  assumes gf: "g \ f = id" and fg: "f \ g = id"
  shows "bij f"
unfolding bij_def inj_on_def surj_def proof safe
  fix a1 a2 assume "f a1 = f a2"
  hence "g ( f a1) = g (f a2)" by simp
  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
next
  fix b
  have "b = f (g b)"
  using fg unfolding fun_eq_iff by simp
  thus "\a. b = f a" by blast
qed

lemma case_sum_step:
  "case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
  "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
  by auto

lemma obj_one_pointE: "\x. s = x \ P \ P"
  by blast

lemma type_copy_obj_one_point_absE:
  assumes "type_definition Rep Abs UNIV" "\x. s = Abs x \ P" shows P
  using type_definition.Rep_inverse[OF assms(1)]
  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp

lemma obj_sumE_f:
  assumes "\x. s = f (Inl x) \ P" "\x. s = f (Inr x) \ P"
  shows "\x. s = f x \ P"
proof
  fix x from assms show "s = f x \ P" by (cases x) auto
qed

lemma case_sum_if:
  "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
  by simp

lemma prod_set_simps[simp]:
  "fsts (x, y) = {x}"
  "snds (x, y) = {y}"
  unfolding prod_set_defs by simp+

lemma sum_set_simps[simp]:
  "setl (Inl x) = {x}"
  "setl (Inr x) = {}"
  "setr (Inl x) = {}"
  "setr (Inr x) = {x}"
  unfolding sum_set_defs by simp+

lemma Inl_Inr_False: "(Inl x = Inr y) = False"
  by simp

lemma Inr_Inl_False: "(Inr x = Inl y) = False"
  by simp

lemma spec2: "\x y. P x y \ P x y"
  by blast

lemma rewriteR_comp_comp: "\g \ h = r\ \ f \ g \ h = f \ r"
  unfolding comp_def fun_eq_iff by auto

lemma rewriteR_comp_comp2: "\g \ h = r1 \ r2; f \ r1 = l\ \ f \ g \ h = l \ r2"
  unfolding comp_def fun_eq_iff by auto

lemma rewriteL_comp_comp: "\f \ g = l\ \ f \ (g \ h) = l \ h"
  unfolding comp_def fun_eq_iff by auto

lemma rewriteL_comp_comp2: "\f \ g = l1 \ l2; l2 \ h = r\ \ f \ (g \ h) = l1 \ r"
  unfolding comp_def fun_eq_iff by auto

lemma convol_o: "\f, g\ \ h = \f \ h, g \ h\"
  unfolding convol_def by auto

lemma map_prod_o_convol: "map_prod h1 h2 \ \f, g\ = \h1 \ f, h2 \ g\"
  unfolding convol_def by auto

lemma map_prod_o_convol_id: "(map_prod f id \ \id, g\) x = \id \ f, g\ x"
  unfolding map_prod_o_convol id_comp comp_id ..

lemma o_case_sum: "h \ case_sum f g = case_sum (h \ f) (h \ g)"
  unfolding comp_def by (auto split: sum.splits)

lemma case_sum_o_map_sum: "case_sum f g \ map_sum h1 h2 = case_sum (f \ h1) (g \ h2)"
  unfolding comp_def by (auto split: sum.splits)

lemma case_sum_o_map_sum_id: "(case_sum id g \ map_sum f id) x = case_sum (f \ id) g x"
  unfolding case_sum_o_map_sum id_comp comp_id ..

lemma rel_fun_def_butlast:
  "rel_fun R (rel_fun S T) f g = (\x y. R x y \ (rel_fun S T) (f x) (g y))"
  unfolding rel_fun_def ..

lemma subst_eq_imp: "(\a b. a = b \ P a b) \ (\a. P a a)"
  by auto

lemma eq_subset: "(=) \ (\a b. P a b \ a = b)"
  by auto

lemma eq_le_Grp_id_iff: "((=) \ Grp (Collect R) id) = (All R)"
  unfolding Grp_def id_apply by blast

lemma Grp_id_mono_subst: "(\x y. Grp P id x y \ Grp Q id (f x) (f y)) \
   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
  unfolding Grp_def by rule auto

lemma vimage2p_mono: "vimage2p f g R x y \ R \ S \ vimage2p f g S x y"
  unfolding vimage2p_def by blast

lemma vimage2p_refl: "(\x. R x x) \ vimage2p f f R x x"
  unfolding vimage2p_def by auto

lemma
  assumes "type_definition Rep Abs UNIV"
  shows type_copy_Rep_o_Abs: "Rep \ Abs = id" and type_copy_Abs_o_Rep: "Abs \ Rep = id"
  unfolding fun_eq_iff comp_apply id_apply
    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all

lemma type_copy_map_comp0_undo:
  assumes "type_definition Rep Abs UNIV"
          "type_definition Rep' Abs' UNIV"
          "type_definition Rep'' Abs'' UNIV"
  shows "Abs' \ M \ Rep'' = (Abs' \ M1 \ Rep) \ (Abs \ M2 \ Rep'') \ M1 \ M2 = M"
  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
    type_definition.Abs_inverse[OF assms(1) UNIV_I]
    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])

lemma vimage2p_id: "vimage2p id id R = R"
  unfolding vimage2p_def by auto

lemma vimage2p_comp: "vimage2p (f1 \ f2) (g1 \ g2) = vimage2p f2 g2 \ vimage2p f1 g1"
  unfolding fun_eq_iff vimage2p_def o_apply by simp

lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
  unfolding rel_fun_def vimage2p_def by auto

lemma fun_cong_unused_0: "f = (\x. g) \ f (\x. 0) = g"
  by (erule arg_cong)

lemma inj_on_convol_ident: "inj_on (\x. (x, f x)) X"
  unfolding inj_on_def by simp

lemma map_sum_if_distrib_then:
  "\f g e x y. map_sum f g (if e then Inl x else y) = (if e then Inl (f x) else map_sum f g y)"
  "\f g e x y. map_sum f g (if e then Inr x else y) = (if e then Inr (g x) else map_sum f g y)"
  by simp_all

lemma map_sum_if_distrib_else:
  "\f g e x y. map_sum f g (if e then x else Inl y) = (if e then map_sum f g x else Inl (f y))"
  "\f g e x y. map_sum f g (if e then x else Inr y) = (if e then map_sum f g x else Inr (g y))"
  by simp_all

lemma case_prod_app: "case_prod f x y = case_prod (\l r. f l r y) x"
  by (cases x) simp

lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \ f) (r \ g) x"
  by (cases x) simp_all

lemma case_sum_transfer:
  "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
  unfolding rel_fun_def by (auto split: sum.splits)

lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\l r. h (f l) (g r)) x"
  by (cases x) simp_all

lemma case_prod_o_map_prod: "case_prod f \ map_prod g1 g2 = case_prod (\l r. f (g1 l) (g2 r))"
  unfolding comp_def by auto

lemma case_prod_transfer:
  "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
  unfolding rel_fun_def by simp

lemma eq_ifI: "(P \ t = u1) \ (\ P \ t = u2) \ t = (if P then u1 else u2)"
  by simp

lemma comp_transfer:
  "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (\) (\)"
  unfolding rel_fun_def by simp

lemma If_transfer: "rel_fun (=) (rel_fun A (rel_fun A A)) If If"
  unfolding rel_fun_def by simp

lemma Abs_transfer:
  assumes type_copy1: "type_definition Rep1 Abs1 UNIV"
  assumes type_copy2: "type_definition Rep2 Abs2 UNIV"
  shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2"
  unfolding vimage2p_def rel_fun_def
    type_definition.Abs_inverse[OF type_copy1 UNIV_I]
    type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp

lemma Inl_transfer:
  "rel_fun S (rel_sum S T) Inl Inl"
  by auto

lemma Inr_transfer:
  "rel_fun T (rel_sum S T) Inr Inr"
  by auto

lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
  unfolding rel_fun_def by simp

lemma eq_onp_live_step: "x = y \ eq_onp P a a \ x \ P a \ y"
  by (simp only: eq_onp_same_args)

lemma top_conj: "top x \ P \ P" "P \ top x \ P"
  by blast+

lemma fst_convol': "fst (\f, g\ x) = f x"
  using fst_convol unfolding convol_def by simp

lemma snd_convol': "snd (\f, g\ x) = g x"
  using snd_convol unfolding convol_def by simp

lemma convol_expand_snd: "fst \ f = g \ \g, snd \ f\ = f"
  unfolding convol_def by auto

lemma convol_expand_snd':
  assumes "(fst \ f = g)"
  shows "h = snd \ f \ \g, h\ = f"
proof -
  from assms have *: "\g, snd \ f\ = f" by (rule convol_expand_snd)
  then have "h = snd \ f \ h = snd \ \g, snd \ f\" by simp
  moreover have "\ \ h = snd \ f" by (simp add: snd_convol)
  moreover have "\ \ \g, h\ = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
  ultimately show ?thesis by simp
qed

lemma case_sum_expand_Inr_pointfree: "f \ Inl = g \ case_sum g (f \ Inr) = f"
  by (auto split: sum.splits)

lemma case_sum_expand_Inr': "f \ Inl = g \ h = f \ Inr \ case_sum g h = f"
  by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits)

lemma case_sum_expand_Inr: "f \ Inl = g \ f x = case_sum g (f \ Inr) x"
  by (auto split: sum.splits)

lemma id_transfer: "rel_fun A A id id"
  unfolding rel_fun_def by simp

lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
  unfolding rel_fun_def by simp

lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
  unfolding rel_fun_def by simp

lemma convol_transfer:
  "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
  unfolding rel_fun_def convol_def by auto

lemma Let_const: "Let x (\_. c) = c"
  unfolding Let_def ..

ML_file \<open>Tools/BNF/bnf_fp_util_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_util.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_def_sugar_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_def_sugar.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_n2m_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_n2m.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_n2m_sugar.ML\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.