src/HOL/Codatatype/BNF_Util.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49314 f252c7c2ac7b
child 49463 83ac281bcdc2
permissions -rw-r--r--
tuned simpset
blanchet@49282
     1
(*  Title:      HOL/Codatatype/BNF_Util.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@49282
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Library for bounded natural functors.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
header {* Library for Bounded Natural Functors *}
blanchet@48975
    10
blanchet@49282
    11
theory BNF_Util
blanchet@49314
    12
imports "../Cardinals/Cardinal_Arithmetic"
blanchet@48975
    13
begin
blanchet@48975
    14
blanchet@48975
    15
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
blanchet@48975
    16
by blast
blanchet@48975
    17
blanchet@48975
    18
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
blanchet@48975
    19
by blast
blanchet@48975
    20
blanchet@48975
    21
lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
blanchet@48975
    22
by simp
blanchet@48975
    23
blanchet@48975
    24
definition collect where
blanchet@48975
    25
  "collect F x = (\<Union>f \<in> F. f x)"
blanchet@48975
    26
blanchet@49312
    27
(* Weak pullbacks: *)
blanchet@48975
    28
definition wpull where
blanchet@48975
    29
"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
blanchet@48975
    30
 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
blanchet@48975
    31
blanchet@48975
    32
(* Weak pseudo-pullbacks *)
blanchet@48975
    33
definition wppull where
blanchet@48975
    34
"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
blanchet@48975
    35
 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
blanchet@48975
    36
           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
blanchet@48975
    37
blanchet@48975
    38
lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
blanchet@48975
    39
by simp
blanchet@48975
    40
blanchet@48975
    41
lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
blanchet@48975
    42
by simp
blanchet@48975
    43
blanchet@48975
    44
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
blanchet@48975
    45
by simp
blanchet@48975
    46
blanchet@48975
    47
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
blanchet@48975
    48
by simp
blanchet@48975
    49
blanchet@48975
    50
lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
blanchet@48975
    51
unfolding bij_def inj_on_def by auto blast
blanchet@48975
    52
blanchet@49312
    53
(* Operator: *)
blanchet@49312
    54
definition "Gr A f = {(a, f a) | a. a \<in> A}"
blanchet@48975
    55
blanchet@49283
    56
ML_file "Tools/bnf_util.ML"
blanchet@49283
    57
ML_file "Tools/bnf_tactics.ML"
blanchet@49283
    58
blanchet@48975
    59
end