# HG changeset patch # User haftmann # Date 1260194053 -3600 # Node ID bb37c95f0b8eb954850e3285206edf1cc5e2ae92 # Parent e820ed4bfd9415ddca32ff6848e553996cb14d15# Parent 2573c794034c32c4dcf9b9ebe763069d7d2f66b3 merged diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Dec 07 14:54:13 2009 +0100 @@ -12,10 +12,10 @@ structure Boogie_Loader: BOOGIE_LOADER = struct -fun log verbose text args thy = - if verbose - then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); thy) - else thy +fun log verbose text args x = + if verbose andalso not (null args) + then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); x) + else x val isabelle_name = let @@ -35,7 +35,7 @@ fun label_name line col = "L_" ^ string_of_int line ^ "_" ^ string_of_int col -datatype attribute_value = StringValue of string | TermValue of Term.term +datatype attribute_value = StringValue of string | TermValue of term @@ -51,27 +51,28 @@ else NONE end + fun log_new bname name = bname ^ " (as " ^ name ^ ")" + fun log_ex bname name = "[" ^ bname ^ " has already been declared as " ^ + name ^ "]" + fun declare (name, arity) thy = let val isa_name = isabelle_name name in (case lookup_type_name thy isa_name arity of - SOME type_name => ((type_name, false), thy) + SOME type_name => (((name, type_name), log_ex name type_name), thy) | NONE => let val args = Name.variant_list [] (replicate arity "'") val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy val type_name = fst (Term.dest_Type T) - in ((type_name, true), thy') end) + in (((name, type_name), log_new name type_name), thy') end) end - - fun type_names ((name, _), (new_name, new)) = - if new then SOME (new_name ^ " (was " ^ name ^ ")") else NONE in fun declare_types verbose tys = - fold_map declare tys #-> (fn tds => - log verbose "Declared types:" (map_filter type_names (tys ~~ tds)) #> - rpair (Symtab.make (map fst tys ~~ map fst tds))) + fold_map declare tys #>> split_list #-> (fn (tds, logs) => + log verbose "Declared types:" logs #> + rpair (Symtab.make tds)) end @@ -146,23 +147,26 @@ else NONE end - fun declare (name, ((Ts, T), atts)) thy = - let val isa_name = isabelle_name name and U = Ts ---> T - in - (case lookup_const thy isa_name U of - SOME t => (((name, t), false), thy) - | NONE => - (case maybe_builtin U atts of - SOME t => (((name, t), false), thy) - | NONE => - thy - |> Sign.declare_const ((Binding.name isa_name, U), - mk_syntax name (length Ts)) - |> apfst (rpair true o pair name))) - end + fun log_term thy t = Syntax.string_of_term_global thy t + fun log_new thy name t = name ^ " (as " ^ log_term thy t ^ ")" + fun log_ex thy name t = "[" ^ name ^ " has already been declared as " ^ + log_term thy t ^ "]" + fun log_builtin thy name t = "[" ^ name ^ " has been identified as " ^ + log_term thy t ^ "]" - fun new_names ((name, t), new) = - if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE + fun declare' name isa_name T arity atts thy = + (case lookup_const thy isa_name T of + SOME t => (((name, t), log_ex thy name t), thy) + | NONE => + (case maybe_builtin T atts of + SOME t => (((name, t), log_builtin thy name t), thy) + | NONE => + thy + |> Sign.declare_const ((Binding.name isa_name, T), + mk_syntax name arity) + |> (fn (t, thy') => (((name, t), log_new thy' name t), thy')))) + fun declare (name, ((Ts, T), atts)) = + declare' name (isabelle_name name) (Ts ---> T) (length Ts) atts fun uniques fns fds = let @@ -182,9 +186,9 @@ end in fun declare_functions verbose fns = - fold_map declare fns #-> (fn fds => - log verbose "Declared constants:" (map_filter new_names fds) #> - rpair (` (uniques fns) (Symtab.make (map fst fds)))) + fold_map declare fns #>> split_list #-> (fn (fds, logs) => + log verbose "Loaded constants:" logs #> + rpair (` (uniques fns) (Symtab.make fds))) end @@ -194,17 +198,41 @@ let fun mk_name idx = "axiom_" ^ string_of_int (idx + 1) in map_index (fn (idx, t) => (mk_name idx, HOLogic.mk_Trueprop t)) axs end - fun only_new_boogie_axioms thy = - let val baxs = map Thm.prop_of (Boogie_Axioms.get (ProofContext.init thy)) - in filter_out (member (op aconv) baxs o snd) end + datatype kind = Unused of thm | Used of thm | New of string + + fun mark (name, t) axs = + (case Termtab.lookup axs t of + SOME (Unused thm) => Termtab.update (t, Used thm) axs + | NONE => Termtab.update (t, New name) axs + | SOME _ => axs) + + val sort_fst_str = sort (prod_ord fast_string_ord (K EQUAL)) + fun split_list_kind thy axs = + let + fun split (_, Used thm) (used, new) = (thm :: used, new) + | split (t, New name) (used, new) = (used, (name, t) :: new) + | split (t, Unused thm) (used, new) = + (warning (Pretty.str_of + (Pretty.big_list "This background axiom has not been loaded:" + [Display.pretty_thm_global thy thm])); + (used, new)) + in apsnd sort_fst_str (fold split axs ([], [])) end + + fun mark_axioms thy axs = + Boogie_Axioms.get (ProofContext.init thy) + |> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm)) + |> fold mark axs + |> split_list_kind thy o Termtab.dest in fun add_axioms verbose axs thy = - let val axs' = only_new_boogie_axioms thy (name_axioms axs) + let val (used, new) = mark_axioms thy (name_axioms axs) in thy - |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) axs') + |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new) |-> Context.theory_map o fold Boogie_Axioms.add_thm - |> log verbose "The following axioms were added:" (map fst axs') + |> log verbose "The following axioms were added:" (map fst new) + |> (fn thy' => log verbose "The following axioms already existed:" + (map (Display.string_of_thm_global thy') used) thy') |> Context.theory_map (fn context => fold Split_VC_SMT_Rules.add_thm (Boogie_Axioms.get (Context.proof_of context)) context) end diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/IsaMakefile Mon Dec 07 14:54:13 2009 +0100 @@ -369,7 +369,6 @@ Library/Sum_Of_Squares/sos_wrapper.ML \ Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \ Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy \ - Library/Crude_Executable_Set.thy \ Library/Infinite_Set.thy Library/FuncSet.thy \ Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \ Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \ diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/Library/Crude_Executable_Set.thy --- a/src/HOL/Library/Crude_Executable_Set.thy Mon Dec 07 11:48:40 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,259 +0,0 @@ -(* Title: HOL/Library/Crude_Executable_Set.thy - Author: Florian Haftmann, TU Muenchen -*) - -header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} - -theory Crude_Executable_Set -imports List_Set -begin - -declare mem_def [code del] -declare Collect_def [code del] -declare insert_code [code del] -declare vimage_code [code del] - -subsection {* Set representation *} - -setup {* - Code.add_type_cmd "set" -*} - -definition Set :: "'a list \ 'a set" where - [simp]: "Set = set" - -definition Coset :: "'a list \ 'a set" where - [simp]: "Coset xs = - set xs" - -setup {* - Code.add_signature_cmd ("Set", "'a list \ 'a set") - #> Code.add_signature_cmd ("Coset", "'a list \ 'a set") - #> Code.add_signature_cmd ("set", "'a list \ 'a set") - #> Code.add_signature_cmd ("op \", "'a \ 'a set \ bool") -*} - -code_datatype Set Coset - - -subsection {* Basic operations *} - -lemma [code]: - "set xs = Set (remdups xs)" - by simp - -lemma [code]: - "x \ Set xs \ member x xs" - "x \ Coset xs \ \ member x xs" - by (simp_all add: mem_iff) - -definition is_empty :: "'a set \ bool" where - [simp]: "is_empty A \ A = {}" - -lemma [code_inline]: - "A = {} \ is_empty A" - by simp - -definition empty :: "'a set" where - [simp]: "empty = {}" - -lemma [code_inline]: - "{} = empty" - by simp - -setup {* - Code.add_signature_cmd ("is_empty", "'a set \ bool") - #> Code.add_signature_cmd ("empty", "'a set") - #> Code.add_signature_cmd ("insert", "'a \ 'a set \ 'a set") - #> Code.add_signature_cmd ("List_Set.remove", "'a \ 'a set \ 'a set") - #> Code.add_signature_cmd ("image", "('a \ 'b) \ 'a set \ 'b set") - #> Code.add_signature_cmd ("List_Set.project", "('a \ bool) \ 'a set \ 'a set") - #> Code.add_signature_cmd ("Ball", "'a set \ ('a \ bool) \ bool") - #> Code.add_signature_cmd ("Bex", "'a set \ ('a \ bool) \ bool") - #> Code.add_signature_cmd ("card", "'a set \ nat") -*} - -lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" - by (simp add: empty_null) - -lemma empty_Set [code]: - "empty = Set []" - by simp - -lemma insert_Set [code]: - "insert x (Set xs) = Set (List_Set.insert x xs)" - "insert x (Coset xs) = Coset (remove_all x xs)" - by (simp_all add: insert_set insert_set_compl) - -lemma remove_Set [code]: - "remove x (Set xs) = Set (remove_all x xs)" - "remove x (Coset xs) = Coset (List_Set.insert x xs)" - by (simp_all add:remove_set remove_set_compl) - -lemma image_Set [code]: - "image f (Set xs) = Set (remdups (map f xs))" - by simp - -lemma project_Set [code]: - "project P (Set xs) = Set (filter P xs)" - by (simp add: project_set) - -lemma Ball_Set [code]: - "Ball (Set xs) P \ list_all P xs" - by (simp add: ball_set) - -lemma Bex_Set [code]: - "Bex (Set xs) P \ list_ex P xs" - by (simp add: bex_set) - -lemma card_Set [code]: - "card (Set xs) = length (remdups xs)" -proof - - have "card (set (remdups xs)) = length (remdups xs)" - by (rule distinct_card) simp - then show ?thesis by simp -qed - - -subsection {* Derived operations *} - -definition set_eq :: "'a set \ 'a set \ bool" where - [simp]: "set_eq = op =" - -lemma [code_inline]: - "op = = set_eq" - by simp - -definition subset_eq :: "'a set \ 'a set \ bool" where - [simp]: "subset_eq = op \" - -lemma [code_inline]: - "op \ = subset_eq" - by simp - -definition subset :: "'a set \ 'a set \ bool" where - [simp]: "subset = op \" - -lemma [code_inline]: - "op \ = subset" - by simp - -setup {* - Code.add_signature_cmd ("set_eq", "'a set \ 'a set \ bool") - #> Code.add_signature_cmd ("subset_eq", "'a set \ 'a set \ bool") - #> Code.add_signature_cmd ("subset", "'a set \ 'a set \ bool") -*} - -lemma set_eq_subset_eq [code]: - "set_eq A B \ subset_eq A B \ subset_eq B A" - by auto - -lemma subset_eq_forall [code]: - "subset_eq A B \ (\x\A. x \ B)" - by (simp add: subset_eq) - -lemma subset_subset_eq [code]: - "subset A B \ subset_eq A B \ \ subset_eq B A" - by (simp add: subset) - - -subsection {* Functorial operations *} - -definition inter :: "'a set \ 'a set \ 'a set" where - [simp]: "inter = op \" - -lemma [code_inline]: - "op \ = inter" - by simp - -definition subtract :: "'a set \ 'a set \ 'a set" where - [simp]: "subtract A B = B - A" - -lemma [code_inline]: - "B - A = subtract A B" - by simp - -definition union :: "'a set \ 'a set \ 'a set" where - [simp]: "union = op \" - -lemma [code_inline]: - "op \ = union" - by simp - -definition Inf :: "'a::complete_lattice set \ 'a" where - [simp]: "Inf = Complete_Lattice.Inf" - -lemma [code_inline]: - "Complete_Lattice.Inf = Inf" - by simp - -definition Sup :: "'a::complete_lattice set \ 'a" where - [simp]: "Sup = Complete_Lattice.Sup" - -lemma [code_inline]: - "Complete_Lattice.Sup = Sup" - by simp - -definition Inter :: "'a set set \ 'a set" where - [simp]: "Inter = Inf" - -lemma [code_inline]: - "Inf = Inter" - by simp - -definition Union :: "'a set set \ 'a set" where - [simp]: "Union = Sup" - -lemma [code_inline]: - "Sup = Union" - by simp - -setup {* - Code.add_signature_cmd ("inter", "'a set \ 'a set \ 'a set") - #> Code.add_signature_cmd ("subtract", "'a set \ 'a set \ 'a set") - #> Code.add_signature_cmd ("union", "'a set \ 'a set \ 'a set") - #> Code.add_signature_cmd ("Inf", "'a set \ 'a") - #> Code.add_signature_cmd ("Sup", "'a set \ 'a") - #> Code.add_signature_cmd ("Inter", "'a set set \ 'a set") - #> Code.add_signature_cmd ("Union", "'a set set \ 'a set") -*} - -lemma inter_project [code]: - "inter A (Set xs) = Set (List.filter (\x. x \ A) xs)" - "inter A (Coset xs) = foldl (\A x. remove x A) A xs" - by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) - -lemma subtract_remove [code]: - "subtract (Set xs) A = foldl (\A x. remove x A) A xs" - "subtract (Coset xs) A = Set (List.filter (\x. x \ A) xs)" - by (auto simp add: minus_set) - -lemma union_insert [code]: - "union (Set xs) A = foldl (\A x. insert x A) A xs" - "union (Coset xs) A = Coset (List.filter (\x. x \ A) xs)" - by (auto simp add: union_set) - -lemma Inf_inf [code]: - "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" - "Inf (Coset []) = (bot :: 'a::complete_lattice)" - by (simp_all add: Inf_UNIV Inf_set_fold) - -lemma Sup_sup [code]: - "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" - "Sup (Coset []) = (top :: 'a::complete_lattice)" - by (simp_all add: Sup_UNIV Sup_set_fold) - -lemma Inter_inter [code]: - "Inter (Set xs) = foldl inter (Coset []) xs" - "Inter (Coset []) = empty" - unfolding Inter_def Inf_inf by simp_all - -lemma Union_union [code]: - "Union (Set xs) = foldl union empty xs" - "Union (Coset []) = Coset []" - unfolding Union_def Sup_sup by simp_all - -hide (open) const is_empty empty remove - set_eq subset_eq subset inter union subtract Inf Sup Inter Union - -end diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/Library/Executable_Set.thy Mon Dec 07 14:54:13 2009 +0100 @@ -1,103 +1,271 @@ (* Title: HOL/Library/Executable_Set.thy Author: Stefan Berghofer, TU Muenchen + Author: Florian Haftmann, TU Muenchen *) -header {* Implementation of finite sets by lists *} +header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} theory Executable_Set -imports Main Fset SML_Quickcheck +imports List_Set begin -subsection {* Preprocessor setup *} +declare mem_def [code del] +declare Collect_def [code del] +declare insert_code [code del] +declare vimage_code [code del] + +subsection {* Set representation *} + +setup {* + Code.add_type_cmd "set" +*} + +definition Set :: "'a list \ 'a set" where + [simp]: "Set = set" + +definition Coset :: "'a list \ 'a set" where + [simp]: "Coset xs = - set xs" + +setup {* + Code.add_signature_cmd ("Set", "'a list \ 'a set") + #> Code.add_signature_cmd ("Coset", "'a list \ 'a set") + #> Code.add_signature_cmd ("set", "'a list \ 'a set") + #> Code.add_signature_cmd ("op \", "'a \ 'a set \ bool") +*} + +code_datatype Set Coset -declare member [code] +consts_code + Coset ("\Coset") + Set ("\Set") +attach {* + datatype 'a set = Set of 'a list | Coset of 'a list; +*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *} + + +subsection {* Basic operations *} + +lemma [code]: + "set xs = Set (remdups xs)" + by simp + +lemma [code]: + "x \ Set xs \ member x xs" + "x \ Coset xs \ \ member x xs" + by (simp_all add: mem_iff) + +definition is_empty :: "'a set \ bool" where + [simp]: "is_empty A \ A = {}" + +lemma [code_unfold]: + "A = {} \ is_empty A" + by simp definition empty :: "'a set" where - "empty = {}" + [simp]: "empty = {}" + +lemma [code_unfold]: + "{} = empty" + by simp + +lemma [code_unfold, code_inline del]: + "empty = Set []" + by simp -- {* Otherwise @{text \}-expansion produces funny things. *} + +setup {* + Code.add_signature_cmd ("is_empty", "'a set \ bool") + #> Code.add_signature_cmd ("empty", "'a set") + #> Code.add_signature_cmd ("insert", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("List_Set.remove", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("image", "('a \ 'b) \ 'a set \ 'b set") + #> Code.add_signature_cmd ("List_Set.project", "('a \ bool) \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Ball", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("Bex", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("card", "'a set \ nat") +*} + +lemma is_empty_Set [code]: + "is_empty (Set xs) \ null xs" + by (simp add: empty_null) + +lemma empty_Set [code]: + "empty = Set []" + by simp + +lemma insert_Set [code]: + "insert x (Set xs) = Set (List_Set.insert x xs)" + "insert x (Coset xs) = Coset (remove_all x xs)" + by (simp_all add: insert_set insert_set_compl) + +lemma remove_Set [code]: + "remove x (Set xs) = Set (remove_all x xs)" + "remove x (Coset xs) = Coset (List_Set.insert x xs)" + by (simp_all add:remove_set remove_set_compl) + +lemma image_Set [code]: + "image f (Set xs) = Set (remdups (map f xs))" + by simp + +lemma project_Set [code]: + "project P (Set xs) = Set (filter P xs)" + by (simp add: project_set) + +lemma Ball_Set [code]: + "Ball (Set xs) P \ list_all P xs" + by (simp add: ball_set) -declare empty_def [symmetric, code_unfold] +lemma Bex_Set [code]: + "Bex (Set xs) P \ list_ex P xs" + by (simp add: bex_set) + +lemma card_Set [code]: + "card (Set xs) = length (remdups xs)" +proof - + have "card (set (remdups xs)) = length (remdups xs)" + by (rule distinct_card) simp + then show ?thesis by simp +qed + + +subsection {* Derived operations *} + +definition set_eq :: "'a set \ 'a set \ bool" where + [simp]: "set_eq = op =" + +lemma [code_unfold]: + "op = = set_eq" + by simp + +definition subset_eq :: "'a set \ 'a set \ bool" where + [simp]: "subset_eq = op \" + +lemma [code_unfold]: + "op \ = subset_eq" + by simp + +definition subset :: "'a set \ 'a set \ bool" where + [simp]: "subset = op \" + +lemma [code_unfold]: + "op \ = subset" + by simp + +setup {* + Code.add_signature_cmd ("set_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset", "'a set \ 'a set \ bool") +*} + +lemma set_eq_subset_eq [code]: + "set_eq A B \ subset_eq A B \ subset_eq B A" + by auto + +lemma subset_eq_forall [code]: + "subset_eq A B \ (\x\A. x \ B)" + by (simp add: subset_eq) + +lemma subset_subset_eq [code]: + "subset A B \ subset_eq A B \ \ subset_eq B A" + by (simp add: subset) + + +subsection {* Functorial operations *} definition inter :: "'a set \ 'a set \ 'a set" where - "inter = op \" + [simp]: "inter = op \" + +lemma [code_unfold]: + "op \ = inter" + by simp -declare inter_def [symmetric, code_unfold] +definition subtract :: "'a set \ 'a set \ 'a set" where + [simp]: "subtract A B = B - A" + +lemma [code_unfold]: + "B - A = subtract A B" + by simp definition union :: "'a set \ 'a set \ 'a set" where - "union = op \" - -declare union_def [symmetric, code_unfold] + [simp]: "union = op \" -definition subset :: "'a set \ 'a set \ bool" where - "subset = op \" +lemma [code_unfold]: + "op \ = union" + by simp -declare subset_def [symmetric, code_unfold] - -lemma [code]: - "subset A B \ (\x\A. x \ B)" - by (simp add: subset_def subset_eq) +definition Inf :: "'a::complete_lattice set \ 'a" where + [simp]: "Inf = Complete_Lattice.Inf" -definition eq_set :: "'a set \ 'a set \ bool" where - [code del]: "eq_set = op =" - -(*declare eq_set_def [symmetric, code_unfold]*) +lemma [code_unfold]: + "Complete_Lattice.Inf = Inf" + by simp -lemma [code]: - "eq_set A B \ A \ B \ B \ A" - by (simp add: eq_set_def set_eq) +definition Sup :: "'a::complete_lattice set \ 'a" where + [simp]: "Sup = Complete_Lattice.Sup" -declare inter [code] - -declare List_Set.project_def [symmetric, code_unfold] +lemma [code_unfold]: + "Complete_Lattice.Sup = Sup" + by simp definition Inter :: "'a set set \ 'a set" where - "Inter = Complete_Lattice.Inter" + [simp]: "Inter = Inf" -declare Inter_def [symmetric, code_unfold] +lemma [code_unfold]: + "Inf = Inter" + by simp definition Union :: "'a set set \ 'a set" where - "Union = Complete_Lattice.Union" + [simp]: "Union = Sup" -declare Union_def [symmetric, code_unfold] - +lemma [code_unfold]: + "Sup = Union" + by simp -subsection {* Code generator setup *} - -ML {* -nonfix inter; -nonfix union; -nonfix subset; +setup {* + Code.add_signature_cmd ("inter", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("subtract", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("union", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Inf", "'a set \ 'a") + #> Code.add_signature_cmd ("Sup", "'a set \ 'a") + #> Code.add_signature_cmd ("Inter", "'a set set \ 'a set") + #> Code.add_signature_cmd ("Union", "'a set set \ 'a set") *} -definition flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where - "flip f a b = f b a" +lemma inter_project [code]: + "inter A (Set xs) = Set (List.filter (\x. x \ A) xs)" + "inter A (Coset xs) = foldl (\A x. remove x A) A xs" + by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) + +lemma subtract_remove [code]: + "subtract (Set xs) A = foldl (\A x. remove x A) A xs" + "subtract (Coset xs) A = Set (List.filter (\x. x \ A) xs)" + by (auto simp add: minus_set) -types_code - fset ("(_/ \fset)") -attach {* -datatype 'a fset = Set of 'a list | Coset of 'a list; -*} +lemma union_insert [code]: + "union (Set xs) A = foldl (\A x. insert x A) A xs" + "union (Coset xs) A = Coset (List.filter (\x. x \ A) xs)" + by (auto simp add: union_set) -consts_code - Set ("\Set") - Coset ("\Coset") +lemma Inf_inf [code]: + "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" + "Inf (Coset []) = (bot :: 'a::complete_lattice)" + by (simp_all add: Inf_UNIV Inf_set_fold) -consts_code - "empty" ("{*Fset.empty*}") - "List_Set.is_empty" ("{*Fset.is_empty*}") - "Set.insert" ("{*Fset.insert*}") - "List_Set.remove" ("{*Fset.remove*}") - "Set.image" ("{*Fset.map*}") - "List_Set.project" ("{*Fset.filter*}") - "Ball" ("{*flip Fset.forall*}") - "Bex" ("{*flip Fset.exists*}") - "union" ("{*Fset.union*}") - "inter" ("{*Fset.inter*}") - "op - \ 'a set \ 'a set \ 'a set" ("{*flip Fset.subtract*}") - "Union" ("{*Fset.Union*}") - "Inter" ("{*Fset.Inter*}") - card ("{*Fset.card*}") - fold ("{*foldl o flip*}") +lemma Sup_sup [code]: + "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" + "Sup (Coset []) = (top :: 'a::complete_lattice)" + by (simp_all add: Sup_UNIV Sup_set_fold) + +lemma Inter_inter [code]: + "Inter (Set xs) = foldl inter (Coset []) xs" + "Inter (Coset []) = empty" + unfolding Inter_def Inf_inf by simp_all -hide (open) const empty inter union subset eq_set Inter Union flip +lemma Union_union [code]: + "Union (Set xs) = foldl union empty xs" + "Union (Coset []) = Coset []" + unfolding Union_def Sup_sup by simp_all -end \ No newline at end of file +hide (open) const is_empty empty remove + set_eq subset_eq subset inter union subtract Inf Sup Inter Union + +end diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/Library/Library.thy Mon Dec 07 14:54:13 2009 +0100 @@ -14,7 +14,6 @@ Continuity ContNotDenum Countable - Crude_Executable_Set Diagonalize Efficient_Nat Enum diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_bv_02 --- a/src/HOL/SMT/Examples/cert/z3_bv_02 Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_bv_02 Mon Dec 07 14:54:13 2009 +0100 @@ -1,12 +1,12 @@ (benchmark Isabelle :extrasorts ( T2 T1) :extrafuns ( - (uf_2 T1) - (uf_1 BitVec[4] BitVec[4] T1) - (uf_3 T1 T2) - (uf_4 BitVec[4]) + (uf_4 T1) + (uf_2 BitVec[4] BitVec[4] T1) + (uf_1 T1 T2) + (uf_3 BitVec[4]) ) -:assumption (forall (?x1 BitVec[4]) (?x2 BitVec[4]) (iff (= (uf_1 ?x1 ?x2) uf_2) (bvule ?x1 ?x2))) -:assumption (not (= (uf_3 (uf_1 bv0[4] uf_4)) (uf_3 uf_2))) +:assumption (not (= (uf_1 (uf_2 bv0[4] uf_3)) (uf_1 uf_4))) +:assumption (forall (?x1 BitVec[4]) (?x2 BitVec[4]) (iff (= (uf_2 ?x1 ?x2) uf_4) (bvule ?x1 ?x2))) :formula true ) diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_hol_03 --- a/src/HOL/SMT/Examples/cert/z3_hol_03 Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_hol_03 Mon Dec 07 14:54:13 2009 +0100 @@ -3,11 +3,13 @@ :extrafuns ( (uf_3 T2) (uf_1 T1 T1) - (uf_2 T2 T2) (uf_4 T1) ) +:extrapreds ( + (up_2 T2) + ) :assumption (forall (?x1 T1) (= (uf_1 ?x1) ?x1)) -:assumption (forall (?x2 T2) (iff (= (uf_2 ?x2) uf_3) (= ?x2 uf_3))) -:assumption (not (and (= (uf_1 uf_4) uf_4) (iff (= (uf_2 uf_3) uf_3) true))) +:assumption (forall (?x2 T2) (iff (up_2 ?x2) (= ?x2 uf_3))) +:assumption (not (and (= (uf_1 uf_4) uf_4) (iff (up_2 uf_3) true))) :formula true ) diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_hol_03.proof --- a/src/HOL/SMT/Examples/cert/z3_hol_03.proof Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_hol_03.proof Mon Dec 07 14:54:13 2009 +0100 @@ -1,120 +1,115 @@ #2 := false -decl uf_1 :: (-> T1 T1) -decl uf_4 :: T1 -#15 := uf_4 -#16 := (uf_1 uf_4) -#48 := (= uf_4 #16) -#83 := (not #48) -decl uf_2 :: (-> T2 T2) +decl up_2 :: (-> T2 bool) decl uf_3 :: T2 #10 := uf_3 -#18 := (uf_2 uf_3) -#51 := (= uf_3 #18) -#84 := (not #51) -#556 := [hypothesis]: #84 -#8 := (:var 0 T2) -#9 := (uf_2 #8) -#575 := (pattern #9) -#12 := (= #8 uf_3) -#11 := (= #9 uf_3) -#13 := (iff #11 #12) -#576 := (forall (vars (?x2 T2)) (:pat #575) #13) -#14 := (forall (vars (?x2 T2)) #13) -#579 := (iff #14 #576) -#577 := (iff #13 #13) -#578 := [refl]: #577 -#580 := [quant-intro #578]: #579 -#70 := (~ #14 #14) -#80 := (~ #13 #13) -#81 := [refl]: #80 -#67 := [nnf-pos #81]: #70 -#45 := [asserted]: #14 -#82 := [mp~ #45 #67]: #14 -#581 := [mp #82 #580]: #576 -#242 := (not #576) -#170 := (or #242 #51) -#150 := (= uf_3 uf_3) -#19 := (= #18 uf_3) -#237 := (iff #19 #150) -#243 := (or #242 #237) -#244 := (iff #243 #170) -#560 := (iff #170 #170) -#562 := [rewrite]: #560 -#230 := (iff #237 #51) -#1 := true -#54 := (iff #51 true) -#57 := (iff #54 #51) -#58 := [rewrite]: #57 -#152 := (iff #237 #54) -#151 := (iff #150 true) -#238 := [rewrite]: #151 -#52 := (iff #19 #51) -#53 := [rewrite]: #52 -#239 := [monotonicity #53 #238]: #152 -#241 := [trans #239 #58]: #230 -#223 := [monotonicity #241]: #244 -#217 := [trans #223 #562]: #244 -#240 := [quant-inst]: #243 -#349 := [mp #240 #217]: #170 -#228 := [unit-resolution #349 #581 #556]: false -#229 := [lemma #228]: #51 -#71 := (or #83 #84) -#61 := (and #48 #51) -#64 := (not #61) -#90 := (iff #64 #71) -#72 := (not #71) -#85 := (not #72) -#88 := (iff #85 #71) -#89 := [rewrite]: #88 -#86 := (iff #64 #85) -#73 := (iff #61 #72) -#74 := [rewrite]: #73 -#87 := [monotonicity #74]: #86 -#91 := [trans #87 #89]: #90 -#20 := (iff #19 true) -#17 := (= #16 uf_4) -#21 := (and #17 #20) -#22 := (not #21) -#65 := (iff #22 #64) -#62 := (iff #21 #61) -#59 := (iff #20 #51) -#55 := (iff #20 #54) -#56 := [monotonicity #53]: #55 -#60 := [trans #56 #58]: #59 -#49 := (iff #17 #48) -#50 := [rewrite]: #49 -#63 := [monotonicity #50 #60]: #62 -#66 := [monotonicity #63]: #65 -#46 := [asserted]: #22 -#69 := [mp #46 #66]: #64 -#92 := [mp #69 #91]: #71 -#563 := [unit-resolution #92 #229]: #83 +#17 := (up_2 uf_3) +#78 := (not #17) +decl uf_1 :: (-> T1 T1) +decl uf_4 :: T1 +#14 := uf_4 +#15 := (uf_1 uf_4) +#46 := (= uf_4 #15) +#79 := (not #46) +#145 := [hypothesis]: #79 #4 := (:var 0 T1) #5 := (uf_1 #4) -#568 := (pattern #5) -#39 := (= #4 #5) -#569 := (forall (vars (?x1 T1)) (:pat #568) #39) -#42 := (forall (vars (?x1 T1)) #39) -#572 := (iff #42 #569) -#570 := (iff #39 #39) -#571 := [refl]: #570 -#573 := [quant-intro #571]: #572 -#77 := (~ #42 #42) -#75 := (~ #39 #39) -#76 := [refl]: #75 -#78 := [nnf-pos #76]: #77 +#563 := (pattern #5) +#37 := (= #4 #5) +#564 := (forall (vars (?x1 T1)) (:pat #563) #37) +#40 := (forall (vars (?x1 T1)) #37) +#567 := (iff #40 #564) +#565 := (iff #37 #37) +#566 := [refl]: #565 +#568 := [quant-intro #566]: #567 +#72 := (~ #40 #40) +#70 := (~ #37 #37) +#71 := [refl]: #70 +#73 := [nnf-pos #71]: #72 #6 := (= #5 #4) #7 := (forall (vars (?x1 T1)) #6) -#43 := (iff #7 #42) -#40 := (iff #6 #39) -#41 := [rewrite]: #40 -#44 := [quant-intro #41]: #43 -#38 := [asserted]: #7 -#47 := [mp #38 #44]: #42 -#79 := [mp~ #47 #78]: #42 -#574 := [mp #79 #573]: #569 -#565 := (not #569) -#566 := (or #565 #48) -#561 := [quant-inst]: #566 -[unit-resolution #561 #574 #563]: false +#41 := (iff #7 #40) +#38 := (iff #6 #37) +#39 := [rewrite]: #38 +#42 := [quant-intro #39]: #41 +#36 := [asserted]: #7 +#45 := [mp #36 #42]: #40 +#74 := [mp~ #45 #73]: #40 +#569 := [mp #74 #568]: #564 +#146 := (not #564) +#233 := (or #146 #46) +#147 := [quant-inst]: #233 +#232 := [unit-resolution #147 #569 #145]: false +#234 := [lemma #232]: #46 +#66 := (or #78 #79) +#54 := (and #17 #46) +#59 := (not #54) +#85 := (iff #59 #66) +#67 := (not #66) +#80 := (not #67) +#83 := (iff #80 #66) +#84 := [rewrite]: #83 +#81 := (iff #59 #80) +#68 := (iff #54 #67) +#69 := [rewrite]: #68 +#82 := [monotonicity #69]: #81 +#86 := [trans #82 #84]: #85 +#1 := true +#18 := (iff #17 true) +#16 := (= #15 uf_4) +#19 := (and #16 #18) +#20 := (not #19) +#60 := (iff #20 #59) +#57 := (iff #19 #54) +#51 := (and #46 #17) +#55 := (iff #51 #54) +#56 := [rewrite]: #55 +#52 := (iff #19 #51) +#49 := (iff #18 #17) +#50 := [rewrite]: #49 +#47 := (iff #16 #46) +#48 := [rewrite]: #47 +#53 := [monotonicity #48 #50]: #52 +#58 := [trans #53 #56]: #57 +#61 := [monotonicity #58]: #60 +#44 := [asserted]: #20 +#64 := [mp #44 #61]: #59 +#87 := [mp #64 #86]: #66 +#561 := [unit-resolution #87 #234]: #78 +#8 := (:var 0 T2) +#9 := (up_2 #8) +#570 := (pattern #9) +#11 := (= #8 uf_3) +#12 := (iff #9 #11) +#571 := (forall (vars (?x2 T2)) (:pat #570) #12) +#13 := (forall (vars (?x2 T2)) #12) +#574 := (iff #13 #571) +#572 := (iff #12 #12) +#573 := [refl]: #572 +#575 := [quant-intro #573]: #574 +#65 := (~ #13 #13) +#75 := (~ #12 #12) +#76 := [refl]: #75 +#62 := [nnf-pos #76]: #65 +#43 := [asserted]: #13 +#77 := [mp~ #43 #62]: #13 +#576 := [mp #77 #575]: #571 +#555 := (not #571) +#557 := (or #555 #17) +#225 := (= uf_3 uf_3) +#236 := (iff #17 #225) +#212 := (or #555 #236) +#551 := (iff #212 #557) +#224 := (iff #557 #557) +#558 := [rewrite]: #224 +#239 := (iff #236 #17) +#238 := (iff #236 #18) +#237 := (iff #225 true) +#165 := [rewrite]: #237 +#235 := [monotonicity #165]: #238 +#218 := [trans #235 #50]: #239 +#223 := [monotonicity #218]: #551 +#559 := [trans #223 #558]: #551 +#344 := [quant-inst]: #212 +#560 := [mp #344 #559]: #557 +[unit-resolution #560 #576 #561]: false unsat diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_linarith_07 --- a/src/HOL/SMT/Examples/cert/z3_linarith_07 Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_07 Mon Dec 07 14:54:13 2009 +0100 @@ -1,11 +1,11 @@ (benchmark Isabelle :extrasorts ( T2 T1) :extrafuns ( - (uf_2 T1) - (uf_1 Int Int T1) - (uf_3 T1 T2) + (uf_3 T1) + (uf_2 Int Int T1) + (uf_1 T1 T2) ) -:assumption (forall (?x1 Int) (?x2 Int) (iff (= (uf_1 ?x1 ?x2) uf_2) (< ?x1 ?x2))) -:assumption (not (= (uf_3 (uf_1 2 3)) (uf_3 uf_2))) +:assumption (not (= (uf_1 (uf_2 2 3)) (uf_1 uf_3))) +:assumption (forall (?x1 Int) (?x2 Int) (iff (= (uf_2 ?x1 ?x2) uf_3) (< ?x1 ?x2))) :formula true ) diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_linarith_07.proof --- a/src/HOL/SMT/Examples/cert/z3_linarith_07.proof Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_07.proof Mon Dec 07 14:54:13 2009 +0100 @@ -1,105 +1,124 @@ #2 := false -decl uf_3 :: (-> T1 T2) -decl uf_2 :: T1 -#7 := uf_2 -#16 := (uf_3 uf_2) -decl uf_1 :: (-> int int T1) -#13 := 3::int -#12 := 2::int -#14 := (uf_1 2::int 3::int) -#15 := (uf_3 #14) -#17 := (= #15 #16) -#516 := (= #16 #15) -#194 := (= uf_2 #14) -#5 := (:var 0 int) -#4 := (:var 1 int) -#6 := (uf_1 #4 #5) -#530 := (pattern #6) -#39 := 0::int -#37 := -1::int -#41 := (* -1::int #5) -#42 := (+ #4 #41) -#40 := (>= #42 0::int) -#38 := (not #40) -#8 := (= #6 uf_2) -#45 := (iff #8 #38) -#531 := (forall (vars (?x1 int) (?x2 int)) (:pat #530) #45) -#48 := (forall (vars (?x1 int) (?x2 int)) #45) -#534 := (iff #48 #531) -#532 := (iff #45 #45) -#533 := [refl]: #532 -#535 := [quant-intro #533]: #534 -#58 := (~ #48 #48) -#56 := (~ #45 #45) -#57 := [refl]: #56 -#59 := [nnf-pos #57]: #58 -#9 := (< #4 #5) -#10 := (iff #8 #9) -#11 := (forall (vars (?x1 int) (?x2 int)) #10) -#49 := (iff #11 #48) -#46 := (iff #10 #45) -#43 := (iff #9 #38) +decl uf_1 :: (-> T1 T2) +decl uf_3 :: T1 +#8 := uf_3 +#9 := (uf_1 uf_3) +decl uf_2 :: (-> int int T1) +#5 := 3::int +#4 := 2::int +#6 := (uf_2 2::int 3::int) +#7 := (uf_1 #6) +#10 := (= #7 #9) +#225 := (= #6 uf_3) +#13 := (:var 0 int) +#12 := (:var 1 int) +#14 := (uf_2 #12 #13) +#549 := (pattern #14) +#52 := 0::int +#50 := -1::int +#54 := (* -1::int #13) +#55 := (+ #12 #54) +#53 := (>= #55 0::int) +#51 := (not #53) +#36 := (= uf_3 #14) +#61 := (iff #36 #51) +#550 := (forall (vars (?x1 int) (?x2 int)) (:pat #549) #61) +#66 := (forall (vars (?x1 int) (?x2 int)) #61) +#553 := (iff #66 #550) +#551 := (iff #61 #61) +#552 := [refl]: #551 +#554 := [quant-intro #552]: #553 +#79 := (~ #66 #66) +#77 := (~ #61 #61) +#78 := [refl]: #77 +#80 := [nnf-pos #78]: #79 +#16 := (< #12 #13) +#15 := (= #14 uf_3) +#17 := (iff #15 #16) +#18 := (forall (vars (?x1 int) (?x2 int)) #17) +#69 := (iff #18 #66) +#42 := (iff #16 #36) +#47 := (forall (vars (?x1 int) (?x2 int)) #42) +#67 := (iff #47 #66) +#64 := (iff #42 #61) +#58 := (iff #51 #36) +#62 := (iff #58 #61) +#63 := [rewrite]: #62 +#59 := (iff #42 #58) +#56 := (iff #16 #51) +#57 := [rewrite]: #56 +#60 := [monotonicity #57]: #59 +#65 := [trans #60 #63]: #64 +#68 := [quant-intro #65]: #67 +#48 := (iff #18 #47) +#45 := (iff #17 #42) +#39 := (iff #36 #16) +#43 := (iff #39 #42) #44 := [rewrite]: #43 -#47 := [monotonicity #44]: #46 -#50 := [quant-intro #47]: #49 +#40 := (iff #17 #39) +#37 := (iff #15 #36) +#38 := [rewrite]: #37 +#41 := [monotonicity #38]: #40 +#46 := [trans #41 #44]: #45 +#49 := [quant-intro #46]: #48 +#70 := [trans #49 #68]: #69 +#35 := [asserted]: #18 +#71 := [mp #35 #70]: #66 +#74 := [mp~ #71 #80]: #66 +#555 := [mp #74 #554]: #550 +#529 := (not #550) +#530 := (or #529 #225) +#220 := (* -1::int 3::int) +#221 := (+ 2::int #220) +#222 := (>= #221 0::int) +#213 := (not #222) +#135 := (= uf_3 #6) +#224 := (iff #135 #213) +#525 := (or #529 #224) +#169 := (iff #525 #530) +#534 := (iff #530 #530) +#174 := [rewrite]: #534 +#527 := (iff #224 #225) +#1 := true +#187 := (iff #225 true) +#190 := (iff #187 #225) +#526 := [rewrite]: #190 +#188 := (iff #224 #187) +#183 := (iff #213 true) +#198 := (not false) +#199 := (iff #198 true) +#540 := [rewrite]: #199 +#203 := (iff #213 #198) +#548 := (iff #222 false) +#544 := (>= -1::int 0::int) +#547 := (iff #544 false) +#542 := [rewrite]: #547 +#545 := (iff #222 #544) +#211 := (= #221 -1::int) +#223 := -3::int +#541 := (+ 2::int -3::int) +#330 := (= #541 -1::int) +#537 := [rewrite]: #330 +#543 := (= #221 #541) +#227 := (= #220 -3::int) +#206 := [rewrite]: #227 +#200 := [monotonicity #206]: #543 +#212 := [trans #200 #537]: #211 +#546 := [monotonicity #212]: #545 +#538 := [trans #546 #542]: #548 +#539 := [monotonicity #538]: #203 +#524 := [trans #539 #540]: #183 +#153 := (iff #135 #225) +#226 := [rewrite]: #153 +#189 := [monotonicity #226 #524]: #188 +#528 := [trans #189 #526]: #527 +#532 := [monotonicity #528]: #169 +#175 := [trans #532 #174]: #169 +#531 := [quant-inst]: #525 +#535 := [mp #531 #175]: #530 +#533 := [unit-resolution #535 #555]: #225 +#536 := [monotonicity #533]: #10 +#11 := (not #10) #34 := [asserted]: #11 -#51 := [mp #34 #50]: #48 -#60 := [mp~ #51 #59]: #48 -#536 := [mp #60 #535]: #531 -#508 := (not #531) -#509 := (or #508 #194) -#201 := (* -1::int 3::int) -#115 := (+ 2::int #201) -#202 := (>= #115 0::int) -#116 := (not #202) -#114 := (= #14 uf_2) -#203 := (iff #114 #116) -#510 := (or #508 #203) -#506 := (iff #510 #509) -#150 := (iff #509 #509) -#513 := [rewrite]: #150 -#171 := (iff #203 #194) -#1 := true -#164 := (iff #194 true) -#169 := (iff #164 #194) -#170 := [rewrite]: #169 -#505 := (iff #203 #164) -#180 := (iff #116 true) -#529 := (not false) -#184 := (iff #529 true) -#520 := [rewrite]: #184 -#519 := (iff #116 #529) -#528 := (iff #202 false) -#192 := (>= -1::int 0::int) -#526 := (iff #192 false) -#527 := [rewrite]: #526 -#193 := (iff #202 #192) -#311 := (= #115 -1::int) -#134 := -3::int -#208 := (+ 2::int -3::int) -#524 := (= #208 -1::int) -#181 := [rewrite]: #524 -#187 := (= #115 #208) -#207 := (= #201 -3::int) -#204 := [rewrite]: #207 -#522 := [monotonicity #204]: #187 -#518 := [trans #522 #181]: #311 -#525 := [monotonicity #518]: #193 -#523 := [trans #525 #527]: #528 -#179 := [monotonicity #523]: #519 -#521 := [trans #179 #520]: #180 -#205 := (iff #114 #194) -#206 := [rewrite]: #205 -#168 := [monotonicity #206 #521]: #505 -#507 := [trans #168 #170]: #171 -#512 := [monotonicity #507]: #506 -#515 := [trans #512 #513]: #506 -#511 := [quant-inst]: #510 -#155 := [mp #511 #515]: #509 -#156 := [unit-resolution #155 #536]: #194 -#514 := [monotonicity #156]: #516 -#517 := [symm #514]: #17 -#18 := (not #17) -#35 := [asserted]: #18 -[unit-resolution #35 #517]: false +[unit-resolution #34 #536]: false unsat diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_linarith_13 --- a/src/HOL/SMT/Examples/cert/z3_linarith_13 Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_13 Mon Dec 07 14:54:13 2009 +0100 @@ -1,13 +1,13 @@ (benchmark Isabelle :extrasorts ( T1) :extrafuns ( - (uf_2 T1) - (uf_3 Int Int T1) + (uf_4 T1) (uf_1 Int Int T1) - (uf_4 Int) + (uf_3 Int Int T1) + (uf_2 Int) ) -:assumption (forall (?x1 Int) (?x2 Int) (iff (= (uf_1 ?x1 ?x2) uf_2) (<= ?x1 ?x2))) -:assumption (forall (?x3 Int) (?x4 Int) (iff (= (uf_3 ?x3 ?x4) uf_2) (< ?x3 ?x4))) -:assumption (not (distinct (uf_3 uf_4 3) (uf_1 3 uf_4))) +:assumption (not (distinct (uf_1 uf_2 3) (uf_3 3 uf_2))) +:assumption (forall (?x1 Int) (?x2 Int) (iff (= (uf_3 ?x1 ?x2) uf_4) (<= ?x1 ?x2))) +:assumption (forall (?x3 Int) (?x4 Int) (iff (= (uf_1 ?x3 ?x4) uf_4) (< ?x3 ?x4))) :formula true ) diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Examples/cert/z3_linarith_13.proof --- a/src/HOL/SMT/Examples/cert/z3_linarith_13.proof Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_13.proof Mon Dec 07 14:54:13 2009 +0100 @@ -1,212 +1,212 @@ #2 := false -decl uf_3 :: (-> int int T1) -#18 := 3::int -decl uf_4 :: int -#17 := uf_4 -#19 := (uf_3 uf_4 3::int) -decl uf_2 :: T1 -#7 := uf_2 -#221 := (= uf_2 #19) +decl uf_4 :: T1 +#13 := uf_4 decl uf_1 :: (-> int int T1) -#20 := (uf_1 3::int uf_4) -#256 := (= uf_2 #20) -#531 := (iff #256 #221) -#529 := (iff #221 #256) -#87 := (= #19 #20) -#21 := (distinct #19 #20) -#22 := (not #21) -#96 := (iff #22 #87) -#88 := (not #87) -#91 := (not #88) -#94 := (iff #91 #87) -#95 := [rewrite]: #94 -#92 := (iff #22 #91) -#89 := (iff #21 #88) -#90 := [rewrite]: #89 -#93 := [monotonicity #90]: #92 -#97 := [trans #93 #95]: #96 -#86 := [asserted]: #22 -#100 := [mp #86 #97]: #87 -#530 := [monotonicity #100]: #529 -#525 := [symm #530]: #531 -#548 := (not #221) -#232 := (not #256) -#526 := (iff #232 #548) -#532 := [monotonicity #525]: #526 -#536 := [hypothesis]: #232 -#533 := [mp #536 #532]: #548 -#259 := (>= uf_4 3::int) -#576 := (not #259) -#542 := (or #256 #576) -#257 := (iff #256 #259) -#5 := (:var 0 int) -#4 := (:var 1 int) -#6 := (uf_1 #4 #5) -#583 := (pattern #6) -#44 := 0::int -#41 := -1::int -#42 := (* -1::int #5) -#43 := (+ #4 #42) -#45 := (<= #43 0::int) -#8 := (= #6 uf_2) -#48 := (iff #8 #45) -#584 := (forall (vars (?x1 int) (?x2 int)) (:pat #583) #48) -#51 := (forall (vars (?x1 int) (?x2 int)) #48) -#587 := (iff #51 #584) -#585 := (iff #48 #48) -#586 := [refl]: #585 -#588 := [quant-intro #586]: #587 -#108 := (~ #51 #51) -#106 := (~ #48 #48) +#5 := 3::int +decl uf_2 :: int +#4 := uf_2 +#6 := (uf_1 uf_2 3::int) +#559 := (= #6 uf_4) +decl uf_3 :: (-> int int T1) +#7 := (uf_3 3::int uf_2) +#254 := (= #7 uf_4) +#524 := (iff #254 #559) +#529 := (iff #559 #254) +#39 := (= #6 #7) +#8 := (distinct #6 #7) +#9 := (not #8) +#48 := (iff #9 #39) +#40 := (not #39) +#43 := (not #40) +#46 := (iff #43 #39) +#47 := [rewrite]: #46 +#44 := (iff #9 #43) +#41 := (iff #8 #40) +#42 := [rewrite]: #41 +#45 := [monotonicity #42]: #44 +#49 := [trans #45 #47]: #48 +#38 := [asserted]: #9 +#52 := [mp #38 #49]: #39 +#523 := [monotonicity #52]: #529 +#530 := [symm #523]: #524 +#547 := (not #559) +#570 := (not #254) +#531 := (iff #570 #547) +#525 := [monotonicity #530]: #531 +#540 := [hypothesis]: #570 +#532 := [mp #540 #525]: #547 +#256 := (>= uf_2 3::int) +#579 := (not #256) +#541 := (or #254 #579) +#258 := (iff #254 #256) +#11 := (:var 0 int) +#10 := (:var 1 int) +#12 := (uf_3 #10 #11) +#581 := (pattern #12) +#57 := 0::int +#54 := -1::int +#55 := (* -1::int #11) +#56 := (+ #10 #55) +#58 := (<= #56 0::int) +#14 := (= #12 uf_4) +#61 := (iff #14 #58) +#582 := (forall (vars (?x1 int) (?x2 int)) (:pat #581) #61) +#64 := (forall (vars (?x1 int) (?x2 int)) #61) +#585 := (iff #64 #582) +#583 := (iff #61 #61) +#584 := [refl]: #583 +#586 := [quant-intro #584]: #585 +#108 := (~ #64 #64) +#106 := (~ #61 #61) #107 := [refl]: #106 #109 := [nnf-pos #107]: #108 -#9 := (<= #4 #5) -#10 := (iff #8 #9) -#11 := (forall (vars (?x1 int) (?x2 int)) #10) -#52 := (iff #11 #51) -#49 := (iff #10 #48) -#46 := (iff #9 #45) -#47 := [rewrite]: #46 -#50 := [monotonicity #47]: #49 -#53 := [quant-intro #50]: #52 -#38 := [asserted]: #11 -#54 := [mp #38 #53]: #51 -#110 := [mp~ #54 #109]: #51 -#589 := [mp #110 #588]: #584 -#575 := (not #584) -#577 := (or #575 #257) -#167 := (* -1::int uf_4) -#254 := (+ 3::int #167) -#168 := (<= #254 0::int) -#255 := (= #20 uf_2) -#169 := (iff #255 #168) -#234 := (or #575 #169) -#571 := (iff #234 #577) -#246 := (iff #577 #577) -#578 := [rewrite]: #246 -#261 := (iff #169 #257) -#187 := (iff #168 #259) -#260 := [rewrite]: #187 -#247 := (iff #255 #256) -#258 := [rewrite]: #247 -#240 := [monotonicity #258 #260]: #261 -#245 := [monotonicity #240]: #571 -#579 := [trans #245 #578]: #571 -#364 := [quant-inst]: #234 -#580 := [mp #364 #579]: #577 -#541 := [unit-resolution #580 #589]: #257 -#581 := (not #257) -#582 := (or #581 #256 #576) -#572 := [def-axiom]: #582 -#537 := [unit-resolution #572 #541]: #542 -#543 := [unit-resolution #537 #536]: #576 -#385 := (or #221 #259) -#552 := (iff #221 #576) -#12 := (uf_3 #4 #5) -#590 := (pattern #12) -#69 := (>= #43 0::int) -#68 := (not #69) -#40 := (= uf_2 #12) -#75 := (iff #40 #68) -#591 := (forall (vars (?x3 int) (?x4 int)) (:pat #590) #75) -#80 := (forall (vars (?x3 int) (?x4 int)) #75) -#594 := (iff #80 #591) -#592 := (iff #75 #75) -#593 := [refl]: #592 -#595 := [quant-intro #593]: #594 -#101 := (~ #80 #80) -#111 := (~ #75 #75) -#112 := [refl]: #111 -#98 := [nnf-pos #112]: #101 -#14 := (< #4 #5) -#13 := (= #12 uf_2) -#15 := (iff #13 #14) -#16 := (forall (vars (?x3 int) (?x4 int)) #15) -#83 := (iff #16 #80) -#60 := (iff #14 #40) -#65 := (forall (vars (?x3 int) (?x4 int)) #60) -#81 := (iff #65 #80) -#78 := (iff #60 #75) -#72 := (iff #68 #40) -#76 := (iff #72 #75) -#77 := [rewrite]: #76 -#73 := (iff #60 #72) -#70 := (iff #14 #68) -#71 := [rewrite]: #70 -#74 := [monotonicity #71]: #73 -#79 := [trans #74 #77]: #78 -#82 := [quant-intro #79]: #81 -#66 := (iff #16 #65) -#63 := (iff #15 #60) -#57 := (iff #40 #14) -#61 := (iff #57 #60) -#62 := [rewrite]: #61 -#58 := (iff #15 #57) -#55 := (iff #13 #40) -#56 := [rewrite]: #55 -#59 := [monotonicity #56]: #58 -#64 := [trans #59 #62]: #63 -#67 := [quant-intro #64]: #66 -#84 := [trans #67 #82]: #83 -#39 := [asserted]: #16 -#85 := [mp #39 #84]: #80 -#113 := [mp~ #85 #98]: #80 -#596 := [mp #113 #595]: #591 -#276 := (not #591) -#550 := (or #276 #552) -#222 := (* -1::int 3::int) -#223 := (+ uf_4 #222) -#224 := (>= #223 0::int) -#560 := (not #224) -#561 := (iff #221 #560) -#554 := (or #276 #561) -#555 := (iff #554 #550) -#266 := (iff #550 #550) -#267 := [rewrite]: #266 -#553 := (iff #561 #552) -#282 := (iff #560 #576) -#280 := (iff #224 #259) +#15 := (<= #10 #11) +#16 := (iff #14 #15) +#17 := (forall (vars (?x1 int) (?x2 int)) #16) +#65 := (iff #17 #64) +#62 := (iff #16 #61) +#59 := (iff #15 #58) +#60 := [rewrite]: #59 +#63 := [monotonicity #60]: #62 +#66 := [quant-intro #63]: #65 +#50 := [asserted]: #17 +#67 := [mp #50 #66]: #64 +#101 := [mp~ #67 #109]: #64 +#587 := [mp #101 #586]: #582 +#238 := (not #582) +#573 := (or #238 #258) +#167 := (* -1::int uf_2) +#252 := (+ 3::int #167) +#253 := (<= #252 0::int) +#245 := (iff #254 #253) +#575 := (or #238 #245) +#362 := (iff #575 #573) +#243 := (iff #573 #573) +#244 := [rewrite]: #243 +#255 := (iff #245 #258) +#257 := (iff #253 #256) +#185 := [rewrite]: #257 +#259 := [monotonicity #185]: #255 +#569 := [monotonicity #259]: #362 +#576 := [trans #569 #244]: #362 +#232 := [quant-inst]: #575 +#577 := [mp #232 #576]: #573 +#535 := [unit-resolution #577 #587]: #258 +#578 := (not #258) +#574 := (or #578 #254 #579) +#580 := [def-axiom]: #574 +#382 := [unit-resolution #580 #535]: #541 +#383 := [unit-resolution #382 #540]: #579 +#526 := (or #559 #256) +#273 := (iff #559 #579) +#18 := (uf_1 #10 #11) +#588 := (pattern #18) +#82 := (>= #56 0::int) +#81 := (not #82) +#53 := (= uf_4 #18) +#88 := (iff #53 #81) +#589 := (forall (vars (?x3 int) (?x4 int)) (:pat #588) #88) +#93 := (forall (vars (?x3 int) (?x4 int)) #88) +#592 := (iff #93 #589) +#590 := (iff #88 #88) +#591 := [refl]: #590 +#593 := [quant-intro #591]: #592 +#102 := (~ #93 #93) +#99 := (~ #88 #88) +#110 := [refl]: #99 +#103 := [nnf-pos #110]: #102 +#20 := (< #10 #11) +#19 := (= #18 uf_4) +#21 := (iff #19 #20) +#22 := (forall (vars (?x3 int) (?x4 int)) #21) +#96 := (iff #22 #93) +#73 := (iff #20 #53) +#78 := (forall (vars (?x3 int) (?x4 int)) #73) +#94 := (iff #78 #93) +#91 := (iff #73 #88) +#85 := (iff #81 #53) +#89 := (iff #85 #88) +#90 := [rewrite]: #89 +#86 := (iff #73 #85) +#83 := (iff #20 #81) +#84 := [rewrite]: #83 +#87 := [monotonicity #84]: #86 +#92 := [trans #87 #90]: #91 +#95 := [quant-intro #92]: #94 +#79 := (iff #22 #78) +#76 := (iff #21 #73) +#70 := (iff #53 #20) +#74 := (iff #70 #73) +#75 := [rewrite]: #74 +#71 := (iff #21 #70) +#68 := (iff #19 #53) +#69 := [rewrite]: #68 +#72 := [monotonicity #69]: #71 +#77 := [trans #72 #75]: #76 +#80 := [quant-intro #77]: #79 +#97 := [trans #80 #95]: #96 +#51 := [asserted]: #22 +#98 := [mp #51 #97]: #93 +#111 := [mp~ #98 #103]: #93 +#594 := [mp #111 #593]: #589 +#552 := (not #589) +#549 := (or #552 #273) +#219 := (* -1::int 3::int) +#220 := (+ uf_2 #219) +#221 := (>= #220 0::int) +#222 := (not #221) +#556 := (= uf_4 #6) +#558 := (iff #556 #222) +#553 := (or #552 #558) +#264 := (iff #553 #549) +#266 := (iff #549 #549) +#544 := [rewrite]: #266 +#274 := (iff #558 #273) +#550 := (iff #222 #579) +#280 := (iff #221 #256) #562 := -3::int -#566 := (+ -3::int uf_4) -#567 := (>= #566 0::int) -#557 := (iff #567 #259) -#279 := [rewrite]: #557 -#570 := (iff #224 #567) -#209 := (= #223 #566) -#559 := (+ uf_4 -3::int) -#568 := (= #559 #566) -#208 := [rewrite]: #568 -#565 := (= #223 #559) -#563 := (= #222 -3::int) -#564 := [rewrite]: #563 -#203 := [monotonicity #564]: #565 -#569 := [trans #203 #208]: #209 -#556 := [monotonicity #569]: #570 -#281 := [trans #556 #279]: #280 -#175 := [monotonicity #281]: #282 -#275 := [monotonicity #175]: #553 -#265 := [monotonicity #275]: #555 -#268 := [trans #265 #267]: #555 -#551 := [quant-inst]: #554 -#546 := [mp #551 #268]: #550 -#384 := [unit-resolution #546 #596]: #552 -#547 := (not #552) -#262 := (or #547 #221 #259) -#544 := [def-axiom]: #262 -#386 := [unit-resolution #544 #384]: #385 -#528 := [unit-resolution #386 #543]: #221 -#527 := [unit-resolution #528 #533]: false -#534 := [lemma #527]: #256 -#523 := [mp #534 #525]: #221 -#363 := (or #232 #259) -#237 := (or #581 #232 #259) -#573 := [def-axiom]: #237 -#365 := [unit-resolution #573 #541]: #363 -#366 := [unit-resolution #365 #534]: #259 -#519 := (or #548 #576) -#545 := (or #547 #548 #576) -#549 := [def-axiom]: #545 -#520 := [unit-resolution #549 #384]: #519 -#522 := [unit-resolution #520 #366]: #548 -[unit-resolution #522 #523]: false +#206 := (+ -3::int uf_2) +#554 := (>= #206 0::int) +#278 := (iff #554 #256) +#279 := [rewrite]: #278 +#555 := (iff #221 #554) +#565 := (= #220 #206) +#201 := (+ uf_2 -3::int) +#207 := (= #201 #206) +#567 := [rewrite]: #207 +#564 := (= #220 #201) +#557 := (= #219 -3::int) +#563 := [rewrite]: #557 +#566 := [monotonicity #563]: #564 +#568 := [trans #566 #567]: #565 +#277 := [monotonicity #568]: #555 +#173 := [trans #277 #279]: #280 +#551 := [monotonicity #173]: #550 +#560 := (iff #556 #559) +#561 := [rewrite]: #560 +#548 := [monotonicity #561 #551]: #274 +#265 := [monotonicity #548]: #264 +#545 := [trans #265 #544]: #264 +#263 := [quant-inst]: #553 +#260 := [mp #263 #545]: #549 +#384 := [unit-resolution #260 #594]: #273 +#542 := (not #273) +#546 := (or #542 #559 #256) +#543 := [def-axiom]: #546 +#527 := [unit-resolution #543 #384]: #526 +#528 := [unit-resolution #527 #383]: #559 +#361 := [unit-resolution #528 #532]: false +#363 := [lemma #361]: #254 +#522 := [mp #363 #530]: #559 +#364 := (or #570 #256) +#230 := (or #578 #570 #256) +#235 := [def-axiom]: #230 +#517 := [unit-resolution #235 #535]: #364 +#518 := [unit-resolution #517 #363]: #256 +#520 := (or #547 #579) +#536 := (or #542 #547 #579) +#537 := [def-axiom]: #536 +#521 := [unit-resolution #537 #384]: #520 +#519 := [unit-resolution #521 #518]: #547 +[unit-resolution #519 #522]: false unsat diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Tools/smt_monomorph.ML --- a/src/HOL/SMT/Tools/smt_monomorph.ML Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML Mon Dec 07 14:54:13 2009 +0100 @@ -74,16 +74,18 @@ fun incr_tvar_indices i t = let - val incrT = Logic.incr_tvar i + val incrT = Logic.incr_tvar_same i fun incr t = (case t of Const (n, T) => Const (n, incrT T) | Free (n, T) => Free (n, incrT T) - | Abs (n, T, t1) => Abs (n, incrT T, incr t1) - | t1 $ t2 => incr t1 $ incr t2 - | _ => t) - in incr t end + | Abs (n, T, t1) => (Abs (n, incrT T, incr t1 handle Same.SAME => t1) + handle Same.SAME => Abs (n, T, incr t1)) + | t1 $ t2 => (incr t1 $ (incr t2 handle Same.SAME => t2) + handle Same.SAME => t1 $ incr t2) + | _ => Same.same t) + in incr t handle Same.SAME => t end val monomorph_limit = 10 @@ -93,18 +95,17 @@ create copies of terms containing those constants. To prevent non-termination, there is an upper limit for the number of recursions involved in the fixpoint construction. *) -fun monomorph thy ts = +fun monomorph thy = let - val (ps, ms) = List.partition term_has_tvars ts + fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1) + fun incr_indices ts = fst (fold_map incr ts 0) fun with_tvar (n, Ts) = let val Ts' = filter typ_has_tvars Ts in if null Ts' then NONE else SOME (n, Ts') end - fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1) - val rps = fst (fold_map incr ps 0) - |> map (fn r => (r, map_filter with_tvar (consts_of [r]))) + fun extract_consts_with_tvar t = (t, map_filter with_tvar (consts_of [t])) - fun mono count is ces cs ts = + fun mono rps count is ces cs ts = let val spec = specialize thy cs is val (ces', (ts', is')) = fold_map spec (rps ~~ ces) (ts, []) @@ -113,8 +114,15 @@ if null is' then ts' else if count > monomorph_limit then (warning "monomorphization limit reached"; ts') - else mono (count + 1) is' ces' cs' ts' + else mono rps (count + 1) is' ces' cs' ts' end - in mono 0 (consts_of ms) (map (K []) rps) [] ms end + fun mono_all rps ms = if null rps then ms + else mono rps 0 (consts_of ms) (map (K []) rps) [] ms + in + List.partition term_has_tvars + #>> incr_indices + #>> map extract_consts_with_tvar + #-> mono_all + end end diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Tools/smt_normalize.ML --- a/src/HOL/SMT/Tools/smt_normalize.ML Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Mon Dec 07 14:54:13 2009 +0100 @@ -75,8 +75,26 @@ | Abs _ => Conv.abs_conv (norm_conv o snd) | _ $ _ => Conv.comb_conv o norm_conv | _ => K Conv.all_conv) ctxt ct + + fun is_normed t = + (case t of + Const (@{const_name All}, _) $ Abs (_, _, u) => is_normed u + | Const (@{const_name All}, _) $ _ => false + | Const (@{const_name All}, _) => false + | Const (@{const_name Ex}, _) $ Abs (_, _, u) => is_normed u + | Const (@{const_name Ex}, _) $ _ => false + | Const (@{const_name Ex}, _) => false + | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) => + is_normed u1 andalso is_normed u2 + | Const (@{const_name Let}, _) $ _ $ _ => false + | Const (@{const_name Let}, _) $ _ => false + | Const (@{const_name Let}, _) => false + | Abs (_, _, u) => is_normed u + | u1 $ u2 => is_normed u1 andalso is_normed u2 + | _ => true) in -val norm_binder_conv = norm_conv +fun norm_binder_conv ctxt ct = + if is_normed (Thm.term_of ct) then Conv.all_conv ct else norm_conv ctxt ct end fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) @@ -94,6 +112,19 @@ norm_def ctxt (thm RS @{thm fun_cong}) | _ => thm) +fun atomize_conv ctxt ct = + (case Thm.term_of ct of + @{term "op ==>"} $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_imp} + | Const (@{const_name "=="}, _) $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_eq} + | Const (@{const_name all}, _) $ Abs _ => + More_Conv.binder_conv atomize_conv ctxt then_conv + Conv.rewr_conv @{thm atomize_all} + | _ => Conv.all_conv) ct + fun normalize_rule ctxt = Conv.fconv_rule ( Thm.beta_conversion true then_conv @@ -101,7 +132,7 @@ norm_binder_conv ctxt) #> norm_def ctxt #> Drule.forall_intr_vars #> - Conv.fconv_rule (ObjectLogic.atomize then_conv norm_binder_conv ctxt) + Conv.fconv_rule (atomize_conv ctxt) fun instantiate_free (cv, ct) thm = if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm) @@ -289,14 +320,20 @@ fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms [] - fun unfold_conv ct = - (case AList.lookup (op =) defs (Term.head_of (Thm.term_of ct)) of + fun unfold_def_conv ds ct = + (case AList.lookup (op =) ds (Term.head_of (Thm.term_of ct)) of SOME (_, eq) => Conv.rewr_conv eq | NONE => Conv.all_conv) ct + + fun unfold_conv ctxt thm = + (case filter (member (op =) (add_syms [thm]) o fst) defs of + [] => thm + | ds => thm |> Conv.fconv_rule + (More_Conv.bottom_conv (K (unfold_def_conv ds)) ctxt)) in fun add_abs_min_max_rules ctxt thms = if Config.get ctxt unfold_defs - then map (Conv.fconv_rule (More_Conv.bottom_conv (K unfold_conv) ctxt)) thms + then map (unfold_conv ctxt) thms else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms end @@ -361,13 +398,23 @@ in_abs repl cvs ct #-> (fn thm => replace ctxt cvs (Thm.rhs_of thm) #>> Thm.transitive thm) in repl [] end + + fun has_free_lambdas t = + (case t of + Const (@{const_name All}, _) $ Abs (_, _, u) => has_free_lambdas u + | Const (@{const_name Ex}, _) $ Abs (_, _, u) => has_free_lambdas u + | Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) => + has_free_lambdas u1 orelse has_free_lambdas u2 + | Abs _ => true + | u1 $ u2 => has_free_lambdas u1 orelse has_free_lambdas u2 + | _ => false) in fun lift_lambdas ctxt thms = let val declare_frees = fold (Thm.fold_terms Term.declare_term_frees) fun rewrite f thm cx = - let val (thm', cx') = f (Thm.cprop_of thm) cx - in (Thm.equal_elim thm' thm, cx') end + if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx) + else f (Thm.cprop_of thm) cx |>> (fn thm' => Thm.equal_elim thm' thm) val rev_int_fst_ord = rev_order o int_ord o pairself fst fun ordered_values tab = @@ -425,8 +472,18 @@ Conv.rewr_conv apply_rule then_conv binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct + fun needs_exp_app tab = Term.exists_subterm (fn + Bound _ $ _ => true + | Const (n, _) => Symtab.defined tab (const n) + | Free (n, _) => Symtab.defined tab (free n) + | _ => false) + + fun rewrite tab ctxt thm = + if not (needs_exp_app tab (Thm.prop_of thm)) then thm + else Conv.fconv_rule (sub_conv tab ctxt) thm + val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty) - in map (Conv.fconv_rule (sub_conv tab ctxt)) thms end + in map (rewrite tab ctxt) thms end end diff -r e820ed4bfd94 -r bb37c95f0b8e src/HOL/SMT/Tools/smt_translate.ML --- a/src/HOL/SMT/Tools/smt_translate.ML Mon Dec 07 11:48:40 2009 +0100 +++ b/src/HOL/SMT/Tools/smt_translate.ML Mon Dec 07 14:54:13 2009 +0100 @@ -241,15 +241,42 @@ specifying their meaning are added. *) local - (** Add the marker symbols "term" and "formulas" to separate formulas and + local + fun cons_nr (SConst _) = 0 + | cons_nr (SFree _) = 1 + | cons_nr (SNum _) = 2 + + fun struct_ord (t, u) = int_ord (cons_nr t, cons_nr u) + + fun atoms_ord (SConst (n, _), SConst (m, _)) = fast_string_ord (n, m) + | atoms_ord (SFree (n, _), SFree (m, _)) = fast_string_ord (n, m) + | atoms_ord (SNum (i, _), SNum (j, _)) = int_ord (i, j) + | atoms_ord _ = sys_error "atoms_ord" + + fun types_ord (SConst (_, T), SConst (_, U)) = TermOrd.typ_ord (T, U) + | types_ord (SFree (_, T), SFree (_, U)) = TermOrd.typ_ord (T, U) + | types_ord (SNum (_, T), SNum (_, U)) = TermOrd.typ_ord (T, U) + | types_ord _ = sys_error "types_ord" + + fun fast_sym_ord tu = + (case struct_ord tu of + EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord) + | ord => ord) + in + structure Stab = Table(type key = sym val ord = fast_sym_ord) + end + + + (** Add the marker symbols "term" and "formula" to separate formulas and terms. **) val connectives = map make_sconst [@{term True}, @{term False}, @{term Not}, @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"}] - fun note false c (ps, fs) = (insert (op =) c ps, fs) - | note true c (ps, fs) = (ps, insert (op =) c fs) + fun insert_sym c = Stab.map_default (c, ()) I + fun note false c (ps, fs) = (insert_sym c ps, fs) + | note true c (ps, fs) = (ps, insert_sym c fs) val term_marker = SConst (@{const_name term}, Term.dummyT) val formula_marker = SConst (@{const_name formula}, Term.dummyT) @@ -316,7 +343,7 @@ val rule = Conv.fconv_rule (unterm_conv ctxt) thm val prop = Thm.prop_of thm val inst = instantiate (Term.add_tvar_names prop []) - fun inst_for T = (singleton intermediate (inst T prop), rule) + fun inst_for T = (rule, singleton intermediate (inst T prop)) in (make_sconst (head_of (Thm.prop_of rule)), inst_for) end val logicals = map (prepare @{context}) @@ -342,10 +369,15 @@ (n = m) andalso Sign.typ_instance thy (T, U) | is_instance _ _ = false - fun lookup_logical thy (c as SConst (_, T)) = - AList.lookup (is_instance thy) logicals c - |> Option.map (fn inst_for => inst_for T) - | lookup_logical _ _ = NONE + fun rule_for thy c T = + AList.lookup (is_instance thy) logicals c + |> Option.map (fn inst_for => inst_for T) + + fun lookup_logical thy (c as SConst (_, T)) (thms, ts) = + (case rule_for thy c T of + SOME (thm, t) => (thm :: thms, t :: ts) + | NONE => (thms, ts)) + | lookup_logical _ _ tss = tss val s_eq = make_sconst @{term "op = :: bool => _"} val s_True = mark_term (SApp (make_sconst @{term True}, [])) @@ -367,7 +399,7 @@ | SApp (c as SConst (@{const_name formula}, _), [u]) => SApp (c, [rewr env false u]) | SApp (c, us) => - let val f = if not loc andalso member (op =) ls c then holds else I + let val f = if not loc andalso Stab.defined ls c then holds else I in f (SApp (rewr_iff c, map (rewr env loc) us)) end | SLet (v, u1, u2) => SLet (v, rewr env loc u1, rewr (is_term u1 :: env) loc u2) @@ -378,14 +410,12 @@ in fun separate thy ts = let - val (ts', (ps, fs)) = fold_map (sep false) ts ([], []) - val eq_name = (fn - (SConst (n, _), SConst (m, _)) => n = m - | (SFree (n, _), SFree (m, _)) => n = m - | _ => false) - val ls = filter (member eq_name fs) ps - val (us, thms) = split_list (map_filter (lookup_logical thy) fs) - in (thms, us @ rewrite ls ts') end + val (ts', (ps, fs)) = fold_map (sep false) ts (Stab.empty, Stab.empty) + fun insert (px as (p, _)) = if Stab.defined fs p then Stab.update px else I + in + Stab.fold (lookup_logical thy o fst) fs ([], []) + ||> append (rewrite (Stab.fold insert ps Stab.empty) ts') + end end diff -r e820ed4bfd94 -r bb37c95f0b8e src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Dec 07 11:48:40 2009 +0100 +++ b/src/Tools/Code/code_thingol.ML Mon Dec 07 14:54:13 2009 +0100 @@ -928,9 +928,9 @@ | NONE => thy; val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; - fun belongs_here c = - not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) - in if is_some some_thyname then cs else filter belongs_here cs end; + fun belongs_here c = forall + (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy') + in if is_some some_thyname then filter belongs_here cs else cs end; fun read_const_expr "*" = ([], consts_of NONE) | read_const_expr s = if String.isSuffix ".*" s then ([], consts_of (SOME (unsuffix ".*" s)))