src/HOL/BNF_Def.thy
author wenzelm
Sun, 26 Nov 2017 21:08:32 +0100
changeset 67091 1393c2340eec
parent 66198 4a5589dd8e1a
child 67399 eab6ce8368fa
permissions -rw-r--r--
more symbols;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55059
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     1
(*  Title:      HOL/BNF_Def.thy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
57698
afef6616cbae header tuning
blanchet
parents: 57641
diff changeset
     4
    Copyright   2012, 2013, 2014
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
Definition of bounded natural functors.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59726
diff changeset
     9
section \<open>Definition of Bounded Natural Functors\<close>
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
theory BNF_Def
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    12
imports BNF_Cardinal_Arithmetic Fun_Def_Base
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    13
keywords
49286
dde4967c9233 added "defaults" option
blanchet
parents: 49284
diff changeset
    14
  "print_bnfs" :: diag and
51836
4d6dcd51dd52 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
blanchet
parents: 49537
diff changeset
    15
  "bnf" :: thy_goal
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    16
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    17
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61423
diff changeset
    18
lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    19
  by auto
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    20
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
    21
inductive
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
    22
   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" for R1 R2
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58352
diff changeset
    23
where
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
    24
  "R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
    25
| "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
    26
58446
e89f57d1e46c generate 'rec_transfer' for datatypes
desharna
parents: 58352
diff changeset
    27
definition
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    28
  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    29
where
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    30
  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    31
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    32
lemma rel_funI [intro]:
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    33
  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    34
  shows "rel_fun A B f g"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    35
  using assms by (simp add: rel_fun_def)
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    36
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    37
lemma rel_funD:
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    38
  assumes "rel_fun A B f g" and "A x y"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    39
  shows "B (f x) (g y)"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    40
  using assms by (simp add: rel_fun_def)
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    41
59513
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    42
lemma rel_fun_mono:
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    43
  "\<lbrakk> rel_fun X A f g; \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun Y B f g"
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    44
by(simp add: rel_fun_def)
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    45
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    46
lemma rel_fun_mono' [mono]:
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    47
  "\<lbrakk> \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun X A f g \<longrightarrow> rel_fun Y B f g"
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    48
by(simp add: rel_fun_def)
6949c8837e90 add monotonicity lemmas for rel_fun
Andreas Lochbihler
parents: 58916
diff changeset
    49
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    50
definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    51
  where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    52
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    53
lemma rel_setI:
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    54
  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    55
  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    56
  shows "rel_set R A B"
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    57
  using assms unfolding rel_set_def by simp
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    58
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    59
lemma predicate2_transferD:
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    60
   "\<lbrakk>rel_fun R1 (rel_fun R2 (op =)) P Q; a \<in> A; b \<in> B; A \<subseteq> {(x, y). R1 x y}; B \<subseteq> {(x, y). R2 x y}\<rbrakk> \<Longrightarrow>
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    61
   P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)"
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61423
diff changeset
    62
  unfolding rel_fun_def by (blast dest!: Collect_case_prodD)
58104
c5316f843f72 generate 'rel_transfer' for BNFs
desharna
parents: 57802
diff changeset
    63
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    64
definition collect where
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    65
  "collect F x = (\<Union>f \<in> F. f x)"
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    66
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    67
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    68
  by simp
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    69
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    70
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    71
  by simp
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    72
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    73
lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    74
  unfolding bij_def inj_on_def by auto blast
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    75
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    76
(* Operator: *)
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    77
definition "Gr A f = {(a, f a) | a. a \<in> A}"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    78
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    79
definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    80
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    81
definition vimage2p where
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    82
  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
    83
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
    84
lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
66198
4a5589dd8e1a more error checking
blanchet
parents: 63834
diff changeset
    85
  by (rule ext) (simp add: collect_def)
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
    86
57641
dc59f147b27d more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents: 57398
diff changeset
    87
definition convol ("\<langle>(_,/ _)\<rangle>") where
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    88
  "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
49495
675b9df572df rel_Gr does not depend on map_wpull
traytel
parents: 49325
diff changeset
    89
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    90
lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    91
  apply(rule ext)
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    92
  unfolding convol_def by simp
49495
675b9df572df rel_Gr does not depend on map_wpull
traytel
parents: 49325
diff changeset
    93
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    94
lemma snd_convol: "snd \<circ> \<langle>f, g\<rangle> = g"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    95
  apply(rule ext)
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
    96
  unfolding convol_def by simp
