--- a/.hgtags Fri Dec 04 12:17:43 2009 +0100
+++ b/.hgtags Fri Dec 04 15:20:24 2009 +0100
@@ -24,9 +24,4 @@
f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 isa2009-1-test
-14ff44e21bec0e1b99d0f7322949b4fd012333e0 isa2009-1-test
-14ff44e21bec0e1b99d0f7322949b4fd012333e0 isa2009-1-test
-e1c262952b0285fa93f2e153891bc573d3de0f33 isa2009-1-test
+6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
--- a/Admin/makedist Fri Dec 04 12:17:43 2009 +0100
+++ b/Admin/makedist Fri Dec 04 15:20:24 2009 +0100
@@ -4,7 +4,7 @@
## global settings
-REPOS_NAME="isabelle-release"
+REPOS_NAME="isabelle"
REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
--- a/CONTRIBUTORS Fri Dec 04 12:17:43 2009 +0100
+++ b/CONTRIBUTORS Fri Dec 04 15:20:24 2009 +0100
@@ -3,6 +3,9 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
Contributions to Isabelle2009-1
-------------------------------
--- a/NEWS Fri Dec 04 12:17:43 2009 +0100
+++ b/NEWS Fri Dec 04 15:20:24 2009 +0100
@@ -1,6 +1,10 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+New in this Isabelle version
+----------------------------
+
+
New in Isabelle2009-1 (December 2009)
-------------------------------------
--- a/src/HOL/GCD.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/GCD.thy Fri Dec 04 15:20:24 2009 +0100
@@ -779,14 +779,6 @@
apply auto
done
-lemma coprime_divprod_nat: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using coprime_dvd_mult_iff_nat[of d a b]
- by (auto simp add: mult_commute)
-
-lemma coprime_divprod_int: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using coprime_dvd_mult_iff_int[of d a b]
- by (auto simp add: mult_commute)
-
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
proof-
--- a/src/HOL/IsaMakefile Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Dec 04 15:20:24 2009 +0100
@@ -369,6 +369,7 @@
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 \
@@ -381,9 +382,9 @@
Library/Order_Relation.thy Library/Nested_Environment.thy \
Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
Library/Library/document/root.tex Library/Library/document/root.bib \
- Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
- Library/Product_ord.thy Library/Char_nat.thy \
- Library/Char_ord.thy Library/Option_ord.thy \
+ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
+ Library/Product_ord.thy Library/Char_nat.thy \
+ Library/Char_ord.thy Library/Option_ord.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Crude_Executable_Set.thy Fri Dec 04 15:20:24 2009 +0100
@@ -0,0 +1,259 @@
+(* 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 bot_def [symmetric] 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 top_def [symmetric] 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/Fset.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Library/Fset.thy Fri Dec 04 15:20:24 2009 +0100
@@ -210,7 +210,7 @@
member (foldl (\<lambda>B A. Fset (member B \<inter> A)) (Coset []) (List.map member As))"
by (rule foldl_apply_inv) simp
then show "Inter (Set As) = foldl inter (Coset []) As"
- by (simp add: Inter_set image_set inter inter_def_raw foldl_map)
+ by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map)
show "Inter (Coset []) = empty"
by simp
qed
@@ -229,7 +229,7 @@
member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
by (rule foldl_apply_inv) simp
then show "Union (Set As) = foldl union empty As"
- by (simp add: Union_set image_set union_def_raw foldl_map)
+ by (simp add: Sup_set_fold image_set union_def_raw foldl_map)
show "Union (Coset []) = Coset []"
by simp
qed
--- a/src/HOL/Library/Library.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Library/Library.thy Fri Dec 04 15:20:24 2009 +0100
@@ -14,6 +14,7 @@
Continuity
ContNotDenum
Countable
+ Crude_Executable_Set
Diagonalize
Efficient_Nat
Enum
--- a/src/HOL/Library/List_Set.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Library/List_Set.thy Fri Dec 04 15:20:24 2009 +0100
@@ -85,6 +85,50 @@
"project P (set xs) = set (filter P xs)"
by (auto simp add: project_def)
+text {* FIXME move the following to @{text Finite_Set.thy} *}
+
+lemma fun_left_comm_idem_inf:
+ "fun_left_comm_idem inf"
+proof
+qed (auto simp add: inf_left_commute)
+
+lemma fun_left_comm_idem_sup:
+ "fun_left_comm_idem sup"
+proof
+qed (auto simp add: sup_left_commute)
+
+lemma inf_Inf_fold_inf:
+ fixes A :: "'a::complete_lattice set"
+ assumes "finite A"
+ shows "inf B (Inf A) = fold inf B A"
+proof -
+ interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
+qed
+
+lemma sup_Sup_fold_sup:
+ fixes A :: "'a::complete_lattice set"
+ assumes "finite A"
+ shows "sup B (Sup A) = fold sup B A"
+proof -
+ interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
+qed
+
+lemma Inf_fold_inf:
+ fixes A :: "'a::complete_lattice set"
+ assumes "finite A"
+ shows "Inf A = fold inf top A"
+ using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
+ fixes A :: "'a::complete_lattice set"
+ assumes "finite A"
+ shows "Sup A = fold sup bot A"
+ using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
+
subsection {* Functorial set operations *}
@@ -105,41 +149,13 @@
by (simp add: minus_fold_remove [of _ A] fold_set)
qed
-lemma Inter_set:
- "Inter (set As) = foldl (op \<inter>) UNIV As"
-proof -
- have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
- by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
- then show ?thesis
- by (simp only: Inter_fold_inter finite_set Int_commute)
-qed
-
-lemma Union_set:
- "Union (set As) = foldl (op \<union>) {} As"
-proof -
- have "fold (op \<union>) {} (set As) = foldl (\<lambda>y x. x \<union> y) {} As"
- by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
- then show ?thesis
- by (simp only: Union_fold_union finite_set Un_commute)
-qed
+lemma INFI_set_fold: -- "FIXME move to List.thy"
+ "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
+ unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
-lemma INTER_set:
- "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
-proof -
- have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
- by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
- then show ?thesis
- by (simp only: INTER_fold_inter finite_set)
-qed
-
-lemma UNION_set:
- "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As"
-proof -
- have "fold (\<lambda>A. op \<union> (f A)) {} (set As) = foldl (\<lambda>B A. f A \<union> B) {} As"
- by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
- then show ?thesis
- by (simp only: UNION_fold_union finite_set)
-qed
+lemma SUPR_set_fold: -- "FIXME move to List.thy"
+ "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
+ unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
subsection {* Derived set operations *}
--- a/src/HOL/List.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/List.thy Fri Dec 04 15:20:24 2009 +0100
@@ -2665,6 +2665,10 @@
apply(rule length_remdups_leq)
done
+lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
+apply(induct xs)
+apply auto
+done
lemma distinct_map:
"distinct(map f xs) = (distinct xs & inj_on f (set xs))"
--- a/src/HOL/Number_Theory/Primes.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Fri Dec 04 15:20:24 2009 +0100
@@ -360,16 +360,15 @@
from prime_dvd_mult_nat[OF p pab']
have "p dvd a \<or> p dvd b" .
moreover
- {assume pa: "p dvd a"
- have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+ { assume pa: "p dvd a"
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
with p have "coprime b p"
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pnb: "coprime (p^n) b"
by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
+ from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
moreover
- {assume pb: "p dvd b"
+ { assume pb: "p dvd b"
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
by auto
@@ -377,7 +376,7 @@
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pna: "coprime (p^n) a"
by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
+ from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
ultimately have ?thesis by blast}
ultimately show ?thesis by blast
qed
--- a/src/HOL/Set.thy Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Set.thy Fri Dec 04 15:20:24 2009 +0100
@@ -1556,6 +1556,9 @@
lemma imp_refl: "P --> P" ..
+lemma not_mono: "Q --> P ==> ~ P --> ~ Q"
+ by iprover
+
lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
by iprover
@@ -1576,9 +1579,6 @@
lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
by iprover
-lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
- by iprover
-
subsubsection {* Inverse image of a function *}
@@ -1724,7 +1724,6 @@
val contra_subsetD = @{thm contra_subsetD}
val distinct_lemma = @{thm distinct_lemma}
val eq_to_mono = @{thm eq_to_mono}
-val eq_to_mono2 = @{thm eq_to_mono2}
val equalityCE = @{thm equalityCE}
val equalityD1 = @{thm equalityD1}
val equalityD2 = @{thm equalityD2}
--- a/src/HOL/Tools/sat_solver.ML Fri Dec 04 12:17:43 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML Fri Dec 04 15:20:24 2009 +0100
@@ -311,7 +311,7 @@
fun int_from_string s =
case Int.fromString s of
SOME i => i
- | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number")
+ | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
(* int list -> int list list *)
fun clauses xs =
let
@@ -350,7 +350,7 @@
o (map (map literal_from_int))
o clauses
o (map int_from_string)
- o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
+ o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
o filter_preamble
o filter (fn l => l <> "")
o split_lines
--- a/src/Pure/Isar/code.ML Fri Dec 04 12:17:43 2009 +0100
+++ b/src/Pure/Isar/code.ML Fri Dec 04 15:20:24 2009 +0100
@@ -12,6 +12,10 @@
val read_bare_const: theory -> string -> string * typ
val read_const: theory -> string -> string
val string_of_const: theory -> string -> string
+ val cert_signature: theory -> typ -> typ
+ val read_signature: theory -> string -> typ
+ val const_typ: theory -> string -> typ
+ val subst_signatures: theory -> term -> term
val args_number: theory -> string -> int
(*constructor sets*)
@@ -31,6 +35,10 @@
val standard_typscheme: theory -> thm list -> thm list
(*executable code*)
+ val add_type: string -> theory -> theory
+ val add_type_cmd: string -> theory -> theory
+ val add_signature: string * typ -> theory -> theory
+ val add_signature_cmd: string * string -> theory -> theory
val add_datatype: (string * typ) list -> theory -> theory
val add_datatype_cmd: string list -> theory -> theory
val type_interpretation:
@@ -102,6 +110,8 @@
(* constants *)
+fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
+
fun check_bare_const thy t = case try dest_Const t
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
@@ -147,6 +157,7 @@
datatype spec = Spec of {
history_concluded: bool,
+ signatures: int Symtab.table * typ Symtab.table,
eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
(*with explicit history*),
dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
@@ -154,16 +165,19 @@
cases: (int * (int * string list)) Symtab.table * unit Symtab.table
};
-fun make_spec (history_concluded, (eqns, (dtyps, cases))) =
- Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases };
-fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns,
- dtyps = dtyps, cases = cases }) =
- make_spec (f (history_concluded, (eqns, (dtyps, cases))));
-fun merge_spec (Spec { history_concluded = _, eqns = eqns1,
+fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) =
+ Spec { history_concluded = history_concluded,
+ signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases };
+fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
+ eqns = eqns, dtyps = dtyps, cases = cases }) =
+ make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases))));
+fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1,
dtyps = dtyps1, cases = (cases1, undefs1) },
- Spec { history_concluded = _, eqns = eqns2,
+ Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2,
dtyps = dtyps2, cases = (cases2, undefs2) }) =
let
+ val signatures = (Symtab.merge (op =) (tycos1, tycos2),
+ Symtab.merge typ_equiv (sigs1, sigs2));
fun merge_eqns ((_, history1), (_, history2)) =
let
val raw_history = AList.merge (op = : serial * serial -> bool)
@@ -176,14 +190,16 @@
val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
val cases = (Symtab.merge (K true) (cases1, cases2),
Symtab.merge (K true) (undefs1, undefs2));
- in make_spec (false, (eqns, (dtyps, cases))) end;
+ in make_spec (false, ((signatures, eqns), (dtyps, cases))) end;
fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
+fun the_signatures (Spec { signatures, ... }) = signatures;
fun the_eqns (Spec { eqns, ... }) = eqns;
fun the_dtyps (Spec { dtyps, ... }) = dtyps;
fun the_cases (Spec { cases, ... }) = cases;
val map_history_concluded = map_spec o apfst;
-val map_eqns = map_spec o apsnd o apfst;
+val map_signatures = map_spec o apsnd o apfst o apfst;
+val map_eqns = map_spec o apsnd o apfst o apsnd;
val map_dtyps = map_spec o apsnd o apsnd o apfst;
val map_cases = map_spec o apsnd o apsnd o apsnd;
@@ -236,8 +252,8 @@
structure Code_Data = TheoryDataFun
(
type T = spec * data Unsynchronized.ref;
- val empty = (make_spec (false,
- (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
+ val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
+ (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
val extend = copy;
fun merge _ ((spec1, _), (spec2, _)) =
@@ -334,7 +350,44 @@
(* constants *)
-fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
+fun arity_number thy tyco = case Symtab.lookup ((fst o the_signatures o the_exec) thy) tyco
+ of SOME n => n
+ | NONE => Sign.arity_number thy tyco;
+
+fun build_tsig thy =
+ let
+ val (tycos, _) = (the_signatures o the_exec) thy;
+ val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
+ |> apsnd (Symtab.fold (fn (tyco, n) =>
+ Symtab.update (tyco, Type.LogicalType n)) tycos);
+ in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
+
+fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
+
+fun read_signature thy = cert_signature thy o Type.strip_sorts
+ o Syntax.parse_typ (ProofContext.init thy);
+
+fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
+
+fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy);
+
+fun const_typ thy c = case lookup_typ thy c
+ of SOME ty => ty
+ | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
+
+fun subst_signature thy c ty =
+ let
+ fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
+ fold2 mk_subst tys1 tys2
+ | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
+ in case lookup_typ thy c
+ of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
+ | NONE => ty
+ end;
+
+fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
+
+fun args_number thy = length o fst o strip_type o const_typ thy;
(* datatypes *)
@@ -355,9 +408,10 @@
val _ = if length tfrees <> length vs
then no_constr "type variables missing in datatype" c_ty else ();
in (tyco, vs) end;
- fun ty_sorts (c, ty) =
+ fun ty_sorts (c, raw_ty) =
let
- val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
+ val ty = subst_signature thy c raw_ty;
+ val ty_decl = (Logic.unvarifyT o const_typ thy) c;
val (tyco, _) = last_typ (c, ty) ty_decl;
val (_, vs) = last_typ (c, ty) ty;
in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
@@ -382,13 +436,13 @@
fun get_datatype thy tyco =
case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
of (_, spec) :: _ => spec
- | [] => Sign.arity_number thy tyco
+ | [] => arity_number thy tyco
|> Name.invents Name.context Name.aT
|> map (rpair [])
|> rpair [];
fun get_datatype_of_constr thy c =
- case (snd o strip_type o Sign.the_const_type thy) c
+ case (snd o strip_type o const_typ thy) c
of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
then SOME tyco else NONE
| _ => NONE;
@@ -446,21 +500,25 @@
("Variable with application on left hand side of equation\n"
^ Display.string_of_thm_global thy thm)
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
- | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
- then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
- then ()
- else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
- ^ Display.string_of_thm_global thy thm)
- else bad_thm
- ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
- ^ Display.string_of_thm_global thy thm);
+ | check n (Const (c_ty as (_, ty))) =
+ let
+ val c' = AxClass.unoverload_const thy c_ty
+ in if n = (length o fst o strip_type o subst_signature thy c') ty
+ then if not proper orelse is_constr_pat c'
+ then ()
+ else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
+ ^ Display.string_of_thm_global thy thm)
+ else bad_thm
+ ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
+ ^ Display.string_of_thm_global thy thm)
+ end;
val _ = map (check 0) args;
val _ = if not proper orelse is_linear thm then ()
else bad_thm ("Duplicate variables on left hand side of equation\n"
^ Display.string_of_thm_global thy thm);
val _ = if (is_none o AxClass.class_of_param thy) c
then ()
- else bad_thm ("Polymorphic constant as head in equation\n"
+ else bad_thm ("Overloaded constant as head in equation\n"
^ Display.string_of_thm_global thy thm)
val _ = if not (is_constr thy c)
then ()
@@ -488,30 +546,35 @@
fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy;
-(*those following are permissive wrt. to overloaded constants!*)
+val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
-val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
fun const_typ_eqn thy thm =
let
val (c, ty) = head_eqn thm;
val c' = AxClass.unoverload_const thy (c, ty);
+ (*permissive wrt. to overloaded constants!*)
in (c', ty) end;
+
fun const_eqn thy = fst o const_typ_eqn thy;
-fun typscheme thy (c, ty) =
+fun raw_typscheme thy (c, ty) =
(map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
+
+fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty);
+
fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
+
fun typscheme_eqns thy c [] =
let
- val raw_ty = Sign.the_const_type thy c;
+ val raw_ty = const_typ thy c;
val tvars = Term.add_tvar_namesT raw_ty [];
val tvars' = case AxClass.class_of_param thy c
of SOME class => [TFree (Name.aT, [class])]
| NONE => Name.invent_list [] Name.aT (length tvars)
|> map (fn v => TFree (v, []));
val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
- in typscheme thy (c, ty) end
- | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
+ in raw_typscheme thy (c, ty) end
+ | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
fun assert_eqns_const thy c eqns =
let
@@ -639,6 +702,34 @@
(** declaring executable ingredients **)
+(* constant signatures *)
+
+fun add_type tyco thy =
+ case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco
+ of SOME (Type.Abbreviation (vs, _, _)) =>
+ (map_exec_purge NONE o map_signatures o apfst)
+ (Symtab.update (tyco, length vs)) thy
+ | _ => error ("No such type abbreviation: " ^ quote tyco);
+
+fun add_type_cmd s thy = add_type (Sign.intern_type thy s) thy;
+
+fun gen_add_signature prep_const prep_signature (raw_c, raw_ty) thy =
+ let
+ val c = prep_const thy raw_c;
+ val ty = prep_signature thy raw_ty;
+ val ty' = expand_signature thy ty;
+ val ty'' = Sign.the_const_type thy c;
+ val _ = if typ_equiv (ty', ty'') then () else
+ error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty);
+ in
+ thy
+ |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty))
+ end;
+
+val add_signature = gen_add_signature (K I) cert_signature;
+val add_signature_cmd = gen_add_signature read_const read_signature;
+
+
(* datatypes *)
structure Type_Interpretation =
--- a/src/Pure/type.ML Fri Dec 04 12:17:43 2009 +0100
+++ b/src/Pure/type.ML Fri Dec 04 15:20:24 2009 +0100
@@ -19,6 +19,7 @@
types: decl Name_Space.table,
log_types: string list}
val empty_tsig: tsig
+ val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig
val defaultS: tsig -> sort
val logical_types: tsig -> string list
val eq_sort: tsig -> sort * sort -> bool
--- a/src/Tools/Code/code_preproc.ML Fri Dec 04 12:17:43 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML Fri Dec 04 15:20:24 2009 +0100
@@ -111,7 +111,7 @@
-- perhaps by means of upcoming code certificates with a corresponding
preprocessor protocol*);
-fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
+fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
fun eqn_conv conv =
let
@@ -148,7 +148,7 @@
in
ct
|> Simplifier.rewrite pre
- |> rhs_conv (AxClass.unoverload_conv thy)
+ |> trans_conv_rule (AxClass.unoverload_conv thy)
end;
fun postprocess_conv thy ct =
@@ -157,7 +157,7 @@
in
ct
|> AxClass.overload_conv thy
- |> rhs_conv (Simplifier.rewrite post)
+ |> trans_conv_rule (Simplifier.rewrite post)
end;
fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
--- a/src/Tools/Code/code_thingol.ML Fri Dec 04 12:17:43 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML Fri Dec 04 15:20:24 2009 +0100
@@ -711,7 +711,7 @@
and translate_eqn thy algbr eqngr (thm, proper) =
let
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
- o Logic.unvarify o prop_of) thm;
+ o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
in
fold_map (translate_term thy algbr eqngr (SOME thm)) args
##>> translate_term thy algbr eqngr (SOME thm) rhs
@@ -888,7 +888,7 @@
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr) vs
##>> translate_typ thy algbr eqngr ty
- ##>> translate_term thy algbr eqngr NONE t
+ ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
#>> (fn ((vs, ty), t) => Fun
(Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
fun term_value (dep, (naming, program1)) =