src/HOL/Transfer.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 71827 5e315defb038
child 75669 43f5dfb7fa35
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     1
(*  Title:      HOL/Transfer.thy
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman, TU Muenchen
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
     3
    Author:     Ondrej Kuncar, TU Muenchen
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     4
*)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     5
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
     6
section \<open>Generic theorem transfer using relations\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     7
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     8
theory Transfer
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
     9
imports Basic_BNF_LFPs Hilbert_Choice Metis
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    10
begin
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    11
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    12
subsection \<open>Relator for function space\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    13
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
    14
bundle lifting_syntax
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
    15
begin
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
    16
  notation rel_fun  (infixr "===>" 55)
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
    17
  notation map_fun  (infixr "--->" 55)
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
    18
end
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
    19
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
    20
context includes lifting_syntax
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
    21
begin
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
    22
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    23
lemma rel_funD2:
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    24
  assumes "rel_fun A B f g" and "A x x"
47937
70375fa2679d generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents: 47924
diff changeset
    25
  shows "B (f x) (g x)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    26
  using assms by (rule rel_funD)
47937
70375fa2679d generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents: 47924
diff changeset
    27
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    28
lemma rel_funE:
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    29
  assumes "rel_fun A B f g" and "A x y"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    30
  obtains "B (f x) (g y)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    31
  using assms by (simp add: rel_fun_def)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    32
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    33
lemmas rel_fun_eq = fun.rel_eq
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    34
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    35
lemma rel_fun_eq_rel:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    36
shows "rel_fun (=) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
    37
  by (simp add: rel_fun_def)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    38
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    39
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    40
subsection \<open>Transfer method\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    41
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    42
text \<open>Explicit tag for relation membership allows for
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    43
  backward proof methods.\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    44
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    45
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    46
  where "Rel r \<equiv> r"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    47
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    48
text \<open>Handling of equality relations\<close>
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 48891
diff changeset
    49
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 48891
diff changeset
    50
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    51
  where "is_equality R \<longleftrightarrow> R = (=)"
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 48891
diff changeset
    52
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    53
lemma is_equality_eq: "is_equality (=)"
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51112
diff changeset
    54
  unfolding is_equality_def by simp
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51112
diff changeset
    55
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    56
text \<open>Reverse implication for monotonicity rules\<close>
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
    57
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
    58
definition rev_implies where
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
    59
  "rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
    60
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
    61
text \<open>Handling of meta-logic connectives\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    62
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    63
definition transfer_forall where
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    64
  "transfer_forall \<equiv> All"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    65
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    66
definition transfer_implies where
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    67
  "transfer_implies \<equiv> (\<longrightarrow>)"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    68
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    69
definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    70
  where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    71
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    72
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    73
  unfolding atomize_all transfer_forall_def ..
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    74
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    75
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    76
  unfolding atomize_imp transfer_implies_def ..
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    77
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    78
lemma transfer_bforall_unfold:
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    79
  "Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    80
  unfolding transfer_bforall_def atomize_imp atomize_all ..
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47325
diff changeset
    81
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    82
lemma transfer_start: "\<lbrakk>P; Rel (=) P Q\<rbrakk> \<Longrightarrow> Q"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    83
  unfolding Rel_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    84
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    85
lemma transfer_start': "\<lbrakk>P; Rel (\<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    86
  unfolding Rel_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    87
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47627
diff changeset
    88
lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
47618
1568dadd598a make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents: 47612
diff changeset
    89
  by simp
1568dadd598a make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents: 47612
diff changeset
    90
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    91
lemma untransfer_start: "\<lbrakk>Q; Rel (=) P Q\<rbrakk> \<Longrightarrow> P"
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
    92
  unfolding Rel_def by simp
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
    93
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
    94
lemma Rel_eq_refl: "Rel (=) x x"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    95
  unfolding Rel_def ..
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    96
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47684
diff changeset
    97
lemma Rel_app:
47523
1bf0e92c1ca0 make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents: 47503
diff changeset
    98
  assumes "Rel (A ===> B) f g" and "Rel A x y"
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47684
diff changeset
    99
  shows "Rel B (f x) (g y)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   100
  using assms unfolding Rel_def rel_fun_def by fast
