# HG changeset patch # User nipkow # Date 1124213132 -7200 # Node ID 0eb0c9259dd77ad81fff18750316020a515af039 # Parent 5b57f995a17944ac96d339d00492c0bcefd81cc9 added quite a few functions for code generation diff -r 5b57f995a179 -r 0eb0c9259dd7 src/HOL/List.ML --- a/src/HOL/List.ML Tue Aug 16 18:53:11 2005 +0200 +++ b/src/HOL/List.ML Tue Aug 16 19:25:32 2005 +0200 @@ -106,10 +106,8 @@ val list_all2_lengthD = thm "list_all2_lengthD"; val list_all2_rev = thm "list_all2_rev"; val list_all2_trans = thm "list_all2_trans"; -val list_all_Cons = thm "list_all_Cons"; -val list_all_Nil = thm "list_all_Nil"; val list_all_append = thm "list_all_append"; -val list_all_conv = thm "list_all_conv"; +val list_all_iff = thm "list_all_iff"; val list_ball_nth = thm "list_ball_nth"; val list_update_overwrite = thm "list_update_overwrite"; val list_update_same_conv = thm "list_update_same_conv"; @@ -173,7 +171,7 @@ val set_empty = thm "set_empty"; val set_filter = thm "set_filter"; val set_map = thm "set_map"; -val set_mem_eq = thm "set_mem_eq"; +val mem_ii = thm "mem_iff"; val set_remdups = thm "set_remdups"; val set_replicate = thm "set_replicate"; val set_replicate_conv_if = thm "set_replicate_conv_if"; diff -r 5b57f995a179 -r 0eb0c9259dd7 src/HOL/List.thy --- a/src/HOL/List.thy Tue Aug 16 18:53:11 2005 +0200 +++ b/src/HOL/List.thy Tue Aug 16 19:25:32 2005 +0200 @@ -26,11 +26,8 @@ last:: "'a list => 'a" butlast :: "'a list => 'a list" set :: "'a list => 'a set" - list_all:: "('a => bool) => ('a list => bool)" list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" - list_ex :: "('a \ bool) \ 'a list \ bool" map :: "('a=>'b) => ('a list => 'b list)" - mem :: "'a => 'a list => bool" (infixl 55) nth :: "'a list => nat => 'a" (infixl "!" 100) list_update :: "'a list => nat => 'a => 'a list" take:: "nat => 'a list => 'a list" @@ -48,6 +45,14 @@ rotate1 :: "'a list \ 'a list" rotate :: "nat \ 'a list \ 'a list" sublist :: "'a list => nat set => 'a list" +(* For efficiency *) + mem :: "'a => 'a list => bool" (infixl 55) + list_inter :: "'a list \ 'a list \ 'a list" + list_ex :: "('a \ bool) \ 'a list \ bool" + list_all:: "('a => bool) => ('a list => bool)" + itrev :: "'a list \ 'a list \ 'a list" + filtermap :: "('a \ 'b option) \ 'a list \ 'b list" + map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list" nonterminals lupdbinds lupdbind @@ -119,22 +124,10 @@ "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" primrec - "x mem [] = False" - "x mem (y#ys) = (if y=x then True else x mem ys)" - -primrec "set [] = {}" "set (x#xs) = insert x (set xs)" primrec - list_all_Nil:"list_all P [] = True" - list_all_Cons: "list_all P (x#xs) = (P(x) \ list_all P xs)" - -primrec -"list_ex P [] = False" -"list_ex P (x#xs) = (P x \ list_ex P xs)" - -primrec "map f [] = []" "map f (x#xs) = f(x)#map f xs" @@ -228,6 +221,38 @@ sublist_def: "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0.. set bs then a#(list_inter as bs) else list_inter as bs)" + +primrec + "list_all P [] = True" + "list_all P (x#xs) = (P(x) \ list_all P xs)" + +primrec +"list_ex P [] = False" +"list_ex P (x#xs) = (P x \ list_ex P xs)" + +primrec + "filtermap f [] = []" + "filtermap f (x#xs) = + (case f x of None \ filtermap f xs + | Some y \ y # (filtermap f xs))" + +primrec + "map_filter f P [] = []" + "map_filter f P (x#xs) = (if P x then f x # map_filter f P xs else + map_filter f P xs)" + +primrec +"itrev [] ys = ys" +"itrev (x#xs) ys = itrev xs (x#ys)" + lemma not_Cons_self [simp]: "xs \ x # xs" by (induct xs) auto @@ -667,34 +692,6 @@ by (induct xs) (auto simp add: card_insert_if) -subsubsection {* @{text mem}, @{text list_all} and @{text list_ex} *} - -text{* Only use @{text mem} for generating executable code. Otherwise -use @{prop"x : set xs"} instead --- it is much easier to reason about. -The same is true for @{text list_all} and @{text list_ex}: write -@{text"\x\set xs"} and @{text"\x\set xs"} instead because the HOL -quantifiers are aleady known to the automatic provers. For the purpose -of generating executable code use the theorems @{text set_mem_eq}, -@{text list_all_conv} and @{text list_ex_iff} to get rid off or -introduce the combinators. *} - -lemma set_mem_eq: "(x mem xs) = (x : set xs)" -by (induct xs) auto - -lemma list_all_conv: "list_all P xs = (\x \ set xs. P x)" -by (induct xs) auto - -lemma list_all_append [simp]: -"list_all P (xs @ ys) = (list_all P xs \ list_all P ys)" -by (induct xs) auto - -lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs" -by (simp add: list_all_conv) - -lemma list_ex_iff: "list_ex P xs = (\x \ set xs. P x)" -by (induct xs) simp_all - - subsubsection {* @{text filter} *} lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" @@ -1931,6 +1928,101 @@ lemma lists_UNIV [simp]: "lists UNIV = UNIV" by auto +subsubsection {* For efficiency *} + +text{* Only use @{text mem} for generating executable code. Otherwise +use @{prop"x : set xs"} instead --- it is much easier to reason about. +The same is true for @{const list_all} and @{const list_ex}: write +@{text"\x\set xs"} and @{text"\x\set xs"} instead because the HOL +quantifiers are aleady known to the automatic provers. For the purpose +of generating executable code use the theorems @{text mem_iff}, +@{text list_all_iff} and @{text list_ex_iff} to get rid off or +introduce the combinators. + +The functions @{const itrev}, @{const filtermap} and @{const +map_filter} are just there to generate efficient code. Do not use them +for modelling and proving. *} + +lemma mem_iff: "(x mem xs) = (x : set xs)" +by (induct xs) auto + +lemma list_inter_conv: "set(list_inter xs ys) = set xs \ set ys" +by (induct xs) auto + +lemma list_all_iff: "list_all P xs = (\x \ set xs. P x)" +by (induct xs) auto + +lemma list_all_append [simp]: +"list_all P (xs @ ys) = (list_all P xs \ list_all P ys)" +by (induct xs) auto + +lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs" +by (simp add: list_all_iff) + +lemma list_ex_iff: "list_ex P xs = (\x \ set xs. P x)" +by (induct xs) simp_all + +lemma itrev[simp]: "ALL ys. itrev xs ys = rev xs @ ys" +by (induct xs) simp_all + +lemma filtermap_conv: + "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \ None) xs)" +by (induct xs) auto + +lemma map_filter_conv[simp]: "map_filter f P xs = map f (filter P xs)" +by (induct xs) auto + + +subsubsection {* Code generation *} + +text{* Defaults for generating efficient code for some standard functions. *} + +lemma [code]: "rev xs = itrev xs []" +by simp + +declare upt_rec[code] + +lemma [code]: "distinct (x#xs) = (~(x mem xs) \ distinct xs)" +by (simp add:mem_iff) + +lemma [code]: + "remdups (x#xs) = (if x mem xs then remdups xs else x # remdups xs)" +by (simp add:mem_iff) + +lemma [code]: + "list_all2 P xs ys = + (length xs = length ys \ (list_all (%(x, y). P x y) (zip xs ys)))" +by (simp add:list_all2_def list_all_iff) + +lemma [code]: "list_inter (a#as) bs = + (if a mem bs then a#(list_inter as bs) else list_inter as bs)" +by(simp add:mem_iff) + +(* If you want to replace bounded quantifiers over lists by list_ex/all: + +declare list_ex_iff[symmetric, THEN eq_reflection, code unfold] +declare list_all_iff[symmetric, THEN eq_reflection, code unfold] +*) + + +subsubsection{* Inductive definition for membership *} + +consts ListMem :: "('a \ 'a list)set" +inductive ListMem +intros + elem: "(x,x#xs) \ ListMem" + insert: "(x,xs) \ ListMem \ (x,y#xs) \ ListMem" + +lemma ListMem_iff: "((x,xs) \ ListMem) = (x \ set xs)" +apply (rule iffI) + apply (induct set: ListMem) + apply auto +apply (induct xs) + apply (auto intro: ListMem.intros) +done + + + subsubsection{*Lists as Cartesian products*} text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from