src/HOL/List.thy
changeset 33318 ddd97d9dfbfb
parent 32960 69916a850301
child 33593 ef54e2108b74
     1.1 --- a/src/HOL/List.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -3587,8 +3587,8 @@
     1.4  by (blast intro: listrel.intros)
     1.5  
     1.6  lemma listrel_Cons:
     1.7 -     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
     1.8 -by (auto simp add: set_Cons_def intro: listrel.intros) 
     1.9 +     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
    1.10 +by (auto simp add: set_Cons_def intro: listrel.intros)
    1.11  
    1.12  
    1.13  subsection {* Size function *}
    1.14 @@ -3615,6 +3615,45 @@
    1.15  by (induct xs) force+
    1.16  
    1.17  
    1.18 +subsection {* Transfer *}
    1.19 +
    1.20 +definition
    1.21 +  embed_list :: "nat list \<Rightarrow> int list"
    1.22 +where
    1.23 +  "embed_list l = map int l"
    1.24 +
    1.25 +definition
    1.26 +  nat_list :: "int list \<Rightarrow> bool"
    1.27 +where
    1.28 +  "nat_list l = nat_set (set l)"
    1.29 +
    1.30 +definition
    1.31 +  return_list :: "int list \<Rightarrow> nat list"
    1.32 +where
    1.33 +  "return_list l = map nat l"
    1.34 +
    1.35 +lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
    1.36 +    embed_list (return_list l) = l"
    1.37 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
    1.38 +  apply (induct l)
    1.39 +  apply auto
    1.40 +done
    1.41 +
    1.42 +lemma transfer_nat_int_list_functions:
    1.43 +  "l @ m = return_list (embed_list l @ embed_list m)"
    1.44 +  "[] = return_list []"
    1.45 +  unfolding return_list_def embed_list_def
    1.46 +  apply auto
    1.47 +  apply (induct l, auto)
    1.48 +  apply (induct m, auto)
    1.49 +done
    1.50 +
    1.51 +(*
    1.52 +lemma transfer_nat_int_fold1: "fold f l x =
    1.53 +    fold (%x. f (nat x)) (embed_list l) x";
    1.54 +*)
    1.55 +
    1.56 +
    1.57  subsection {* Code generator *}
    1.58  
    1.59  subsubsection {* Setup *}
    1.60 @@ -4017,5 +4056,4 @@
    1.61    "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
    1.62  by(simp add: all_from_to_int_iff_ball list_ex_iff)
    1.63  
    1.64 -
    1.65  end