47523
1bf0e92c1ca0 make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents: 47503
diff changeset
   101
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47684
diff changeset
   102
lemma Rel_abs:
47523
1bf0e92c1ca0 make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents: 47503
diff changeset
   103
  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47684
diff changeset
   104
  shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   105
  using assms unfolding Rel_def rel_fun_def by fast
47523
1bf0e92c1ca0 make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents: 47503
diff changeset
   106
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   107
subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   108
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   109
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   110
  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   111
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   112
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   113
  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   114
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   115
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   116
  where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   117
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   118
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   119
  where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   120
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   121
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   122
  where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   123
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   124
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   125
  where "bi_unique R \<longleftrightarrow>
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   126
    (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   127
    (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   128
71827
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   129
lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   130
  unfolding Uniq_def left_unique_def by force
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   131
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   132
lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   133
unfolding left_unique_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   134
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   135
lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   136
unfolding left_unique_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   137
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   138
lemma left_totalI:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   139
  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   140
unfolding left_total_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   141
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   142
lemma left_totalE:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   143
  assumes "left_total R"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   144
  obtains "(\<And>x. \<exists>y. R x y)"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   145
using assms unfolding left_total_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   146
53927
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   147
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
71827
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   148
  by(simp add: bi_unique_def)
53927
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   149
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   150
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
71827
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   151
  by(simp add: bi_unique_def)
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   152
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   153
lemma bi_unique_iff: "bi_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z) \<and> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   154
  unfolding Uniq_def bi_unique_def by force
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   155
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   156
lemma right_unique_iff: "right_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
5e315defb038 the Uniq quantifier
paulson <lp15@cam.ac.uk>
parents: 71697
diff changeset
   157
  unfolding Uniq_def right_unique_def by force
53927
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   158
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   159
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   160
unfolding right_unique_def by fast
53927
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   161
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   162
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   163
unfolding right_unique_def by fast
53927
abe2b313f0e5 add lemmas
Andreas Lochbihler
parents: 53011
diff changeset
   164
59514
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   165
lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   166
by(simp add: right_total_def)
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   167
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   168
lemma right_totalE:
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   169
  assumes "right_total A"
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   170
  obtains x where "A x y"
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   171
using assms by(auto simp add: right_total_def)
509caf5edfa6 add intro and elim rules for right_total
Andreas Lochbihler
parents: 59276
diff changeset
   172
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   173
lemma right_total_alt_def2:
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   174
  "right_total R \<longleftrightarrow> ((R ===> (\<longrightarrow>)) ===> (\<longrightarrow>)) All All" (is "?lhs = ?rhs")
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   175
proof
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   176
  assume ?lhs then show ?rhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   177
    unfolding right_total_def rel_fun_def by blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   178
next
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   179
  assume \<section>: ?rhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   180
  show ?lhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   181
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   182
    unfolding right_total_def by blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   183
qed
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   184
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   185
lemma right_unique_alt_def2:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   186
  "right_unique R \<longleftrightarrow> (R ===> R ===> (\<longrightarrow>)) (=) (=)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   187
  unfolding right_unique_def rel_fun_def by auto
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   188
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   189
lemma bi_total_alt_def2:
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   190
  "bi_total R \<longleftrightarrow> ((R ===> (=)) ===> (=)) All All" (is "?lhs = ?rhs")
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   191
proof
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   192
  assume ?lhs then show ?rhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   193
    unfolding bi_total_def rel_fun_def by blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   194
next
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   195
  assume \<section>: ?rhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   196
  show ?lhs
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   197
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. \<exists>y. R x y" "\<lambda>y. True"]
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   198
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   199
    by (auto simp: bi_total_def)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   200
qed
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   201
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   202
lemma bi_unique_alt_def2:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   203
  "bi_unique R \<longleftrightarrow> (R ===> R ===> (=)) (=) (=)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   204
  unfolding bi_unique_def rel_fun_def by auto
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   205
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   206
lemma [simp]:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   207
  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   208
    and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   209
  by(auto simp add: left_unique_def right_unique_def)
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   210
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   211
lemma [simp]:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   212
  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   213
    and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   214
  by(simp_all add: left_total_def right_total_def)
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   215
53944
50c8f7f21327 add lemmas
Andreas Lochbihler
parents: 53927
diff changeset
   216
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   217
  by(auto simp add: bi_unique_def)
53944
50c8f7f21327 add lemmas
Andreas Lochbihler
parents: 53927
diff changeset
   218
50c8f7f21327 add lemmas
Andreas Lochbihler
parents: 53927
diff changeset
   219
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   220
  by(auto simp add: bi_total_def)
53944
50c8f7f21327 add lemmas
Andreas Lochbihler
parents: 53927
diff changeset
   221
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   222
lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> (=))" unfolding right_unique_def by blast
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   223
lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> (=))" unfolding left_unique_def by blast
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   224
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   225
lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> (=))" unfolding right_total_def by blast
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   226
lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> (=))" unfolding left_total_def by blast
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   227
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   228
lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   229
unfolding left_total_def right_total_def bi_total_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   230
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   231
lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   232
unfolding left_unique_def right_unique_def bi_unique_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   233
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   234
lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   235
unfolding bi_total_alt_def ..
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   236
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   237
lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   238
unfolding bi_unique_alt_def ..
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   239
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   240
end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   241
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   242
70491
8cac53925407 prefer named lemmas -- more compact proofterms;
wenzelm
parents: 69605
diff changeset
   243
