# HG changeset patch # User haftmann # Date 1277790918 -7200 # Node ID 165cd386288dabff2bf3f7c470b04877c485fe39 # Parent 32ad67684ee77265ce02ec24d83ff88d94563e71# Parent ebb8b1a79c4c07a9cdc97793e17ac2af20c749cd merged diff -r 32ad67684ee7 -r 165cd386288d NEWS --- a/NEWS Tue Jun 29 02:18:08 2010 +0100 +++ b/NEWS Tue Jun 29 07:55:18 2010 +0200 @@ -21,6 +21,22 @@ of ML functions, facts etc. involving split have been retained so far, though. INCOMPATIBILITY. +* Dropped old infix syntax "mem" for List.member; use "in set" +instead. INCOMPATIBILITY. + +* Refactoring of code-generation specific operations in List.thy + + constants + null ~> List.null + + facts + mem_iff ~> member_def + null_empty ~> null_def + +INCOMPATIBILITY. Note that these were not suppossed to be used +regularly unless for striking reasons; their main purpose was code +generation. + * Some previously unqualified names have been qualified: types diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 07:55:18 2010 +0200 @@ -201,14 +201,16 @@ lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" by (induct l, auto) -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" -by (induct l, auto) +lemma mem_cnb_minus: "x \ set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" + by (induct l) auto lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x" +lemma cnb_minus [simp]: "x \ set l ==> cnb (remove l x) = cnb l - crypt_nb x" apply (induct l, auto) -by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp) +apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI) +apply simp +done lemma parts_cnb: "Z:parts (set l) ==> cnb l = (cnb l - crypt_nb Z) + crypt_nb Z" @@ -272,7 +274,7 @@ apply (clarsimp, blast) (* K ~:invKey`Ks *) apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))") -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) +apply (drule_tac x="decrypt' l' K Y" in spec, simp) apply (subgoal_tac "Crypt K Y:parts (set l)") apply (drule parts_cnb, rotate_tac -1, simp) apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 07:55:18 2010 +0200 @@ -197,12 +197,12 @@ lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" by (induct l, auto) -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" +lemma mem_cnb_minus: "x \ set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" by (induct l, auto) lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x" +lemma cnb_minus [simp]: "x \ set l ==> cnb (remove l x) = cnb l - crypt_nb x" apply (induct l, auto) by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp) @@ -268,7 +268,7 @@ apply (clarsimp, blast) (* K ~:invKey`Ks *) apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))") -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) +apply (drule_tac x="decrypt' l' K Y" in spec, simp) apply (subgoal_tac "Crypt K Y:parts (set l)") apply (drule parts_cnb, rotate_tac -1, simp) apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Bali/Trans.thy Tue Jun 29 07:55:18 2010 +0200 @@ -10,7 +10,7 @@ theory Trans imports Evaln begin definition groundVar :: "var \ bool" where -"groundVar v \ (case v of +"groundVar v \ (case v of LVar ln \ True | {accC,statDeclC,stat}e..fn \ \ a. e=Lit a | e1.[e2] \ \ a i. e1= Lit a \ e2 = Lit i @@ -35,19 +35,15 @@ qed definition groundExprs :: "expr list \ bool" where -"groundExprs es \ list_all (\ e. \ v. e=Lit v) es" + "groundExprs es \ (\e \ set es. \v. e = Lit v)" -consts the_val:: "expr \ val" -primrec -"the_val (Lit v) = v" +primrec the_val:: "expr \ val" where + "the_val (Lit v) = v" -consts the_var:: "prog \ state \ var \ (vvar \ state)" -primrec -"the_var G s (LVar ln) =(lvar ln (store s),s)" -the_var_FVar_def: -"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" -the_var_AVar_def: -"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" +primrec the_var:: "prog \ state \ var \ (vvar \ state)" where + "the_var G s (LVar ln) =(lvar ln (store s),s)" +| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" +| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" lemma the_var_FVar_simp[simp]: "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 07:55:18 2010 +0200 @@ -425,7 +425,7 @@ lemma poly_exp_eq_zero: "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \ 0)" -apply (simp only: fun_eq add: all_simps [symmetric]) +apply (simp only: fun_eq add: HOL.all_simps [symmetric]) apply (rule arg_cong [where f = All]) apply (rule ext) apply (induct_tac "n") diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Extraction/Euclid.thy Tue Jun 29 07:55:18 2010 +0200 @@ -44,7 +44,7 @@ done lemma prime_eq': "prime (p::nat) = (1 < p \ (\m k. p = m * k \ 1 < m \ m = p))" - by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) + by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) lemma not_prime_ex_mk: assumes n: "Suc 0 < n" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Extraction/Warshall.thy --- a/src/HOL/Extraction/Warshall.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Extraction/Warshall.thy Tue Jun 29 07:55:18 2010 +0200 @@ -38,7 +38,7 @@ "\x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \ r y z = T)" by (induct ys) simp+ -theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \ list_all P xs)" +theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \ P x \ list_all P xs" by (induct xs, simp+, iprover) theorem list_all_lemma: diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Import/HOL/HOL4Base.thy --- a/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 07:55:18 2010 +0200 @@ -3130,7 +3130,7 @@ by (import list EVERY_MEM) lemma EXISTS_MEM: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = (EX e::'a::type. e mem l & P e)" + list_ex P l = (EX e::'a::type. e mem l & P e)" by (import list EXISTS_MEM) lemma MEM_APPEND: "ALL (e::'a::type) (l1::'a::type list) l2::'a::type list. @@ -3138,15 +3138,15 @@ by (import list MEM_APPEND) lemma EXISTS_APPEND: "ALL (P::'a::type => bool) (l1::'a::type list) l2::'a::type list. - list_exists P (l1 @ l2) = (list_exists P l1 | list_exists P l2)" + list_ex P (l1 @ l2) = (list_ex P l1 | list_ex P l2)" by (import list EXISTS_APPEND) lemma NOT_EVERY: "ALL (P::'a::type => bool) l::'a::type list. - (~ list_all P l) = list_exists (Not o P) l" + (~ list_all P l) = list_ex (Not o P) l" by (import list NOT_EVERY) lemma NOT_EXISTS: "ALL (P::'a::type => bool) l::'a::type list. - (~ list_exists P l) = list_all (Not o P) l" + (~ list_ex P l) = list_all (Not o P) l" by (import list NOT_EXISTS) lemma MEM_MAP: "ALL (l::'a::type list) (f::'a::type => 'b::type) x::'b::type. @@ -3220,7 +3220,7 @@ lemma EXISTS_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool) P'::'a::type => bool. l1 = l2 & (ALL x::'a::type. x mem l2 --> P x = P' x) --> - list_exists P l1 = list_exists P' l2" + list_ex P l1 = list_ex P' l2" by (import list EXISTS_CONG) lemma EVERY_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool) @@ -4598,7 +4598,7 @@ SCANR f e (x # l) = f x (hd (SCANR f e l)) # SCANR f e l)" by (import rich_list SCANR) -lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l" +lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l" by (import rich_list IS_EL_DEF) definition AND_EL :: "bool list => bool" where @@ -4608,9 +4608,9 @@ by (import rich_list AND_EL_DEF) definition OR_EL :: "bool list => bool" where - "OR_EL == list_exists I" - -lemma OR_EL_DEF: "OR_EL = list_exists I" + "OR_EL == list_ex I" + +lemma OR_EL_DEF: "OR_EL = list_ex I" by (import rich_list OR_EL_DEF) consts @@ -4937,7 +4937,7 @@ by (import rich_list ALL_EL_MAP) lemma SOME_EL_SNOC: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list. - list_exists P (SNOC x l) = (P x | list_exists P l)" + list_ex P (SNOC x l) = (P x | list_ex P l)" by (import rich_list SOME_EL_SNOC) lemma IS_EL_SNOC: "ALL (y::'a::type) (x::'a::type) l::'a::type list. @@ -5080,11 +5080,11 @@ by (import rich_list ALL_EL_FOLDL) lemma SOME_EL_FOLDR: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = foldr (%x::'a::type. op | (P x)) l False" + list_ex P l = foldr (%x::'a::type. op | (P x)) l False" by (import rich_list SOME_EL_FOLDR) lemma SOME_EL_FOLDL: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l" + list_ex P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l" by (import rich_list SOME_EL_FOLDL) lemma ALL_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list. @@ -5096,11 +5096,11 @@ by (import rich_list ALL_EL_FOLDL_MAP) lemma SOME_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list. - list_exists x xa = foldr op | (map x xa) False" + list_ex x xa = foldr op | (map x xa) False" by (import rich_list SOME_EL_FOLDR_MAP) lemma SOME_EL_FOLDL_MAP: "ALL (x::'a::type => bool) xa::'a::type list. - list_exists x xa = foldl op | False (map x xa)" + list_ex x xa = foldl op | False (map x xa)" by (import rich_list SOME_EL_FOLDL_MAP) lemma FOLDR_FILTER: "ALL (f::'a::type => 'a::type => 'a::type) (e::'a::type) @@ -5132,12 +5132,12 @@ by (import rich_list ASSOC_FOLDL_FLAT) lemma SOME_EL_MAP: "ALL (P::'b::type => bool) (f::'a::type => 'b::type) l::'a::type list. - list_exists P (map f l) = list_exists (P o f) l" + list_ex P (map f l) = list_ex (P o f) l" by (import rich_list SOME_EL_MAP) lemma SOME_EL_DISJ: "ALL (P::'a::type => bool) (Q::'a::type => bool) l::'a::type list. - list_exists (%x::'a::type. P x | Q x) l = - (list_exists P l | list_exists Q l)" + list_ex (%x::'a::type. P x | Q x) l = + (list_ex P l | list_ex Q l)" by (import rich_list SOME_EL_DISJ) lemma IS_EL_FOLDR: "ALL (x::'a::type) xa::'a::type list. @@ -5579,7 +5579,7 @@ by (import rich_list FLAT_FLAT) lemma SOME_EL_REVERSE: "ALL (P::'a::type => bool) l::'a::type list. - list_exists P (rev l) = list_exists P l" + list_ex P (rev l) = list_ex P l" by (import rich_list SOME_EL_REVERSE) lemma ALL_EL_SEG: "ALL (P::'a::type => bool) l::'a::type list. @@ -5621,29 +5621,29 @@ lemma SOME_EL_SEG: "ALL (m::nat) (k::nat) l::'a::type list. m + k <= length l --> - (ALL P::'a::type => bool. list_exists P (SEG m k l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (SEG m k l) --> list_ex P l)" by (import rich_list SOME_EL_SEG) lemma SOME_EL_FIRSTN: "ALL (m::nat) l::'a::type list. m <= length l --> - (ALL P::'a::type => bool. list_exists P (FIRSTN m l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (FIRSTN m l) --> list_ex P l)" by (import rich_list SOME_EL_FIRSTN) lemma SOME_EL_BUTFIRSTN: "ALL (m::nat) l::'a::type list. m <= length l --> (ALL P::'a::type => bool. - list_exists P (BUTFIRSTN m l) --> list_exists P l)" + list_ex P (BUTFIRSTN m l) --> list_ex P l)" by (import rich_list SOME_EL_BUTFIRSTN) lemma SOME_EL_LASTN: "ALL (m::nat) l::'a::type list. m <= length l --> - (ALL P::'a::type => bool. list_exists P (LASTN m l) --> list_exists P l)" + (ALL P::'a::type => bool. list_ex P (LASTN m l) --> list_ex P l)" by (import rich_list SOME_EL_LASTN) lemma SOME_EL_BUTLASTN: "ALL (m::nat) l::'a::type list. m <= length l --> (ALL P::'a::type => bool. - list_exists P (BUTLASTN m l) --> list_exists P l)" + list_ex P (BUTLASTN m l) --> list_ex P l)" by (import rich_list SOME_EL_BUTLASTN) lemma IS_EL_REVERSE: "ALL (x::'a::type) l::'a::type list. x mem rev l = x mem l" @@ -5657,7 +5657,7 @@ n + m <= length l --> (ALL x::'a::type. x mem SEG n m l --> x mem l)" by (import rich_list IS_EL_SEG) -lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l" +lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l" by (import rich_list IS_EL_SOME_EL) lemma IS_EL_FIRSTN: "ALL (x::nat) xa::'a::type list. diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Import/HOL4Compat.thy --- a/src/HOL/Import/HOL4Compat.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Import/HOL4Compat.thy Tue Jun 29 07:55:18 2010 +0200 @@ -6,6 +6,7 @@ imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum begin +abbreviation (input) mem (infixl "mem" 55) where "x mem xs \ List.member xs x" no_notation differentiable (infixl "differentiable" 60) no_notation sums (infixr "sums" 80) @@ -326,8 +327,8 @@ qed qed -lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)" - by simp +lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)" + by (simp add: null_def) definition sum :: "nat list \ nat" where "sum l == foldr (op +) l 0" @@ -347,8 +348,8 @@ lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)" by simp -lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))" - by auto +lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))" + by (simp add: member_def) lemma FILTER: "(!P. filter P [] = []) & (!P h t. filter P (h#t) = (if P h then h#filter P t else filter P t))" @@ -373,15 +374,7 @@ lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))" by simp -consts - list_exists :: "['a \ bool,'a list] \ bool" - -primrec - list_exists_Nil: "list_exists P Nil = False" - list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)" - -lemma list_exists_DEF: "(!P. list_exists P [] = False) & - (!P h t. list_exists P (h#t) = (P h | list_exists P t))" +lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))" by simp consts diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Induct/Term.thy --- a/src/HOL/Induct/Term.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Induct/Term.thy Tue Jun 29 07:55:18 2010 +0200 @@ -13,18 +13,12 @@ text {* \medskip Substitution function on terms *} -consts - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" - subst_term_list :: - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" - -primrec +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" + and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where "subst_term f (Var a) = f a" - "subst_term f (App b ts) = App b (subst_term_list f ts)" - - "subst_term_list f [] = []" - "subst_term_list f (t # ts) = - subst_term f t # subst_term_list f ts" +| "subst_term f (App b ts) = App b (subst_term_list f ts)" +| "subst_term_list f [] = []" +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" text {* \medskip A simple theorem about composition of substitutions *} @@ -41,9 +35,9 @@ lemma assumes var: "!!v. P (Var v)" - and app: "!!f ts. list_all P ts ==> P (App f ts)" + and app: "!!f ts. (\t \ set ts. P t) ==> P (App f ts)" shows term_induct2: "P t" - and "list_all P ts" + and "\t \ set ts. P t" apply (induct t and ts) apply (rule var) apply (rule app) diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Isar_Examples/Nested_Datatype.thy --- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 07:55:18 2010 +0200 @@ -10,17 +10,14 @@ Var 'a | App 'b "('a, 'b) term list" -consts - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" - subst_term_list :: - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and + subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where + "subst_term f (Var a) = f a" +| "subst_term f (App b ts) = App b (subst_term_list f ts)" +| "subst_term_list f [] = []" +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" -primrec (subst) - "subst_term f (Var a) = f a" - "subst_term f (App b ts) = App b (subst_term_list f ts)" - "subst_term_list f [] = []" - "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" - +lemmas subst_simps = subst_term_subst_term_list.simps text {* \medskip A simple lemma about composition of substitutions. @@ -44,13 +41,13 @@ next fix b ts assume "?Q ts" then show "?P (App b ts)" - by (simp only: subst.simps) + by (simp only: subst_simps) next show "?Q []" by simp next fix t ts assume "?P t" "?Q ts" then show "?Q (t # ts)" - by (simp only: subst.simps) + by (simp only: subst_simps) qed qed @@ -59,18 +56,18 @@ theorem term_induct' [case_names Var App]: assumes var: "!!a. P (Var a)" - and app: "!!b ts. list_all P ts ==> P (App b ts)" + and app: "!!b ts. (\t \ set ts. P t) ==> P (App b ts)" shows "P t" proof (induct t) fix a show "P (Var a)" by (rule var) next - fix b t ts assume "list_all P ts" + fix b t ts assume "\t \ set ts. P t" then show "P (App b ts)" by (rule app) next - show "list_all P []" by simp + show "\t \ set []. P t" by simp next - fix t ts assume "P t" "list_all P ts" - then show "list_all P (t # ts)" by simp + fix t ts assume "P t" "\t' \ set ts. P t'" + then show "\t' \ set (t # ts). P t'" by simp qed lemma diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/AssocList.thy Tue Jun 29 07:55:18 2010 +0200 @@ -674,8 +674,8 @@ by (rule mapping_eqI) simp lemma is_empty_Mapping [code]: - "Mapping.is_empty (Mapping xs) \ null xs" - by (cases xs) (simp_all add: is_empty_def) + "Mapping.is_empty (Mapping xs) \ List.null xs" + by (cases xs) (simp_all add: is_empty_def null_def) lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (update k v xs)" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Jun 29 07:55:18 2010 +0200 @@ -122,7 +122,7 @@ next case (insert x xs) then have "\ member (Dlist xs) x" and "P (Dlist xs)" - by (simp_all add: member_def mem_iff) + by (simp_all add: member_def List.member_def) with insrt have "P (insert x (Dlist xs))" . with insert show ?case by (simp add: insert_def distinct_remdups_id) qed @@ -144,7 +144,7 @@ case (Cons x xs) with dxs distinct have "\ member (Dlist xs) x" and "dxs = insert x (Dlist xs)" - by (simp_all add: member_def mem_iff insert_def distinct_remdups_id) + by (simp_all add: member_def List.member_def insert_def distinct_remdups_id) with insert show P . qed qed @@ -205,7 +205,7 @@ lemma is_empty_Set [code]: "Fset.is_empty (Set dxs) \ null dxs" - by (simp add: null_def null_empty member_set) + by (simp add: null_def List.null_def member_set) lemma bot_code [code]: "bot = Set empty" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/Enum.thy Tue Jun 29 07:55:18 2010 +0200 @@ -49,8 +49,8 @@ lemma order_fun [code]: fixes f g :: "'a\enum \ 'b\order" shows "f \ g \ list_all (\x. f x \ g x) enum" - and "f < g \ f \ g \ \ list_all (\x. f x = g x) enum" - by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le) + and "f < g \ f \ g \ list_ex (\x. f x \ g x) enum" + by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le) subsection {* Quantifiers *} @@ -58,8 +58,8 @@ lemma all_code [code]: "(\x. P x) \ list_all P enum" by (simp add: list_all_iff enum_all) -lemma exists_code [code]: "(\x. P x) \ \ list_all (Not o P) enum" - by (simp add: list_all_iff enum_all) +lemma exists_code [code]: "(\x. P x) \ list_ex P enum" + by (simp add: list_ex_iff enum_all) subsection {* Default instances *} diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/Executable_Set.thy Tue Jun 29 07:55:18 2010 +0200 @@ -50,9 +50,9 @@ by simp lemma [code]: - "x \ Set xs \ member xs x" - "x \ Coset xs \ \ member xs x" - by (simp_all add: mem_iff) + "x \ Set xs \ List.member xs x" + "x \ Coset xs \ \ List.member xs x" + by (simp_all add: member_def) definition is_empty :: "'a set \ bool" where [simp]: "is_empty A \ A = {}" @@ -85,8 +85,8 @@ *} lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" - by (simp add: empty_null) + "is_empty (Set xs) \ List.null xs" + by (simp add: null_def) lemma empty_Set [code]: "empty = Set []" @@ -112,11 +112,11 @@ lemma Ball_Set [code]: "Ball (Set xs) P \ list_all P xs" - by (simp add: ball_set) + by (simp add: list_all_iff) lemma Bex_Set [code]: "Bex (Set xs) P \ list_ex P xs" - by (simp add: bex_set) + by (simp add: list_ex_iff) lemma card_Set [code]: "card (Set xs) = length (remdups xs)" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/Fset.thy Tue Jun 29 07:55:18 2010 +0200 @@ -51,7 +51,7 @@ lemma member_code [code]: "member (Set xs) = List.member xs" "member (Coset xs) = Not \ List.member xs" - by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def) + by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def) lemma member_image_UNIV [simp]: "member ` UNIV = UNIV" @@ -141,7 +141,7 @@ [simp]: "is_empty A \ More_Set.is_empty (member A)" lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" + "is_empty (Set xs) \ List.null xs" by (simp add: is_empty_set) lemma empty_Set [code]: @@ -188,14 +188,14 @@ lemma forall_Set [code]: "forall P (Set xs) \ list_all P xs" - by (simp add: Set_def ball_set) + by (simp add: Set_def list_all_iff) definition exists :: "('a \ bool) \ 'a fset \ bool" where [simp]: "exists P A \ Bex (member A) P" lemma exists_Set [code]: "exists P (Set xs) \ list_ex P xs" - by (simp add: Set_def bex_set) + by (simp add: Set_def list_ex_iff) definition card :: "'a fset \ nat" where [simp]: "card A = Finite_Set.card (member A)" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/More_Set.thy Tue Jun 29 07:55:18 2010 +0200 @@ -37,16 +37,8 @@ subsection {* Basic set operations *} lemma is_empty_set: - "is_empty (set xs) \ null xs" - by (simp add: is_empty_def null_empty) - -lemma ball_set: - "(\x\set xs. P x) \ list_all P xs" - by (rule list_ball_code) - -lemma bex_set: - "(\x\set xs. P x) \ list_ex P xs" - by (rule list_bex_code) + "is_empty (set xs) \ List.null xs" + by (simp add: is_empty_def null_def) lemma empty_set: "{} = set []" diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/Univ_Poly.thy Tue Jun 29 07:55:18 2010 +0200 @@ -407,7 +407,7 @@ lemma (in idom) poly_exp_eq_zero[simp]: "(poly (p %^ n) = poly []) = (poly p = poly [] & n \ 0)" -apply (simp only: fun_eq add: all_simps [symmetric]) +apply (simp only: fun_eq add: HOL.all_simps [symmetric]) apply (rule arg_cong [where f = All]) apply (rule ext) apply (induct n) diff -r 32ad67684ee7 -r 165cd386288d src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Tue Jun 29 07:55:18 2010 +0200 @@ -228,7 +228,7 @@ val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ - @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); + @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); val real_abs_thms1 = @{lemma "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and diff -r 32ad67684ee7 -r 165cd386288d src/HOL/List.thy --- a/src/HOL/List.thy Tue Jun 29 02:18:08 2010 +0100 +++ b/src/HOL/List.thy Tue Jun 29 07:55:18 2010 +0200 @@ -2352,6 +2352,22 @@ case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) qed +lemma rev_foldl_cons [code]: + "rev xs = foldl (\xs x. x # xs) [] xs" +proof (induct xs) + case Nil then show ?case by simp +next + case Cons + { + fix x xs ys + have "foldl (\xs x. x # xs) ys xs @ [x] + = foldl (\xs x. x # xs) (ys @ [x]) xs" + by (induct xs arbitrary: ys) auto + } + note aux = this + show ?case by (induct xs) (auto simp add: Cons aux) +qed + text{* The ``First Duality Theorem'' in Bird \& Wadler: *} @@ -2509,120 +2525,6 @@ by (simp add: sup_commute) -subsubsection {* List summation: @{const listsum} and @{text"\"}*} - -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" -by (induct xs) (simp_all add:add_assoc) - -lemma listsum_rev [simp]: - fixes xs :: "'a\comm_monoid_add list" - shows "listsum (rev xs) = listsum xs" -by (induct xs) (simp_all add:add_ac) - -lemma listsum_map_remove1: -fixes f :: "'a \ ('b::comm_monoid_add)" -shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" -by (induct xs)(auto simp add:add_ac) - -lemma list_size_conv_listsum: - "list_size f xs = listsum (map f xs) + size xs" -by(induct xs) auto - -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" -by (induct xs) auto - -lemma length_concat: "length (concat xss) = listsum (map length xss)" -by (induct xss) simp_all - -lemma listsum_map_filter: - fixes f :: "'a \ 'b \ comm_monoid_add" - assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" - shows "listsum (map f (filter P xs)) = listsum (map f xs)" -using assms by (induct xs) auto - -text{* For efficient code generation --- - @{const listsum} is not tail recursive but @{const foldl} is. *} -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" -by(simp add:listsum_foldr foldl_foldr1) - -lemma distinct_listsum_conv_Setsum: - "distinct xs \ listsum xs = Setsum(set xs)" -by (induct xs) simp_all - -lemma listsum_eq_0_nat_iff_nat[simp]: - "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" -by(simp add: listsum) - -lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" -apply(induct ns arbitrary: k) - apply simp -apply(fastsimp simp add:nth_Cons split: nat.split) -done - -lemma listsum_update_nat: "k - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" -apply(induct ns arbitrary:k) - apply (auto split:nat.split) -apply(drule elem_le_listsum_nat) -apply arith -done - -text{* Some syntactic sugar for summing a function over a list: *} - -syntax - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) -syntax (xsymbols) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) - -translations -- {* Beware of argument permutation! *} - "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" - "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" - -lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" - by (induct xs) (simp_all add: left_distrib) - -lemma listsum_0 [simp]: "(\x\xs. 0) = 0" - by (induct xs) (simp_all add: left_distrib) - -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} -lemma uminus_listsum_map: - fixes f :: "'a \ 'b\ab_group_add" - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" -by (induct xs) simp_all - -lemma listsum_addf: - fixes f g :: "'a \ 'b::comm_monoid_add" - shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" -by (induct xs) (simp_all add: algebra_simps) - -lemma listsum_subtractf: - fixes f g :: "'a \ 'b::ab_group_add" - shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" -by (induct xs) simp_all - -lemma listsum_const_mult: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. c * f x) = c * (\x\xs. f x)" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_mult_const: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. f x * c) = (\x\xs. f x) * c" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_abs: - fixes xs :: "'a::ordered_ab_group_add_abs list" - shows "\listsum xs\ \ listsum (map abs xs)" -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) - -lemma listsum_mono: - fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" - shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" -by (induct xs, simp, simp add: add_mono) - - subsubsection {* @{text upt} *} lemma upt_rec[code]: "[i.."}*} + +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" +by (induct xs) (simp_all add:add_assoc) + +lemma listsum_rev [simp]: + fixes xs :: "'a\comm_monoid_add list" + shows "listsum (rev xs) = listsum xs" +by (induct xs) (simp_all add:add_ac) + +lemma listsum_map_remove1: +fixes f :: "'a \ ('b::comm_monoid_add)" +shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))" +by (induct xs)(auto simp add:add_ac) + +lemma list_size_conv_listsum: + "list_size f xs = listsum (map f xs) + size xs" +by(induct xs) auto + +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" +by (induct xs) auto + +lemma length_concat: "length (concat xss) = listsum (map length xss)" +by (induct xss) simp_all + +lemma listsum_map_filter: + fixes f :: "'a \ 'b \ comm_monoid_add" + assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" + shows "listsum (map f (filter P xs)) = listsum (map f xs)" +using assms by (induct xs) auto + +text{* For efficient code generation --- + @{const listsum} is not tail recursive but @{const foldl} is. *} +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" +by(simp add:listsum_foldr foldl_foldr1) + +lemma distinct_listsum_conv_Setsum: + "distinct xs \ listsum xs = Setsum(set xs)" +by (induct xs) simp_all + +lemma listsum_eq_0_nat_iff_nat[simp]: + "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" +by(simp add: listsum) + +lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" +apply(induct ns arbitrary: k) + apply simp +apply(fastsimp simp add:nth_Cons split: nat.split) +done + +lemma listsum_update_nat: "k + listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" +apply(induct ns arbitrary:k) + apply (auto split:nat.split) +apply(drule elem_le_listsum_nat) +apply arith +done + +text{* Some syntactic sugar for summing a function over a list: *} + +syntax + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) +syntax (xsymbols) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) +syntax (HTML output) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) + +translations -- {* Beware of argument permutation! *} + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" + "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" + +lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" + by (induct xs) (simp_all add: left_distrib) + +lemma listsum_0 [simp]: "(\x\xs. 0) = 0" + by (induct xs) (simp_all add: left_distrib) + +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} +lemma uminus_listsum_map: + fixes f :: "'a \ 'b\ab_group_add" + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" +by (induct xs) simp_all + +lemma listsum_addf: + fixes f g :: "'a \ 'b::comm_monoid_add" + shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" +by (induct xs) (simp_all add: algebra_simps) + +lemma listsum_subtractf: + fixes f g :: "'a \ 'b::ab_group_add" + shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" +by (induct xs) simp_all + +lemma listsum_const_mult: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. c * f x) = c * (\x\xs. f x)" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_mult_const: + fixes f :: "'a \ 'b::semiring_0" + shows "(\x\xs. f x * c) = (\x\xs. f x) * c" +by (induct xs, simp_all add: algebra_simps) + +lemma listsum_abs: + fixes xs :: "'a::ordered_ab_group_add_abs list" + shows "\listsum xs\ \ listsum (map abs xs)" +by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) + +lemma listsum_mono: + fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" + shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)" +by (induct xs, simp, simp add: add_mono) + +lemma listsum_distinct_conv_setsum_set: + "distinct xs \ listsum (map f xs) = setsum f (set xs)" + by (induct xs) simp_all + +lemma interv_listsum_conv_setsum_set_nat: + "listsum (map f [m.. i = 0 ..< length xs. xs ! i)" + using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) + + subsubsection {* @{const insert} *} lemma in_set_insert [simp]: @@ -4513,9 +4546,266 @@ *) -subsection {* Code generator *} - -subsubsection {* Setup *} +subsection {* Code generation *} + +subsubsection {* Counterparts for set-related operations *} + +definition member :: "'a list \ 'a \ bool" where + [code_post]: "member xs x \ x \ set xs" + +text {* + Only use @{text member} for generating executable code. Otherwise use + @{prop "x \ set xs"} instead --- it is much easier to reason about. +*} + +lemma member_set: + "member = set" + by (simp add: expand_fun_eq member_def mem_def) + +lemma member_rec [code]: + "member (x # xs) y \ x = y \ member xs y" + "member [] y \ False" + by (auto simp add: member_def) + +lemma in_set_member [code_unfold]: + "x \ set xs \ member xs x" + by (simp add: member_def) + +declare INFI_def [code_unfold] +declare SUPR_def [code_unfold] + +declare set_map [symmetric, code_unfold] + +definition list_all :: "('a \ bool) \ 'a list \ bool" where + list_all_iff [code_post]: "list_all P xs \ (\x \ set xs. P x)" + +definition list_ex :: "('a \ bool) \ 'a list \ bool" where + list_ex_iff [code_post]: "list_ex P xs \ (\x \ set xs. P x)" + +text {* + Usually you should prefer @{text "\x\set xs"} and @{text "\x\set xs"} + over @{const list_all} and @{const list_ex} in specifications. +*} + +lemma list_all_simps [simp, code]: + "list_all P (x # xs) \ P x \ list_all P xs" + "list_all P [] \ True" + by (simp_all add: list_all_iff) + +lemma list_ex_simps [simp, code]: + "list_ex P (x # xs) \ P x \ list_ex P xs" + "list_ex P [] \ False" + by (simp_all add: list_ex_iff) + +lemma Ball_set_list_all [code_unfold]: + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set_list_ex [code_unfold]: + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_append [simp]: + "list_all P (xs @ ys) \ list_all P xs \ list_all P ys" + by (auto simp add: list_all_iff) + +lemma list_ex_append [simp]: + "list_ex P (xs @ ys) \ list_ex P xs \ list_ex P ys" + by (auto simp add: list_ex_iff) + +lemma list_all_rev [simp]: + "list_all P (rev xs) \ list_all P xs" + by (simp add: list_all_iff) + +lemma list_ex_rev [simp]: + "list_ex P (rev xs) \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma list_all_length: + "list_all P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_all_iff set_conv_nth) + +lemma list_ex_length: + "list_ex P xs \ (\n < length xs. P (xs ! n))" + by (auto simp add: list_ex_iff set_conv_nth) + +lemma list_all_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_all f xs = list_all g ys" + by (simp add: list_all_iff) + +lemma list_any_cong [fundef_cong]: + "xs = ys \ (\x. x \ set ys \ f x = g x) \ list_ex f xs = list_ex g ys" + by (simp add: list_ex_iff) + +text {* Bounded quantification and summation over nats. *} + +lemma atMost_upto [code_unfold]: + "{..n} = set [0..mnat. P m) \ (\m \ {0..mnat. P m) \ (\m \ {0..m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma ex_nat_less [code_unfold]: + "(\m\n\nat. P m) \ (\m \ {0..n}. P m)" + by auto + +lemma setsum_set_upt_conv_listsum_nat [code_unfold]: + "setsum f (set [m.. bool" where + [code_post]: "null xs \ xs = []" + +text {* + Efficient emptyness check is implemented by @{const null}. +*} + +lemma null_rec [code]: + "null (x # xs) \ False" + "null [] \ True" + by (simp_all add: null_def) + +lemma eq_Nil_null [code_unfold]: + "xs = [] \ null xs" + by (simp add: null_def) + +lemma equal_Nil_null [code_unfold]: + "eq_class.eq xs [] \ null xs" + by (simp add: eq eq_Nil_null) + +definition maps :: "('a \ 'b list) \ 'a list \ 'b list" where + [code_post]: "maps f xs = concat (map f xs)" + +definition map_filter :: "('a \ 'b option) \ 'a list \ 'b list" where + [code_post]: "map_filter f xs = map (the \ f) (filter (\x. f x \ None) xs)" + +text {* + Operations @{const maps} and @{const map_filter} avoid + intermediate lists on execution -- do not use for proving. +*} + +lemma maps_simps [code]: + "maps f (x # xs) = f x @ maps f xs" + "maps f [] = []" + by (simp_all add: maps_def) + +lemma map_filter_simps [code]: + "map_filter f (x # xs) = (case f x of None \ map_filter f xs | Some y \ y # map_filter f xs)" + "map_filter f [] = []" + by (simp_all add: map_filter_def split: option.split) + +lemma concat_map_maps [code_unfold]: + "concat (map f xs) = maps f xs" + by (simp add: maps_def) + +lemma map_filter_map_filter [code_unfold]: + "map f (filter P xs) = map_filter (\x. if P x then Some (f x) else None) xs" + by (simp add: map_filter_def) + +text {* Optimized code for @{text"\i\{a..b::int}"} and @{text"\n:{a.."}. *} + +definition all_interval_nat :: "(nat \ bool) \ nat \ nat \ bool" where + "all_interval_nat P i j \ (\n \ {i.. i \ j \ P i \ all_interval_nat P (Suc i) j" +proof - + have *: "\n. P i \ \n\{Suc i.. i \ n \ n < j \ P n" + proof - + fix n + assume "P i" "\n\{Suc i.. n" "n < j" + then show "P n" by (cases "n = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_nat_def intro: *) +qed + +lemma list_all_iff_all_interval_nat [code_unfold]: + "list_all P [i.. all_interval_nat P i j" + by (simp add: list_all_iff all_interval_nat_def) + +lemma list_ex_iff_not_all_inverval_nat [code_unfold]: + "list_ex P [i.. \ (all_interval_nat (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_nat_def) + +definition all_interval_int :: "(int \ bool) \ int \ int \ bool" where + "all_interval_int P i j \ (\k \ {i..j}. P k)" + +lemma [code]: + "all_interval_int P i j \ i > j \ P i \ all_interval_int P (i + 1) j" +proof - + have *: "\k. P i \ \k\{i+1..j}. P k \ i \ k \ k \ j \ P k" + proof - + fix k + assume "P i" "\k\{i+1..j}. P k" "i \ k" "k \ j" + then show "P k" by (cases "k = i") simp_all + qed + show ?thesis by (auto simp add: all_interval_int_def intro: *) +qed + +lemma list_all_iff_all_interval_int [code_unfold]: + "list_all P [i..j] \ all_interval_int P i j" + by (simp add: list_all_iff all_interval_int_def) + +lemma list_ex_iff_not_all_inverval_int [code_unfold]: + "list_ex P [i..j] \ \ (all_interval_int (Not \ P) i j)" + by (simp add: list_ex_iff all_interval_int_def) + +hide_const (open) member null maps map_filter all_interval_nat all_interval_int + + +subsubsection {* Pretty lists *} use "Tools/list_code.ML" @@ -4578,374 +4868,6 @@ *} -subsubsection {* Generation of efficient code *} - -definition member :: "'a list \