49495
675b9df572df rel_Gr does not depend on map_wpull
traytel
parents: 49325
diff changeset
    97
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
    98
lemma convol_mem_GrpI:
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 60758
diff changeset
    99
  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (case_prod (Grp A g)))"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   100
  unfolding convol_def Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   101
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   102
definition csquare where
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   103
  "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   104
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   105
lemma eq_alt: "op = = Grp UNIV id"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   106
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   107
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   108
lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   109
  by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   110
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   111
lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R"
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   112
  by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   113
53561
92bcac4f9ac9 simplified derivation of in_rel
traytel
parents: 53560
diff changeset
   114
lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)"
92bcac4f9ac9 simplified derivation of in_rel
traytel
parents: 53560
diff changeset
   115
  unfolding Grp_def by auto
92bcac4f9ac9 simplified derivation of in_rel
traytel
parents: 53560
diff changeset
   116
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   117
lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   118
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   119
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   120
lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   121
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   122
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   123
lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   124
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   125
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   126
lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   127
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   128
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   129
lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   130
  unfolding Grp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   131
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61423
diff changeset
   132
lemma Collect_case_prod_Grp_eqD: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   133
  unfolding Grp_def comp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   134
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61423
diff changeset
   135
lemma Collect_case_prod_Grp_in: "z \<in> Collect (case_prod (Grp A f)) \<Longrightarrow> fst z \<in> A"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   136
  unfolding Grp_def comp_def by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   137
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   138
definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   139
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   140
lemma pick_middlep:
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   141
  "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   142
  unfolding pick_middlep_def apply(rule someI_ex) by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   143
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   144
definition fstOp where
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   145
  "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   146
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   147
definition sndOp where
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   148
  "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   149
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 60758
diff changeset
   150
lemma fstOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (case_prod P)"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   151
  unfolding fstOp_def mem_Collect_eq
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   152
  by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   153
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   154
lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   155
  unfolding comp_def fstOp_def by simp
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   156
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   157
lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   158
  unfolding comp_def sndOp_def by simp
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   159
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 60758
diff changeset
   160
lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   161
  unfolding sndOp_def mem_Collect_eq
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   162
  by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   163
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   164
lemma csquare_fstOp_sndOp:
61423
9b6a0fb85fa3 emphasized general nature of parameter
haftmann
parents: 61422
diff changeset
   165
  "csquare (Collect (f (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   166
  unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   167
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
   168
lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   169
  by (simp split: prod.split)
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   170
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
   171
lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   172
  by (simp split: prod.split)
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   173
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 60758
diff changeset
   174
lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   175
  by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   176
51917
f964a9887713 store proper theorems even for fixed points that have no passive live variables
traytel
parents: 51916
diff changeset
   177
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   178
  by simp
49537
fe1deee434b6 generate "rel_as_srel" and "rel_flip" properties
blanchet
parents: 49510
diff changeset
   179
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   180
lemma case_sum_o_inj: "case_sum f g \<circ> Inl = f" "case_sum f g \<circ> Inr = g"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   181
  by auto
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   182
67091
1393c2340eec more symbols;
wenzelm
parents: 66198
diff changeset
   183
lemma map_sum_o_inj: "map_sum f g \<circ> Inl = Inl \<circ> f" "map_sum f g \<circ> Inr = Inr \<circ> g"
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   184
  by auto
57802
9c065009cd8a handle deep nesting in N2M
traytel
parents: 57698
diff changeset
   185
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   186
lemma card_order_csum_cone_cexp_def:
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   187
  "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   188
  unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   189
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   190
lemma If_the_inv_into_in_Func:
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   191
  "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   192
   (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   193
  unfolding Func_def by (auto dest: the_inv_into_into)
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   194
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   195
lemma If_the_inv_into_f_f:
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   196
  "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   197
  unfolding Func_def by (auto elim: the_inv_into_f_f)
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 51917
diff changeset
   198
56635
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
   199
lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
   200
  by (simp add: the_inv_f_f)
b07c8ad23010 added 'inj_map' as auxiliary BNF theorem
blanchet
parents: 55945
diff changeset
   201
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52730
diff changeset
   202
lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
63834
6a757f36997e tuned proofs;
wenzelm
parents: 63714
diff changeset
   203
  unfolding vimage2p_def .
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52660
diff changeset
   204
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   205
lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   206
  unfolding rel_fun_def vimage2p_def by auto
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52660
diff changeset
   207
61032
b57df8eecad6 standardized some occurences of ancient "split" alias
haftmann
parents: 60758
diff changeset
   208
lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)"
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52730
diff changeset
   209
  unfolding vimage2p_def convol_def by auto