lemma is_equality_lemma: "(\<And>R. is_equality R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (=))"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   244
  unfolding is_equality_def
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   245
proof (rule equal_intr_rule)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   246
  show "(\<And>R. R = (=) \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (=)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   247
    apply (drule meta_spec)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   248
    apply (erule meta_mp [OF _ refl])
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   249
    done
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   250
qed simp
70491
8cac53925407 prefer named lemmas -- more compact proofterms;
wenzelm
parents: 69605
diff changeset
   251
8cac53925407 prefer named lemmas -- more compact proofterms;
wenzelm
parents: 69605
diff changeset
   252
lemma Domainp_lemma: "(\<And>R. Domainp T = R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (Domainp T))"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   253
proof (rule equal_intr_rule)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   254
  show "(\<And>R. Domainp T = R \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (Domainp T)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   255
    apply (drule meta_spec)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   256
    apply (erule meta_mp [OF _ refl])
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   257
    done
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   258
qed simp
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   259
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   260
ML_file \<open>Tools/Transfer/transfer.ML\<close>
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   261
declare refl [transfer_rule]
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   262
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   263
hide_const (open) Rel
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   264
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
   265
context includes lifting_syntax
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   266
begin
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   267
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   268
text \<open>Handling of domains\<close>
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   269
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   270
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   271
  by auto
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   272
58386
traytel
parents: 58182
diff changeset
   273
lemma Domainp_refl[transfer_domain_rule]:
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   274
  "Domainp T = Domainp T" ..
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   275
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   276
lemma Domain_eq_top[transfer_domain_rule]: "Domainp (=) = top" by auto
60229
4cd6462c1fda Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents: 59523
diff changeset
   277
64425
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   278
lemma Domainp_pred_fun_eq[relator_domain]:
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   279
  assumes "left_unique T"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   280
  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"   (is "?lhs = ?rhs")
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   281
proof (intro ext iffI)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   282
  fix x
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   283
  assume "?lhs x"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   284
  then show "?rhs x"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   285
    using assms unfolding rel_fun_def pred_fun_def by blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   286
next
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   287
  fix x
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   288
  assume "?rhs x"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   289
  then have "\<exists>g. \<forall>y xa. T xa y \<longrightarrow> S (x xa) (g y)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   290
    using assms unfolding Domainp_iff left_unique_def  pred_fun_def
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   291
    by (intro choice) blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   292
  then show "?lhs x"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   293
    by blast
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   294
qed
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   295
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   296
text \<open>Properties are preserved by relation composition.\<close>
47660
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   297
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   298
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   299
  by auto
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   300
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   301
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   302
  unfolding bi_total_def OO_def by fast
47660
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   303
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   304
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   305
  unfolding bi_unique_def OO_def by blast
47660
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   306
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   307
lemma right_total_OO:
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   308
  "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   309
  unfolding right_total_def OO_def by fast
47660
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   310
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   311
lemma right_unique_OO:
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   312
  "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   313
  unfolding right_unique_def OO_def by fast
