src/HOL/BNF/BNF_Util.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 54008 b15cfc2864de
child 54435 4a655e62ad34
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
blanchet@49509
     1
(*  Title:      HOL/BNF/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@54008
    12
imports Ctr_Sugar "../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
definition collect where
blanchet@49463
    22
"collect F x = (\<Union>f \<in> F. f x)"
blanchet@48975
    23
blanchet@49312
    24
(* Weak pullbacks: *)
blanchet@48975
    25
definition wpull where
blanchet@48975
    26
"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
blanchet@48975
    27
 (\<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
    28
blanchet@48975
    29
(* Weak pseudo-pullbacks *)
blanchet@48975
    30
definition wppull where
blanchet@48975
    31
"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
blanchet@48975
    32
 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
blanchet@48975
    33
           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
blanchet@48975
    34
blanchet@48975
    35
lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
blanchet@48975
    36
by simp
blanchet@48975
    37
blanchet@48975
    38
lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
blanchet@48975
    39
by simp
blanchet@48975
    40
blanchet@48975
    41
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
blanchet@48975
    42
by simp
blanchet@48975
    43
blanchet@48975
    44
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
blanchet@48975
    45
by simp
blanchet@48975
    46
blanchet@48975
    47
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
    48
unfolding bij_def inj_on_def by auto blast
blanchet@48975
    49
blanchet@49463
    50
lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
blanchet@49463
    51
by simp
blanchet@49463
    52
blanchet@49312
    53
(* Operator: *)
blanchet@49312
    54
definition "Gr A f = {(a, f a) | a. a \<in> A}"
blanchet@48975
    55
traytel@51893
    56
definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
traytel@51893
    57
blanchet@49283
    58
ML_file "Tools/bnf_util.ML"
blanchet@49283
    59
ML_file "Tools/bnf_tactics.ML"
blanchet@49283
    60
blanchet@48975
    61
end