src/HOL/SetInterval.thy
changeset 33318 ddd97d9dfbfb
parent 33044 fd0a9c794ec1
child 33434 e9de8d69c1b9
     1.1 --- a/src/HOL/SetInterval.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Set intervals *}
     1.5  
     1.6  theory SetInterval
     1.7 -imports Int
     1.8 +imports Int Nat_Transfer
     1.9  begin
    1.10  
    1.11  context ord
    1.12 @@ -1150,4 +1150,41 @@
    1.13    "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
    1.14    "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
    1.15  
    1.16 +subsection {* Transfer setup *}
    1.17 +
    1.18 +lemma transfer_nat_int_set_functions:
    1.19 +    "{..n} = nat ` {0..int n}"
    1.20 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
    1.21 +  apply (auto simp add: image_def)
    1.22 +  apply (rule_tac x = "int x" in bexI)
    1.23 +  apply auto
    1.24 +  apply (rule_tac x = "int x" in bexI)
    1.25 +  apply auto
    1.26 +  done
    1.27 +
    1.28 +lemma transfer_nat_int_set_function_closures:
    1.29 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
    1.30 +  by (simp add: nat_set_def)
    1.31 +
    1.32 +declare TransferMorphism_nat_int[transfer add
    1.33 +  return: transfer_nat_int_set_functions
    1.34 +    transfer_nat_int_set_function_closures
    1.35 +]
    1.36 +
    1.37 +lemma transfer_int_nat_set_functions:
    1.38 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
    1.39 +  by (simp only: is_nat_def transfer_nat_int_set_functions
    1.40 +    transfer_nat_int_set_function_closures
    1.41 +    transfer_nat_int_set_return_embed nat_0_le
    1.42 +    cong: transfer_nat_int_set_cong)
    1.43 +
    1.44 +lemma transfer_int_nat_set_function_closures:
    1.45 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
    1.46 +  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
    1.47 +
    1.48 +declare TransferMorphism_int_nat[transfer add
    1.49 +  return: transfer_int_nat_set_functions
    1.50 +    transfer_int_nat_set_function_closures
    1.51 +]
    1.52 +
    1.53  end