47660
7a5c681c0265 new example theory for quotient/transfer
huffman
parents: 47658
diff changeset
   314
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   315
lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   316
  unfolding left_total_def OO_def by fast
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   317
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   318
lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   319
  unfolding left_unique_def OO_def by blast
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   320
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   321
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   322
subsection \<open>Properties of relators\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   323
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   324
lemma left_total_eq[transfer_rule]: "left_total (=)"
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   325
  unfolding left_total_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   326
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   327
lemma left_unique_eq[transfer_rule]: "left_unique (=)"
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   328
  unfolding left_unique_def by blast
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   329
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   330
lemma right_total_eq [transfer_rule]: "right_total (=)"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   331
  unfolding right_total_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   332
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   333
lemma right_unique_eq [transfer_rule]: "right_unique (=)"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   334
  unfolding right_unique_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   335
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   336
lemma bi_total_eq[transfer_rule]: "bi_total (=)"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   337
  unfolding bi_total_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   338
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   339
lemma bi_unique_eq[transfer_rule]: "bi_unique (=)"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   340
  unfolding bi_unique_def by simp
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   341
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   342
lemma left_total_fun[transfer_rule]:
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   343
  assumes "left_unique A" "left_total B"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   344
  shows "left_total (A ===> B)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   345
  unfolding left_total_def 
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   346
proof
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   347
  fix f
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   348
  show "Ex ((A ===> B) f)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   349
    unfolding rel_fun_def
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   350
  proof (intro exI strip)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   351
    fix x y
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   352
    assume A: "A x y"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   353
    have "(THE x. A x y) = x"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   354
      using A assms by (simp add: left_unique_def the_equality)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   355
    then show "B (f x) (SOME z. B (f (THE x. A x y)) z)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   356
      using assms by (force simp: left_total_def intro: someI_ex)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   357
  qed
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   358
qed
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   359
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   360
lemma left_unique_fun[transfer_rule]:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   361
  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   362
  unfolding left_total_def left_unique_def rel_fun_def
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   363
  by (clarify, rule ext, fast)
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   364
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   365
lemma right_total_fun [transfer_rule]:
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   366
  assumes "right_unique A" "right_total B"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   367
  shows "right_total (A ===> B)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   368
  unfolding right_total_def 
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   369
proof
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   370
  fix g
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   371
  show "\<exists>x. (A ===> B) x g"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   372
    unfolding rel_fun_def
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   373
  proof (intro exI strip)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   374
    fix x y
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   375
    assume A: "A x y"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   376
    have "(THE y. A x y) = y"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   377
      using A assms by (simp add: right_unique_def the_equality)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   378
    then show "B (SOME z. B z (g (THE y. A x y))) (g y)"
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   379
      using assms by (force simp: right_total_def intro: someI_ex)
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   380
  qed
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   381
qed
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   382
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   383
lemma right_unique_fun [transfer_rule]:
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   384
  "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   385
  unfolding right_total_def right_unique_def rel_fun_def
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   386
  by (clarify, rule ext, fast)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   387
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   388
lemma bi_total_fun[transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   389
  "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   390
  unfolding bi_unique_alt_def bi_total_alt_def
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   391
  by (blast intro: right_total_fun left_total_fun)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   392
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   393
lemma bi_unique_fun[transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   394
  "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   395
  unfolding bi_unique_alt_def bi_total_alt_def
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   396
  by (blast intro: right_unique_fun left_unique_fun)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   397
56543
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   398
end
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   399
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   400
lemma if_conn:
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   401
  "(if P \<and> Q then t else e) = (if P then if Q then t else e else e)"
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   402
  "(if P \<or> Q then t else e) = (if P then t else if Q then t else e)"
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   403
  "(if P \<longrightarrow> Q then t else e) = (if P then if Q then t else e else t)"
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   404
  "(if \<not> P then t else e) = (if P then e else t)"
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   405
by auto
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   406
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   407
ML_file \<open>Tools/Transfer/transfer_bnf.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   408
ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_transfer.ML\<close>
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59141
diff changeset
   409
56543
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   410
declare pred_fun_def [simp]
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   411
declare rel_fun_eq [relator_eq]
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   412
64425
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   413
(* Delete the automated generated rule from the bnf command;
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   414
  we have a more general rule (Domainp_pred_fun_eq) that subsumes it. *)
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   415
declare fun.Domainp_rel[relator_domain del]
b17acc1834e3 a more general relator domain rule for the function type
kuncar
parents: 64014
diff changeset
   416
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   417
subsection \<open>Transfer rules\<close>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   418
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 63092
diff changeset
   419
context includes lifting_syntax
56543
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   420
begin
9bd56f2e4c10 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents: 56524
diff changeset
   421
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   422
lemma Domainp_forall_transfer [transfer_rule]:
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   423
  assumes "right_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   424
  shows "((A ===> (=)) ===> (=))
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   425
    (transfer_bforall (Domainp A)) transfer_forall"
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   426
  using assms unfolding right_total_def
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   427
  unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   428
  by fast
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   429
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   430
text \<open>Transfer rules using implication instead of equality on booleans.\<close>
47684
ead185e60b8c tuned precedence order of transfer rules
huffman
parents: 47660
diff changeset
   431
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   432
lemma transfer_forall_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   433
  "bi_total A \<Longrightarrow> ((A ===> (=)) ===> (=)) transfer_forall transfer_forall"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   434
  "right_total A \<Longrightarrow> ((A ===> (=)) ===> implies) transfer_forall transfer_forall"
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   435
  "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   436
  "bi_total A \<Longrightarrow> ((A ===> (=)) ===> rev_implies) transfer_forall transfer_forall"
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   437
  "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   438
  unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
56085
3d11892ea537 killed a few 'metis' calls
blanchet
parents: 55945
diff changeset
   439
  by fast+
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   440
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   441
lemma transfer_implies_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   442
  "((=)        ===> (=)        ===> (=)       ) transfer_implies transfer_implies"
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   443
  "(rev_implies ===> implies     ===> implies    ) transfer_implies transfer_implies"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   444
  "(rev_implies ===> (=)        ===> implies    ) transfer_implies transfer_implies"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   445
  "((=)        ===> implies     ===> implies    ) transfer_implies transfer_implies"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   446
  "((=)        ===> (=)        ===> implies    ) transfer_implies transfer_implies"
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   447
  "(implies     ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   448
  "(implies     ===> (=)        ===> rev_implies) transfer_implies transfer_implies"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   449
  "((=)        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   450
  "((=)        ===> (=)        ===> rev_implies) transfer_implies transfer_implies"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   451
  unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51956
diff changeset
   452
47684
ead185e60b8c tuned precedence order of transfer rules
huffman
parents: 47660
diff changeset
   453
lemma eq_imp_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   454
  "right_unique A \<Longrightarrow> (A ===> A ===> (\<longrightarrow>)) (=) (=)"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   455
  unfolding right_unique_alt_def2 .
47684
ead185e60b8c tuned precedence order of transfer rules
huffman
parents: 47660
diff changeset
   456
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   457
text \<open>Transfer rules using equality.\<close>
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   458
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   459
lemma left_unique_transfer [transfer_rule]:
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   460
  assumes "right_total A"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   461
  assumes "right_total B"
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   462
  assumes "bi_unique A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   463
  shows "((A ===> B ===> (=)) ===> implies) left_unique left_unique"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   464
  using assms unfolding left_unique_def right_total_def bi_unique_def rel_fun_def
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   465
  by metis
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56085
diff changeset
   466
47636
b786388b4b3a uniform naming scheme for transfer rules
huffman
parents: 47635
diff changeset
   467
lemma eq_transfer [transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   468
  assumes "bi_unique A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   469
  shows "(A ===> A ===> (=)) (=) (=)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   470
  using assms unfolding bi_unique_def rel_fun_def by auto
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   471
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   472
lemma right_total_Ex_transfer[transfer_rule]:
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   473
  assumes "right_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   474
  shows "((A ===> (=)) ===> (=)) (Bex (Collect (Domainp A))) Ex"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   475
  using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   476
  by fast
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   477
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   478
lemma right_total_All_transfer[transfer_rule]:
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   479
  assumes "right_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   480
  shows "((A ===> (=)) ===> (=)) (Ball (Collect (Domainp A))) All"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   481
  using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   482
  by fast
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   483
70927
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   484
context
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   485
  includes lifting_syntax
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   486
begin
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   487
68521
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   488
lemma right_total_fun_eq_transfer:
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   489
  assumes [transfer_rule]: "right_total A" "bi_unique B"
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   490
  shows "((A ===> B) ===> (A ===> B) ===> (=)) (\<lambda>f g. \<forall>x\<in>Collect(Domainp A). f x = g x) (=)"
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   491
  unfolding fun_eq_iff
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   492
  by transfer_prover
1bad08165162 added lemmas and transfer rules
immler
parents: 67399
diff changeset
   493
70927
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   494
end
cc204e10385c tuned syntax
haftmann
parents: 70491
diff changeset
   495
47636
b786388b4b3a uniform naming scheme for transfer rules
huffman
parents: 47635
diff changeset
   496
lemma All_transfer [transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   497
  assumes "bi_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   498
  shows "((A ===> (=)) ===> (=)) All All"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   499
  using assms unfolding bi_total_def rel_fun_def by fast
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   500
47636
b786388b4b3a uniform naming scheme for transfer rules
huffman
parents: 47635
diff changeset
   501
lemma Ex_transfer [transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   502
  assumes "bi_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   503
  shows "((A ===> (=)) ===> (=)) Ex Ex"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   504
  using assms unfolding bi_total_def rel_fun_def by fast
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   505
59515
28e1349eb48b add parametricity rule for Ex1
Andreas Lochbihler
parents: 59514
diff changeset
   506
lemma Ex1_parametric [transfer_rule]:
28e1349eb48b add parametricity rule for Ex1
Andreas Lochbihler
parents: 59514
diff changeset
   507
  assumes [transfer_rule]: "bi_unique A" "bi_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   508
  shows "((A ===> (=)) ===> (=)) Ex1 Ex1"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   509
unfolding Ex1_def by transfer_prover
59515
28e1349eb48b add parametricity rule for Ex1
Andreas Lochbihler
parents: 59514
diff changeset
   510
58448
a1d4e7473c98 generate 'corec_transfer' for codatatypes
desharna
parents: 58444
diff changeset
   511
declare If_transfer [transfer_rule]
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   512
47636
b786388b4b3a uniform naming scheme for transfer rules
huffman
parents: 47635
diff changeset
   513
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   514
  unfolding rel_fun_def by simp
47612
bc9c7b5c26fd add transfer rule for Let
huffman
parents: 47523
diff changeset
   515
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
   516
declare id_transfer [transfer_rule]
47625
10cfaf771687 add transfer rule for 'id'
huffman
parents: 47618
diff changeset
   517
58444
ed95293f14b6 generate 'ctor_rec_transfer' for datatypes
desharna
parents: 58386
diff changeset
   518
declare comp_transfer [transfer_rule]
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   519
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
   520
lemma curry_transfer [transfer_rule]:
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
   521
  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
   522
  unfolding curry_def by transfer_prover
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58889
diff changeset
   523
47636
b786388b4b3a uniform naming scheme for transfer rules
huffman
parents: 47635
diff changeset
   524
lemma fun_upd_transfer [transfer_rule]:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   525
  assumes [transfer_rule]: "bi_unique A"
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   526
  shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   527
  unfolding fun_upd_def  by transfer_prover
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   528
55415
05f5fdb8d093 renamed 'nat_{case,rec}' to '{case,rec}_nat'
blanchet
parents: 55084
diff changeset
   529
lemma case_nat_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   530
  "(A ===> ((=) ===> A) ===> (=) ===> A) case_nat case_nat"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   531
  unfolding rel_fun_def by (simp split: nat.split)
47627
2b1d3eda59eb add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents: 47625
diff changeset
   532
55415
05f5fdb8d093 renamed 'nat_{case,rec}' to '{case,rec}_nat'
blanchet
parents: 55084
diff changeset
   533
lemma rec_nat_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   534
  "(A ===> ((=) ===> A ===> A) ===> (=) ===> A) rec_nat rec_nat"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55811
diff changeset
   535
  unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
47924
4e951258204b add transfer rules for nat_rec and funpow
huffman
parents: 47789
diff changeset
   536
4e951258204b add transfer rules for nat_rec and funpow
huffman
parents: 47789
diff changeset
   537
lemma funpow_transfer [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   538
  "((=) ===> (A ===> A) ===> (A ===> A)) compow compow"
47924
4e951258204b add transfer rules for nat_rec and funpow
huffman
parents: 47789
diff changeset
   539
  unfolding funpow_def by transfer_prover
4e951258204b add transfer rules for nat_rec and funpow
huffman
parents: 47789
diff changeset
   540
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   541
lemma mono_transfer[transfer_rule]:
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   542
  assumes [transfer_rule]: "bi_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   543
  assumes [transfer_rule]: "(A ===> A ===> (=)) (\<le>) (\<le>)"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   544
  assumes [transfer_rule]: "(B ===> B ===> (=)) (\<le>) (\<le>)"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   545
  shows "((A ===> B) ===> (=)) mono mono"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   546
unfolding mono_def by transfer_prover
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   547
58182
82478e6c60cb tweaked setup for datatype realizer
blanchet
parents: 58128
diff changeset
   548
lemma right_total_relcompp_transfer[transfer_rule]:
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   549
  assumes [transfer_rule]: "right_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   550
  shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=))
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   551
    (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) (OO)"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   552
unfolding OO_def by transfer_prover
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   553
58182
82478e6c60cb tweaked setup for datatype realizer
blanchet
parents: 58128
diff changeset
   554
lemma relcompp_transfer[transfer_rule]:
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   555
  assumes [transfer_rule]: "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   556
  shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (OO) (OO)"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   557
unfolding OO_def by transfer_prover
47627
2b1d3eda59eb add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents: 47625
diff changeset
   558
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   559
lemma right_total_Domainp_transfer[transfer_rule]:
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   560
  assumes [transfer_rule]: "right_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   561
  shows "((A ===> B ===> (=)) ===> A ===> (=)) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp"
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   562
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   563
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   564
lemma Domainp_transfer[transfer_rule]:
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   565
  assumes [transfer_rule]: "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   566
  shows "((A ===> B ===> (=)) ===> A ===> (=)) Domainp Domainp"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   567
unfolding Domainp_iff by transfer_prover
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   568
58182
82478e6c60cb tweaked setup for datatype realizer
blanchet
parents: 58128
diff changeset
   569
lemma reflp_transfer[transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   570
  "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> (=)) reflp reflp"
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   571
  "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   572
  "right_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> implies) reflp reflp"
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   573
  "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   574
  "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> rev_implies) reflp reflp"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   575
unfolding reflp_def rev_implies_def bi_total_def right_total_def rel_fun_def
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   576
by fast+
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   577
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   578
lemma right_unique_transfer [transfer_rule]:
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   579
  "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   580
  \<Longrightarrow> ((A ===> B ===> (=)) ===> implies) right_unique right_unique"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   581
unfolding right_unique_def right_total_def bi_unique_def rel_fun_def
53952
b2781a3ce958 new parametricity rules and useful lemmas
kuncar
parents: 53944
diff changeset
   582
by metis
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   583
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   584
lemma left_total_parametric [transfer_rule]:
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   585
  assumes [transfer_rule]: "bi_total A" "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   586
  shows "((A ===> B ===> (=)) ===> (=)) left_total left_total"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   587
unfolding left_total_def by transfer_prover
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   588
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   589
lemma right_total_parametric [transfer_rule]:
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   590
  assumes [transfer_rule]: "bi_total A" "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   591
  shows "((A ===> B ===> (=)) ===> (=)) right_total right_total"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   592
unfolding right_total_def by transfer_prover
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   593
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   594
lemma left_unique_parametric [transfer_rule]:
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   595
  assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   596
  shows "((A ===> B ===> (=)) ===> (=)) left_unique left_unique"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   597
unfolding left_unique_def by transfer_prover
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   598
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   599
lemma prod_pred_parametric [transfer_rule]:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   600
  "((A ===> (=)) ===> (B ===> (=)) ===> rel_prod A B ===> (=)) pred_prod pred_prod"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   601
unfolding prod.pred_set Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   602
by simp transfer_prover
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   603
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   604
lemma apfst_parametric [transfer_rule]:
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   605
  "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   606
unfolding apfst_def by transfer_prover
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   607
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   608
lemma rel_fun_eq_eq_onp: "((=) ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   609
unfolding eq_onp_def rel_fun_def by auto
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   610
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   611
lemma rel_fun_eq_onp_rel:
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   612
  shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   613
by (auto simp add: eq_onp_def rel_fun_def)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   614
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   615
lemma eq_onp_transfer [transfer_rule]:
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   616
  assumes [transfer_rule]: "bi_unique A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   617
  shows "((A ===> (=)) ===> A ===> A ===> (=)) eq_onp eq_onp"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   618
unfolding eq_onp_def by transfer_prover
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents: 56520
diff changeset
   619
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   620
lemma rtranclp_parametric [transfer_rule]:
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   621
  assumes "bi_unique A" "bi_total A"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   622
  shows "((A ===> A ===> (=)) ===> A ===> A ===> (=)) rtranclp rtranclp"
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   623
proof(rule rel_funI iffI)+
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   624
  fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and R' x y x' y'
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   625
  assume R: "(A ===> A ===> (=)) R R'" and "A x x'"
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   626
  {
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   627
    assume "R\<^sup>*\<^sup>* x y" "A y y'"
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   628
    thus "R'\<^sup>*\<^sup>* x' y'"
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   629
    proof(induction arbitrary: y')
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   630
      case base
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   631
      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x' = y'" by(rule bi_uniqueDr)
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   632
      thus ?case by simp
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   633
    next
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   634
      case (step y z z')
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   635
      from \<open>bi_total A\<close> obtain y' where "A y y'" unfolding bi_total_def by blast
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   636
      hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   637
      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R y z\<close>
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   638
      have "R' y' z'" by(auto dest: rel_funD)
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   639
      ultimately show ?case ..
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   640
    qed
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   641
  next
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   642
    assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   643
    thus "R\<^sup>*\<^sup>* x y"
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   644
    proof(induction arbitrary: y)
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   645
      case base
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   646
      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x = y" by(rule bi_uniqueDl)
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   647
      thus ?case by simp
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   648
    next
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   649
      case (step y' z' z)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   650
      from \<open>bi_total A\<close> obtain y where "A y y'" unfolding bi_total_def by blast
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   651
      hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60229
diff changeset
   652
      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R' y' z'\<close>
57599
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   653
      have "R y z" by(auto dest: rel_funD)
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   654
      ultimately show ?case ..
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   655
    qed
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   656
  }
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   657
qed
7ef939f89776 add parametricity lemmas
Andreas Lochbihler
parents: 57398
diff changeset
   658
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   659
lemma right_unique_parametric [transfer_rule]:
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   660
  assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 64425
diff changeset
   661
  shows "((A ===> B ===> (=)) ===> (=)) right_unique right_unique"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   662
  unfolding right_unique_def by transfer_prover
59523
860fb1c65553 more transfer rules
Andreas Lochbihler
parents: 59515
diff changeset
   663
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 60758
diff changeset
   664
lemma map_fun_parametric [transfer_rule]:
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 60758
diff changeset
   665
  "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   666
  unfolding map_fun_def by transfer_prover
61630
608520e0e8e2 add various lemmas
Andreas Lochbihler
parents: 60758
diff changeset
   667
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   668
end
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
   669
64014
ca1239a3277b more lemmas
haftmann
parents: 63343
diff changeset
   670
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   671
subsection \<open>\<^const>\<open>of_bool\<close> and \<^const>\<open>of_nat\<close>\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   672
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   673
context
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   674
  includes lifting_syntax
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   675
begin
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   676
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   677
lemma transfer_rule_of_bool:
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   678
  \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   679
    if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   680
    for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   681
  unfolding of_bool_def by transfer_prover
64014
ca1239a3277b more lemmas
haftmann
parents: 63343
diff changeset
   682
ca1239a3277b more lemmas
haftmann
parents: 63343
diff changeset
   683
lemma transfer_rule_of_nat:
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   684
  "((=) ===> (\<cong>)) of_nat of_nat"
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   685
    if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   686
    \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   687
  for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
71697
34ff9ca387c0 fixed more nasty proofs
paulson <lp15@cam.ac.uk>
parents: 71182
diff changeset
   688
  unfolding of_nat_def by transfer_prover
64014
ca1239a3277b more lemmas
haftmann
parents: 63343
diff changeset
   689
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 52358
diff changeset
   690
end
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   691
410935efbf5c characterization of singleton bit operation
haftmann
parents: 70927
diff changeset
   692
end