src/HOL/ex/Transfer_Int_Nat.thy
author blanchet
Thu, 06 Mar 2014 14:57:14 +0100
changeset 55938 f20d1db5aa3c
parent 53013 3fbcfa911863
child 55945 e96383acecf9
permissions -rw-r--r--
renamed 'set_rel' to 'rel_set'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     1
(*  Title:      HOL/ex/Transfer_Int_Nat.thy
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman, TU Muenchen
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     3
*)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     4
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     5
header {* Using the transfer method between nat and int *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     6
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     7
theory Transfer_Int_Nat
53013
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
     8
imports GCD
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
     9
begin
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    10
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    11
subsection {* Correspondence relation *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    12
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    13
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    14
  where "ZN = (\<lambda>z n. z = of_nat n)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    15
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
    16
subsection {* Transfer domain rules *}
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
    17
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
    18
lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
    19
  unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
    20
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    21
subsection {* Transfer rules *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    22
53013
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
    23
context
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
    24
begin
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
    25
interpretation lifting_syntax .
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
    26
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    27
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    28
  unfolding ZN_def bi_unique_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    29
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    30
lemma right_total_ZN [transfer_rule]: "right_total ZN"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    31
  unfolding ZN_def right_total_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    32
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    33
lemma ZN_0 [transfer_rule]: "ZN 0 0"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    34
  unfolding ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    35
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    36
lemma ZN_1 [transfer_rule]: "ZN 1 1"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    37
  unfolding ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    38
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    39
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    40
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    41
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    42
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    43
  unfolding fun_rel_def ZN_def by (simp add: int_mult)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    44
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    45
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    46
  unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    47
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    48
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    49
  unfolding fun_rel_def ZN_def by (simp add: int_power)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    50
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    51
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    52
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    53
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    54
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    55
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    56
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    57
lemma ZN_All [transfer_rule]:
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    58
  "((ZN ===> op =) ===> op =) (Ball {0..}) All"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    59
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    60
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    61
lemma ZN_transfer_forall [transfer_rule]:
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    62
  "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    63
  unfolding transfer_forall_def transfer_bforall_def
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    64
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    65
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    66
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    67
  unfolding fun_rel_def ZN_def Bex_def atLeast_iff
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    68
  by (metis zero_le_imp_eq_int zero_zle_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    69
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    70
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    71
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    72
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    73
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    74
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    75
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    76
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    77
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    78
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    79
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    80
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    81
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    82
lemma ZN_numeral [transfer_rule]:
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    83
  "(op = ===> ZN) numeral numeral"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    84
  unfolding fun_rel_def ZN_def by simp
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    85
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    86
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    87
  unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    88
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    89
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    90
  unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    91
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    92
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    93
  unfolding fun_rel_def ZN_def by (simp add: zmod_int)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    94
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    95
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    96
  unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
    97
52360
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
    98
lemma ZN_atMost [transfer_rule]:
55938
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
    99
  "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
   100
  unfolding fun_rel_def ZN_def rel_set_def
52360
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   101
  by (clarsimp simp add: Bex_def, arith)
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   102
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   103
lemma ZN_atLeastAtMost [transfer_rule]:
55938
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
   104
  "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
   105
  unfolding fun_rel_def ZN_def rel_set_def
52360
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   106
  by (clarsimp simp add: Bex_def, arith)
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   107
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   108
lemma ZN_setsum [transfer_rule]:
55938
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
   109
  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
52360
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   110
  apply (intro fun_relI)
55938
f20d1db5aa3c renamed 'set_rel' to 'rel_set'
blanchet
parents: 53013
diff changeset
   111
  apply (erule (1) bi_unique_rel_set_lemma)
52360
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   112
  apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   113
  apply (rule setsum_cong2, simp)
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   114
  done
ac7ac2b242a2 more int/nat transfer rules; examples of new untransferred attribute
huffman
parents: 51956
diff changeset
   115
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   116
text {* For derived operations, we can use the @{text "transfer_prover"}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   117
  method to help generate transfer rules. *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   118
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   119
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   120
  unfolding listsum_def [abs_def] by transfer_prover
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   121
53013
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
   122
end
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 52360
diff changeset
   123
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   124
subsection {* Transfer examples *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   125
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   126
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   127
  assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   128
  shows "\<And>i::nat. i + 0 = i"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   129
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   130
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   131
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   132
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   133
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   134
  assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   135
  shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   136
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   137
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   138
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   139
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   140
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   141
  assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   142
  shows "\<forall>x y :: nat. x * y div y = x"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   143
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   144
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   145
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   146
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   147
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   148
  assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   149
  shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   150
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   151
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   152
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   153
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   154
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   155
  assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   156
  shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   157
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   158
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   159
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   160
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   161
text {* The @{text "fixing"} option prevents generalization over the free
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   162
  variable @{text "n"}, allowing the local transfer rule to be used. *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   163
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   164
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   165
  assumes [transfer_rule]: "ZN x n"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   166
  assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   167
  shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   168
apply (transfer fixing: n)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   169
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   170
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   171
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   172
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   173
  assumes "gcd (2^i) (3^j) = (1::int)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   174
  shows "gcd (2^i) (3^j) = (1::nat)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   175
apply (transfer fixing: i j)
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   176
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   177
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   178
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   179
lemma
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   180
  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   181
    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   182
  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   183
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   184
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   185
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   186
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
   187
text {* Quantifiers over higher types (e.g. @{text "nat list"}) are
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
   188
  transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN} *}
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   189
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   190
lemma
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
   191
  assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   192
    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   193
  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   194
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   195
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   196
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   197
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   198
text {* Equality on a higher type can be transferred if the relations
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   199
  involved are bi-unique. *}
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   200
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   201
lemma
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 47654
diff changeset
   202
  assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
47654
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   203
    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   204
  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   205
apply transfer
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   206
apply fact
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   207
done
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   208
f7df7104d13e new example theory for transfer package
huffman
parents:
diff changeset
   209
end