--- 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
--- 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 \
--- 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 \<Rightarrow> 'a set" where
- [simp]: "Set = set"
-
-definition Coset :: "'a list \<Rightarrow> 'a set" where
- [simp]: "Coset xs = - set xs"
-
-setup {*
- Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
-*}
-
-code_datatype Set Coset
-
-
-subsection {* Basic operations *}
-
-lemma [code]:
- "set xs = Set (remdups xs)"
- by simp
-
-lemma [code]:
- "x \<in> Set xs \<longleftrightarrow> member x xs"
- "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
- by (simp_all add: mem_iff)
-
-definition is_empty :: "'a set \<Rightarrow> bool" where
- [simp]: "is_empty A \<longleftrightarrow> A = {}"
-
-lemma [code_inline]:
- "A = {} \<longleftrightarrow> 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 \<Rightarrow> bool")
- #> Code.add_signature_cmd ("empty", "'a set")
- #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
- #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
- #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
- #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
-*}
-
-lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> 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 \<longleftrightarrow> list_all P xs"
- by (simp add: ball_set)
-
-lemma Bex_Set [code]:
- "Bex (Set xs) P \<longleftrightarrow> 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 \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "set_eq = op ="
-
-lemma [code_inline]:
- "op = = set_eq"
- by simp
-
-definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "subset_eq = op \<subseteq>"
-
-lemma [code_inline]:
- "op \<subseteq> = subset_eq"
- by simp
-
-definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "subset = op \<subset>"
-
-lemma [code_inline]:
- "op \<subset> = subset"
- by simp
-
-setup {*
- Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
- #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
- #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
-*}
-
-lemma set_eq_subset_eq [code]:
- "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
- by auto
-
-lemma subset_eq_forall [code]:
- "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (simp add: subset_eq)
-
-lemma subset_subset_eq [code]:
- "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
- by (simp add: subset)
-
-
-subsection {* Functorial operations *}
-
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "inter = op \<inter>"
-
-lemma [code_inline]:
- "op \<inter> = inter"
- by simp
-
-definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "subtract A B = B - A"
-
-lemma [code_inline]:
- "B - A = subtract A B"
- by simp
-
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "union = op \<union>"
-
-lemma [code_inline]:
- "op \<union> = union"
- by simp
-
-definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Inf = Complete_Lattice.Inf"
-
-lemma [code_inline]:
- "Complete_Lattice.Inf = Inf"
- by simp
-
-definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Sup = Complete_Lattice.Sup"
-
-lemma [code_inline]:
- "Complete_Lattice.Sup = Sup"
- by simp
-
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- [simp]: "Inter = Inf"
-
-lemma [code_inline]:
- "Inf = Inter"
- by simp
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- [simp]: "Union = Sup"
-
-lemma [code_inline]:
- "Sup = Union"
- by simp
-
-setup {*
- Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
- #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
- #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
-*}
-
-lemma inter_project [code]:
- "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
- "inter A (Coset xs) = foldl (\<lambda>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 (\<lambda>A x. remove x A) A xs"
- "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
- by (auto simp add: minus_set)
-
-lemma union_insert [code]:
- "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
- "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> 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
--- 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 \<Rightarrow> 'a set" where
+ [simp]: "Set = set"
+
+definition Coset :: "'a list \<Rightarrow> 'a set" where
+ [simp]: "Coset xs = - set xs"
+
+setup {*
+ Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
+*}
+
+code_datatype Set Coset
-declare member [code]
+consts_code
+ Coset ("\<module>Coset")
+ Set ("\<module>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 \<in> Set xs \<longleftrightarrow> member x xs"
+ "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
+ by (simp_all add: mem_iff)
+
+definition is_empty :: "'a set \<Rightarrow> bool" where
+ [simp]: "is_empty A \<longleftrightarrow> A = {}"
+
+lemma [code_unfold]:
+ "A = {} \<longleftrightarrow> 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 \<eta>}-expansion produces funny things. *}
+
+setup {*
+ Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("empty", "'a set")
+ #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
+ #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
+*}
+
+lemma is_empty_Set [code]:
+ "is_empty (Set xs) \<longleftrightarrow> 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 \<longleftrightarrow> list_all P xs"
+ by (simp add: ball_set)
-declare empty_def [symmetric, code_unfold]
+lemma Bex_Set [code]:
+ "Bex (Set xs) P \<longleftrightarrow> 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 \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "set_eq = op ="
+
+lemma [code_unfold]:
+ "op = = set_eq"
+ by simp
+
+definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "subset_eq = op \<subseteq>"
+
+lemma [code_unfold]:
+ "op \<subseteq> = subset_eq"
+ by simp
+
+definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "subset = op \<subset>"
+
+lemma [code_unfold]:
+ "op \<subset> = subset"
+ by simp
+
+setup {*
+ Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+*}
+
+lemma set_eq_subset_eq [code]:
+ "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
+ by auto
+
+lemma subset_eq_forall [code]:
+ "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ by (simp add: subset_eq)
+
+lemma subset_subset_eq [code]:
+ "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
+ by (simp add: subset)
+
+
+subsection {* Functorial operations *}
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "inter = op \<inter>"
+ [simp]: "inter = op \<inter>"
+
+lemma [code_unfold]:
+ "op \<inter> = inter"
+ by simp
-declare inter_def [symmetric, code_unfold]
+definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ [simp]: "subtract A B = B - A"
+
+lemma [code_unfold]:
+ "B - A = subtract A B"
+ by simp
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "union = op \<union>"
-
-declare union_def [symmetric, code_unfold]
+ [simp]: "union = op \<union>"
-definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "subset = op \<le>"
+lemma [code_unfold]:
+ "op \<union> = union"
+ by simp
-declare subset_def [symmetric, code_unfold]
-
-lemma [code]:
- "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (simp add: subset_def subset_eq)
+definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
+ [simp]: "Inf = Complete_Lattice.Inf"
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 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 \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by (simp add: eq_set_def set_eq)
+definition Sup :: "'a::complete_lattice set \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
+ #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
+ #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
*}
-definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
- "flip f a b = f b a"
+lemma inter_project [code]:
+ "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
+ "inter A (Coset xs) = foldl (\<lambda>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 (\<lambda>A x. remove x A) A xs"
+ "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
+ by (auto simp add: minus_set)
-types_code
- fset ("(_/ \<module>fset)")
-attach {*
-datatype 'a fset = Set of 'a list | Coset of 'a list;
-*}
+lemma union_insert [code]:
+ "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
+ "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
+ by (auto simp add: union_set)
-consts_code
- Set ("\<module>Set")
- Coset ("\<module>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 - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> '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
--- 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
--- 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
)
--- 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
)
--- 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
--- 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
)
--- 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
--- 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
)
--- 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
--- 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
--- 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
--- 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
--- 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)))