Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 50 kB

Quellcode-Bibliothek BNF_Least_Fixpoint.thy Sprache: Isabelle

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

Least fixpoint (datatype) operation on bounded natural functors.
*)

section \<open>Least Fixpoint (Datatype) Operation on Bounded Natural Functors\<close>

theory BNF_Least_Fixpoint
imports BNF_Fixpoint_Base
keywords
  "datatype" :: thy_defn and
  "datatype_compat" :: thy_defn
begin

lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}"
  by blast

lemma image_Collect_subsetI: "(\x. P x \ f x \ B) \ f ` {x. P x} \ B"
  by blast

lemma Collect_restrict: "{x. x \ X \ P x} \ X"
  by auto

lemma prop_restrict: "\x \ Z; Z \ {x. x \ X \ P x}\ \ P x"
  by auto

lemma underS_I: "\i \ j; (i, j) \ R\ \ i \ underS R j"
  unfolding underS_def by simp

lemma underS_E: "i \ underS R j \ i \ j \ (i, j) \ R"
  unfolding underS_def by simp

lemma underS_Field: "i \ underS R j \ i \ Field R"
  unfolding underS_def Field_def by auto

lemma ex_bij_betw: "|A| \o (r :: 'b rel) \ \f B :: 'b set. bij_betw f B A"
  by (subst (asm) internalize_card_of_ordLeq) (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])

lemma bij_betwI':
  "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y);
    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
  unfolding bij_betw_def inj_on_def by blast

lemma surj_fun_eq:
  assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 \ f) x = (g2 \ f) x"
  shows "g1 = g2"
proof (rule ext)
  fix y
  from surj_on obtain x where "x \ X" and "y = f x" by blast
  thus "g1 y = g2 y" using eq_on by simp
qed

lemma Card_order_wo_rel: "Card_order r \ wo_rel r"
  unfolding wo_rel_def card_order_on_def by blast

lemma Cinfinite_limit: "\x \ Field r; Cinfinite r\ \ \y \ Field r. x \ y \ (x, y) \ r"
  unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)

lemma Card_order_trans:
  "\Card_order r; x \ y; (x, y) \ r; y \ z; (y, z) \ r\ \ x \ z \ (x, z) \ r"
  unfolding card_order_on_def well_order_on_def linear_order_on_def
    partial_order_on_def preorder_on_def trans_def antisym_def by blast

lemma Cinfinite_limit2:
  assumes x1: "x1 \ Field r" and x2: "x2 \ Field r" and r: "Cinfinite r"
  shows "\y \ Field r. (x1 \ y \ (x1, y) \ r) \ (x2 \ y \ (x2, y) \ r)"
proof -
  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
    unfolding card_order_on_def well_order_on_def linear_order_on_def
      partial_order_on_def preorder_on_def by auto
  obtain y1 where y1: "y1 \ Field r" "x1 \ y1" "(x1, y1) \ r"
    using Cinfinite_limit[OF x1 r] by blast
  obtain y2 where y2: "y2 \ Field r" "x2 \ y2" "(x2, y2) \ r"
    using Cinfinite_limit[OF x2 r] by blast
  show ?thesis
  proof (cases "y1 = y2")
    case True with y1 y2 show ?thesis by blast
  next
    case False
    with y1(1) y2(1) total have "(y1, y2) \ r \ (y2, y1) \ r"
      unfolding total_on_def by auto
    thus ?thesis
    proof
      assume *: "(y1, y2) \ r"
      with trans y1(3) have "(x1, y2) \ r" unfolding trans_def by blast
      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
    next
      assume *: "(y2, y1) \ r"
      with trans y2(3) have "(x2, y1) \ r" unfolding trans_def by blast
      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
    qed
  qed
qed

lemma Cinfinite_limit_finite:
  "\finite X; X \ Field r; Cinfinite r\ \ \y \ Field r. \x \ X. (x \ y \ (x, y) \ r)"
proof (induct X rule: finite_induct)
  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