52719
480a3479fa47 transfer rule for map (not yet registered as a transfer rule)
traytel
parents: 52660
diff changeset
   210
54961
e60428f432bc new codatatype example: stream processors
traytel
parents: 54841
diff changeset
   211
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
e60428f432bc new codatatype example: stream processors
traytel
parents: 54841
diff changeset
   212
  unfolding vimage2p_def Grp_def by auto
e60428f432bc new codatatype example: stream processors
traytel
parents: 54841
diff changeset
   213
58106
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   214
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   215
  by simp
c8cba801c483 generate 'set_transfer' for BNFs
desharna
parents: 58104
diff changeset
   216
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   217
lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> k) x"
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   218
  unfolding comp_apply by assumption
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58106
diff changeset
   219
59726
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   220
lemma refl_ge_eq: "(\<And>x. R x x) \<Longrightarrow> op = \<le> R"
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   221
  by auto
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   222
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   223
lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   224
  by auto
64c2bb331035 BNF relators preserve reflexivity
traytel
parents: 59513
diff changeset
   225
61240
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   226
lemma reflp_eq: "reflp R = (op = \<le> R)"
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   227
  by (auto simp: reflp_def fun_eq_iff)
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   228
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   229
lemma transp_relcompp: "transp r \<longleftrightarrow> r OO r \<le> r"
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   230
  by (auto simp: transp_def)
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   231
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   232
lemma symp_conversep: "symp R = (R\<inverse>\<inverse> \<le> R)"
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   233
  by (auto simp: symp_def fun_eq_iff)
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   234
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   235
lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y"
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   236
  by blast
464c5da3f508 more useful properties of the relators
traytel
parents: 61032
diff changeset
   237
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   238
definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   239
  where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   240
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   241
lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   242
  unfolding eq_onp_def Grp_def by auto
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   243
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   244
lemma eq_onp_to_eq: "eq_onp P x y \<Longrightarrow> x = y"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   245
  by (simp add: eq_onp_def)
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   246
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   247
lemma eq_onp_top_eq_eq: "eq_onp top = op ="
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   248
  by (simp add: eq_onp_def)
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   249
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   250
lemma eq_onp_same_args: "eq_onp P x x = P x"
63092
a949b2a5f51d eliminated use of empty "assms";
wenzelm
parents: 62329
diff changeset
   251
  by (auto simp add: eq_onp_def)
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   252
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   253
lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   254
  unfolding eq_onp_def by blast
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   255
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   256
lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   257
  by auto
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   258
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   259
lemma eq_onp_mono0: "\<forall>x\<in>A. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>x\<in>A. \<forall>y\<in>A. eq_onp P x y \<longrightarrow> eq_onp Q x y"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   260
  unfolding eq_onp_def by auto
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   261
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   262
lemma eq_onp_True: "eq_onp (\<lambda>_. True) = (op =)"
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   263
  unfolding eq_onp_def by simp
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   264
67091
1393c2340eec more symbols;
wenzelm
parents: 66198
diff changeset
   265
lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g \<circ> f)"
62324
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   266
  by auto
ae44f16dcea5 make predicator a first-class bnf citizen
traytel
parents: 61681
diff changeset
   267
62329
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   268
lemma rel_fun_Collect_case_prodD:
67091
1393c2340eec more symbols;
wenzelm
parents: 66198
diff changeset
   269
  "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f \<circ> fst) x) ((g \<circ> snd) x)"
62329
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   270
  unfolding rel_fun_def by auto
9f7fa08d2307 derive transfer rule for predicator
traytel
parents: 62324
diff changeset
   271
63714
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63092
diff changeset
   272
lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> Q"
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63092
diff changeset
   273
  unfolding eq_onp_def by auto
b62f4f765353 derive pred_mono property for BNFs
traytel
parents: 63092
diff changeset
   274
57398
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
   275
ML_file "Tools/BNF/bnf_util.ML"
882091eb1e9a merged two small theory files
blanchet
parents: 56635
diff changeset
   276
ML_file "Tools/BNF/bnf_tactics.ML"
55062
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   277
ML_file "Tools/BNF/bnf_def_tactics.ML"
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   278
ML_file "Tools/BNF/bnf_def.ML"
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49286
diff changeset
   279
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   280
end