next
  case (insert x X)
  then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast
  then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r"
    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
  show ?case
    apply (intro bexI ballI)
    apply (erule insertE)
    apply hypsubst
    apply (rule z(2))
    using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
    apply blast
    apply (rule z(1))
    done
qed

lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A"
  by auto

lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\x. x \ Field r \ P x" for r P]

lemma meta_spec2:
  assumes "(\x y. PROP P x y)"
  shows "PROP P x y"
  by (rule assms)

lemma nchotomy_relcomppE:
  assumes "\y. \x. y = f x" "(r OO s) a c" "\b. r a (f b) \ s (f b) c \ P"
  shows P
proof (rule relcompp.cases[OF assms(2)], hypsubst)
  fix b assume "r a b" "s b c"
  moreover from assms(1) obtain b' where "b = f b'" by blast
  ultimately show P by (blast intro: assms(3))
qed

lemma predicate2D_vimage2p: "\R \ vimage2p f g S; R x y\ \ S (f x) (g y)"
  unfolding vimage2p_def by auto

lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R"
  by (rule ssubst)

lemma all_mem_range1:
  "(\y. y \ range f \ P y) \ (\x. P (f x)) "
  by (rule equal_intr_rule) fast+

lemma all_mem_range2:
  "(\fa y. fa \ range f \ y \ range fa \ P y) \ (\x xa. P (f x xa))"
  by (rule equal_intr_rule) fast+

lemma all_mem_range3:
  "(\fa fb y. fa \ range f \ fb \ range fa \ y \ range fb \ P y) \ (\x xa xb. P (f x xa xb))"
  by (rule equal_intr_rule) fast+

lemma all_mem_range4:
  "(\fa fb fc y. fa \ range f \ fb \ range fa \ fc \ range fb \ y \ range fc \ P y) \
   (\<And>x xa xb xc. P (f x xa xb xc))"
  by (rule equal_intr_rule) fast+

lemma all_mem_range5:
  "(\fa fb fc fd y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \
     y \<in> range fd \<Longrightarrow> P y) \<equiv>
   (\<And>x xa xb xc xd. P (f x xa xb xc xd))"
  by (rule equal_intr_rule) fast+

lemma all_mem_range6:
  "(\fa fb fc fd fe ff y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \
     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> y \<in> range ff \<Longrightarrow> P y) \<equiv>
   (\<And>x xa xb xc xd xe xf. P (f x xa xb xc xd xe xf))"
  by (rule equal_intr_rule) (fastforce, fast)

lemma all_mem_range7:
  "(\fa fb fc fd fe ff fg y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \
     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> fg \<in> range ff \<Longrightarrow> y \<in> range fg \<Longrightarrow> P y) \<equiv>
   (\<And>x xa xb xc xd xe xf xg. P (f x xa xb xc xd xe xf xg))"
  by (rule equal_intr_rule) (fastforce, fast)

lemma all_mem_range8:
  "(\fa fb fc fd fe ff fg fh y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \
     fe \<in> range fd \<Longrightarrow> ff \<in> range fe \<Longrightarrow> fg \<in> range ff \<Longrightarrow> fh \<in> range fg \<Longrightarrow> y \<in> range fh \<Longrightarrow> P y) \<equiv>
   (\<And>x xa xb xc xd xe xf xg xh. P (f x xa xb xc xd xe xf xg xh))"
  by (rule equal_intr_rule) (fastforce, fast)

lemmas all_mem_range = all_mem_range1 all_mem_range2 all_mem_range3 all_mem_range4 all_mem_range5
  all_mem_range6 all_mem_range7 all_mem_range8

lemma pred_fun_True_id: "NO_MATCH id p \ pred_fun (\x. True) p f = pred_fun (\x. True) id (p \ f)"
  unfolding fun.pred_map unfolding comp_def id_def ..

ML_file \<open>Tools/BNF/bnf_lfp_util.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp_compat.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close>

ML_file \<open>Tools/datatype_simprocs.ML\<close>

simproc_setup datatype_no_proper_subterm
  ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_proc\<close>

end

quality100%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.