--- a/NEWS Mon Mar 22 10:25:07 2010 +0100
+++ b/NEWS Mon Mar 22 10:25:44 2010 +0100
@@ -290,6 +290,10 @@
Pretty.pp argument to merge, which is absent in the standard
Theory_Data version.
+* Renamed varify/unvarify operations to varify_global/unvarify_global
+to emphasize that these only work in a global situation (which is
+quite rare).
+
*** System ***
--- a/src/HOL/Algebra/AbelCoset.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,13 +1,11 @@
-(*
- Title: HOL/Algebra/AbelCoset.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/AbelCoset.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory AbelCoset
imports Coset Ring
begin
-
subsection {* More Lifting from Groups to Abelian Groups *}
subsubsection {* Definitions *}
@@ -17,36 +15,41 @@
no_notation Plus (infixr "<+>" 65)
-constdefs (structure G)
+definition
a_r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "+>\<index>" 60)
- "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+definition
a_l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<+\<index>" 60)
- "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+definition
A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("a'_rcosets\<index> _" [81] 80)
- "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+definition
set_add :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
- "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+definition
A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("a'_set'_inv\<index> _" [81] 80)
- "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
-constdefs (structure G)
- a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
- ("racong\<index> _")
- "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+definition
+ a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("racong\<index> _")
+ where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
+definition
+ A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
--{*Actually defined for groups rather than monoids*}
- "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
-definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>
- ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where
+definition
+ a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
--{*the kernel of a homomorphism (additive)*}
- "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+ where "a_kernel G H h =
+ kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
+ \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
locale abelian_group_hom = G: abelian_group G + H: abelian_group H
for G (structure) and H (structure) +
@@ -515,6 +518,7 @@
text {* The isomorphism theorems have been omitted from lifting, at
least for now *}
+
subsubsection{*The First Isomorphism Theorem*}
text{*The quotient by the kernel of a homomorphism is isomorphic to the
@@ -524,7 +528,7 @@
a_kernel_def kernel_def
lemma a_kernel_def':
- "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
+ "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
@@ -637,6 +641,7 @@
by (rule group_hom.FactGroup_iso[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+
subsubsection {* Cosets *}
text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
@@ -721,7 +726,6 @@
folded A_RCOSETS_def, simplified monoid_record_simps])
-
subsubsection {* Addition of Subgroups *}
lemma (in abelian_monoid) set_add_closed:
--- a/src/HOL/Algebra/Bij.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Bij.thy Mon Mar 22 10:25:44 2010 +0100
@@ -2,17 +2,20 @@
Author: Florian Kammueller, with new proofs by L C Paulson
*)
-theory Bij imports Group begin
-
+theory Bij
+imports Group
+begin
section {* Bijections of a Set, Permutation and Automorphism Groups *}
-definition Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" where
+definition
+ Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
--{*Only extensional functions, since otherwise we get too many.*}
- "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
+ where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
-definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
- "BijGroup S \<equiv>
+definition
+ BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ where "BijGroup S =
\<lparr>carrier = Bij S,
mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
one = \<lambda>x \<in> S. x\<rparr>"
@@ -69,11 +72,13 @@
done
-definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
- "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
+definition
+ auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
+ where "auto G = hom G G \<inter> Bij (carrier G)"
-definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
- "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
+definition
+ AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+ where "AutoGroup G = BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
--- a/src/HOL/Algebra/Congruence.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,10 +1,11 @@
-(*
- Title: Algebra/Congruence.thy
- Author: Clemens Ballarin, started 3 January 2008
- Copyright: Clemens Ballarin
+(* Title: Algebra/Congruence.thy
+ Author: Clemens Ballarin, started 3 January 2008
+ Copyright: Clemens Ballarin
*)
-theory Congruence imports Main begin
+theory Congruence
+imports Main
+begin
section {* Objects *}
@@ -19,21 +20,25 @@
record 'a eq_object = "'a partial_object" +
eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
-constdefs (structure S)
+definition
elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
- "x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)"
+ where "x .\<in>\<^bsub>S\<^esub> A \<longleftrightarrow> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
+definition
set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
- "A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))"
+ where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
+definition
eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
- "class_of x == {y \<in> carrier S. x .= y}"
+ where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
+definition
eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
- "closure_of A == {y \<in> carrier S. y .\<in> A}"
+ where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
+definition
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
- "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
+ where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
abbreviation
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
--- a/src/HOL/Algebra/Coset.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,28 +1,34 @@
(* Title: HOL/Algebra/Coset.thy
- Author: Florian Kammueller, with new proofs by L C Paulson, and
- Stephan Hohe
+ Author: Florian Kammueller
+ Author: L C Paulson
+ Author: Stephan Hohe
*)
-theory Coset imports Group begin
-
+theory Coset
+imports Group
+begin
section {*Cosets and Quotient Groups*}
-constdefs (structure G)
+definition
r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
- "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
+ where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
+definition
l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60)
- "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
+ where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
+definition
RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80)
- "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
+ where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
+definition
set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
- "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
+ where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
+definition
SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("set'_inv\<index> _" [81] 80)
- "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
+ where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
locale normal = subgroup + group +
@@ -589,10 +595,9 @@
subsubsection{*An Equivalence Relation*}
-constdefs (structure G)
- r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
- ("rcong\<index> _")
- "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
+definition
+ r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("rcong\<index> _")
+ where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
lemma (in subgroup) equiv_rcong:
@@ -650,6 +655,7 @@
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
qed
+
subsubsection{*Two Distinct Right Cosets are Disjoint*}
lemma (in group) rcos_equation:
@@ -675,6 +681,7 @@
done
qed
+
subsection {* Further lemmas for @{text "r_congruent"} *}
text {* The relation is a congruence *}
@@ -751,8 +758,9 @@
subsection {*Order of a Group and Lagrange's Theorem*}
-definition order :: "('a, 'b) monoid_scheme \<Rightarrow> nat" where
- "order S \<equiv> card (carrier S)"
+definition
+ order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
+ where "order S = card (carrier S)"
lemma (in group) rcosets_part_G:
assumes "subgroup H G"
@@ -821,10 +829,10 @@
subsection {*Quotient Groups: Factorization of a Group*}
-definition FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65) where
+definition
+ FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
--{*Actually defined for groups rather than monoids*}
- "FactGroup G H \<equiv>
- \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
+ where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
lemma (in normal) setmult_closed:
"\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
@@ -887,10 +895,10 @@
text{*The quotient by the kernel of a homomorphism is isomorphic to the
range of that homomorphism.*}
-definition kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
- ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where
+definition
+ kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
--{*the kernel of a homomorphism*}
- "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
+ where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
apply (rule subgroup.intro)
--- a/src/HOL/Algebra/Divisibility.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: Divisibility in monoids and rings
- Author: Clemens Ballarin, started 18 July 2008
+(* Title: Divisibility in monoids and rings
+ Author: Clemens Ballarin, started 18 July 2008
Based on work by Stephan Hohe.
*)
@@ -156,34 +155,35 @@
show "a \<in> Units G" by (simp add: Units_def, fast)
qed
+
subsection {* Divisibility and Association *}
subsubsection {* Function definitions *}
-constdefs (structure G)
+definition
factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
- "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
-
-constdefs (structure G)
+ where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"
+
+definition
associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
- "a \<sim> b == a divides b \<and> b divides a"
+ where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
abbreviation
"division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
-constdefs (structure G)
+definition
properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
- "properfactor G a b == a divides b \<and> \<not>(b divides a)"
-
-constdefs (structure G)
+ where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
+
+definition
irreducible :: "[_, 'a] \<Rightarrow> bool"
- "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
-
-constdefs (structure G)
- prime :: "[_, 'a] \<Rightarrow> bool"
- "prime G p == p \<notin> Units G \<and>
- (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
-
+ where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
+
+definition
+ prime :: "[_, 'a] \<Rightarrow> bool" where
+ "prime G p \<longleftrightarrow>
+ p \<notin> Units G \<and>
+ (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
subsubsection {* Divisibility *}
@@ -1041,20 +1041,21 @@
subsubsection {* Function definitions *}
-constdefs (structure G)
+definition
factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
- "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
-
+ where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
+
+definition
wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
- "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
+ where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
abbreviation
- list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
- "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
-
-constdefs (structure G)
+ list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
+ where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
+
+definition
essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
- "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
+ where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
locale factorial_monoid = comm_monoid_cancel +
@@ -1901,8 +1902,8 @@
abbreviation
"assocs G x == eq_closure_of (division_rel G) {x}"
-constdefs (structure G)
- "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
+definition
+ "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
text {* Helper lemmas *}
@@ -2615,24 +2616,26 @@
subsubsection {* Definitions *}
-constdefs (structure G)
+definition
isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)
- "x gcdof a b \<equiv> x divides a \<and> x divides b \<and>
- (\<forall>y\<in>carrier G. (y divides a \<and> y divides b \<longrightarrow> y divides x))"
-
+ where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
+ (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
+
+definition
islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)
- "x lcmof a b \<equiv> a divides x \<and> b divides x \<and>
- (\<forall>y\<in>carrier G. (a divides y \<and> b divides y \<longrightarrow> x divides y))"
-
-constdefs (structure G)
+ where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
+ (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
+
+definition
somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof a b"
-
+ where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"
+
+definition
somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
-
-constdefs (structure G)
- "SomeGcd G A == inf (division_rel G) A"
+ where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
+
+definition
+ "SomeGcd G A = inf (division_rel G) A"
locale gcd_condition_monoid = comm_monoid_cancel +
@@ -3630,9 +3633,10 @@
text {* Number of factors for wellfoundedness *}
-definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
- "factorcount G a == THE c. (ALL as. set as \<subseteq> carrier G \<and>
- wfactors G as a \<longrightarrow> c = length as)"
+definition
+ factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
+ "factorcount G a =
+ (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"
lemma (in monoid) ee_length:
assumes ee: "essentially_equal G as bs"
--- a/src/HOL/Algebra/Exponent.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Exponent.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Algebra/Exponent.thy
- Author: Florian Kammueller, with new proofs by L C Paulson
+ Author: Florian Kammueller
+ Author: L C Paulson
- exponent p s yields the greatest power of p that divides s.
+exponent p s yields the greatest power of p that divides s.
*)
theory Exponent
@@ -12,8 +13,9 @@
subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
-definition exponent :: "nat => nat => nat" where
-"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
+definition
+ exponent :: "nat => nat => nat"
+ where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
text{*Prime Theorems*}
--- a/src/HOL/Algebra/FiniteProduct.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Mon Mar 22 10:25:44 2010 +0100
@@ -4,8 +4,9 @@
This file is largely based on HOL/Finite_Set.thy.
*)
-theory FiniteProduct imports Group begin
-
+theory FiniteProduct
+imports Group
+begin
subsection {* Product Operator for Commutative Monoids *}
@@ -26,8 +27,9 @@
inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
-definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
- "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
+definition
+ foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+ where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
lemma foldSetD_closed:
"[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D
@@ -285,11 +287,12 @@
subsubsection {* Products over Finite Sets *}
-constdefs (structure G)
+definition
finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
- "finprod G f A == if finite A
- then foldD (carrier G) (mult G o f) \<one> A
- else undefined"
+ where "finprod G f A =
+ (if finite A
+ then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
+ else undefined)"
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
--- a/src/HOL/Algebra/Group.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: HOL/Algebra/Group.thy
- Author: Clemens Ballarin, started 4 February 2003
+(* Title: HOL/Algebra/Group.thy
+ Author: Clemens Ballarin, started 4 February 2003
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
*)
@@ -9,7 +8,6 @@
imports Lattice FuncSet
begin
-
section {* Monoids and Groups *}
subsection {* Definitions *}
@@ -22,22 +20,29 @@
mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
one :: 'a ("\<one>\<index>")
-constdefs (structure G)
+definition
m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
- "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
+ where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
+definition
Units :: "_ => 'a set"
--{*The set of invertible elements*}
- "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
+ where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
consts
- pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
+ pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
+
+overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
+begin
+ definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+end
-defs (overloaded)
- nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
- int_pow_def: "pow G a z ==
- let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
- in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
+overloading int_pow == "pow :: [_, 'a, int] => 'a"
+begin
+ definition "int_pow G a z =
+ (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+ in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+end
locale monoid =
fixes G (structure)
@@ -478,10 +483,12 @@
subsection {* Direct Products *}
-definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
- "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
- mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
- one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
+definition
+ DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
+ "G \<times>\<times> H =
+ \<lparr>carrier = carrier G \<times> carrier H,
+ mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
+ one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
lemma DirProd_monoid:
assumes "monoid G" and "monoid H"
@@ -534,9 +541,9 @@
subsection {* Homomorphisms and Isomorphisms *}
-constdefs (structure G and H)
- hom :: "_ => _ => ('a => 'b) set"
- "hom G H ==
+definition
+ hom :: "_ => _ => ('a => 'b) set" where
+ "hom G H =
{h. h \<in> carrier G -> carrier H &
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
@@ -544,8 +551,9 @@
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
by (fastsimp simp add: hom_def compose_def)
-definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
- "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
+definition
+ iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
+ where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
lemma iso_refl: "(%x. x) \<in> G \<cong> G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
--- a/src/HOL/Algebra/Ideal.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: HOL/Algebra/CIdeal.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/CIdeal.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory Ideal
@@ -45,11 +44,12 @@
done
qed
+
subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
-constdefs (structure R)
+definition
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
- "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
+ where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
subsubsection {* Principal Ideals *}
@@ -71,6 +71,7 @@
show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
qed
+
subsubsection {* Maximal Ideals *}
locale maximalideal = ideal +
@@ -93,6 +94,7 @@
(rule is_ideal, rule I_notcarr, rule I_maximal)
qed
+
subsubsection {* Prime Ideals *}
locale primeideal = ideal + cring +
@@ -139,6 +141,7 @@
done
qed
+
subsection {* Special Ideals *}
lemma (in ring) zeroideal:
@@ -451,9 +454,9 @@
text {* Generation of Principal Ideals in Commutative Rings *}
-constdefs (structure R)
+definition
cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
- "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
+ where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
text {* genhideal (?) really generates an ideal *}
lemma (in cring) cgenideal_ideal:
@@ -867,6 +870,7 @@
qed
qed
+
subsection {* Derived Theorems *}
--"A non-zero cring that has only the two trivial ideals is a field"
--- a/src/HOL/Algebra/IntRing.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,13 +1,11 @@
-(*
- Title: HOL/Algebra/IntRing.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/IntRing.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory IntRing
imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
begin
-
section {* The Ring of Integers *}
subsection {* Some properties of @{typ int} *}
@@ -22,8 +20,9 @@
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
-definition int_ring :: "int ring" ("\<Z>") where
- "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+definition
+ int_ring :: "int ring" ("\<Z>") where
+ "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
lemma int_Zcarr [intro!, simp]:
"k \<in> carrier \<Z>"
@@ -48,6 +47,8 @@
apply (unfold int_ring_def, simp+)
done
*)
+
+
subsection {* Interpretations *}
text {* Since definitions of derived operations are global, their
@@ -323,8 +324,9 @@
subsection {* Ideals and the Modulus *}
-definition ZMod :: "int => int => int set" where
- "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
+definition
+ ZMod :: "int => int => int set"
+ where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
lemmas ZMod_defs =
ZMod_def genideal_def
@@ -405,8 +407,9 @@
subsection {* Factorization *}
-definition ZFact :: "int \<Rightarrow> int set ring" where
- "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
+definition
+ ZFact :: "int \<Rightarrow> int set ring"
+ where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
lemmas ZFact_defs = ZFact_def FactRing_def
--- a/src/HOL/Algebra/Lattice.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Lattice.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,12 +1,13 @@
-(*
- Title: HOL/Algebra/Lattice.thy
- Author: Clemens Ballarin, started 7 November 2003
- Copyright: Clemens Ballarin
+(* Title: HOL/Algebra/Lattice.thy
+ Author: Clemens Ballarin, started 7 November 2003
+ Copyright: Clemens Ballarin
Most congruence rules by Stephan Hohe.
*)
-theory Lattice imports Congruence begin
+theory Lattice
+imports Congruence
+begin
section {* Orders and Lattices *}
@@ -25,9 +26,9 @@
and le_cong:
"\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
-constdefs (structure L)
+definition
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
- "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
+ where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
subsubsection {* The order relation *}
@@ -102,12 +103,13 @@
subsubsection {* Upper and lower bounds of a set *}
-constdefs (structure L)
+definition
Upper :: "[_, 'a set] => 'a set"
- "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
+ where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
+definition
Lower :: "[_, 'a set] => 'a set"
- "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
+ where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
lemma Upper_closed [intro!, simp]:
"Upper L A \<subseteq> carrier L"
@@ -275,12 +277,13 @@
subsubsection {* Least and greatest, as predicate *}
-constdefs (structure L)
+definition
least :: "[_, 'a, 'a set] => bool"
- "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
+ where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
+definition
greatest :: "[_, 'a, 'a set] => bool"
- "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
+ where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
.\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
@@ -400,18 +403,21 @@
text {* Supremum and infimum *}
-constdefs (structure L)
+definition
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
- "\<Squnion>A == SOME x. least L x (Upper L A)"
+ where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
+definition
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
- "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
+ where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
+definition
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
- "x \<squnion> y == \<Squnion> {x, y}"
+ where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
+definition
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
- "x \<sqinter> y == \<Sqinter> {x, y}"
+ where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
subsection {* Lattices *}
@@ -981,12 +987,13 @@
shows "weak_complete_lattice L"
proof qed (auto intro: sup_exists inf_exists)
-constdefs (structure L)
+definition
top :: "_ => 'a" ("\<top>\<index>")
- "\<top> == sup L (carrier L)"
+ where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
+definition
bottom :: "_ => 'a" ("\<bottom>\<index>")
- "\<bottom> == inf L (carrier L)"
+ where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
lemma (in weak_complete_lattice) supI:
--- a/src/HOL/Algebra/Module.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Module.thy Mon Mar 22 10:25:44 2010 +0100
@@ -3,8 +3,9 @@
Copyright: Clemens Ballarin
*)
-theory Module imports Ring begin
-
+theory Module
+imports Ring
+begin
section {* Modules over an Abelian Group *}
--- a/src/HOL/Algebra/QuotRing.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: HOL/Algebra/QuotRing.thy
- Author: Stephan Hohe
+(* Title: HOL/Algebra/QuotRing.thy
+ Author: Stephan Hohe
*)
theory QuotRing
@@ -11,10 +10,10 @@
subsection {* Multiplication on Cosets *}
-constdefs (structure R)
+definition
rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
- "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
+ where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
text {* @{const "rcoset_mult"} fulfils the properties required by
@@ -89,11 +88,10 @@
subsection {* Quotient Ring Definition *}
-constdefs (structure R)
- FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
- (infixl "Quot" 65)
- "FactRing R I \<equiv>
- \<lparr>carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \<one>), zero = I, add = set_add R\<rparr>"
+definition
+ FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" (infixl "Quot" 65)
+ where "FactRing R I =
+ \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
subsection {* Factorization over General Ideals *}
@@ -181,6 +179,7 @@
done
qed
+
subsection {* Factorization over Prime Ideals *}
text {* The quotient ring generated by a prime ideal is a domain *}
--- a/src/HOL/Algebra/README.html Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/README.html Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOL/Algebra/ROOT.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/ROOT.ML Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- The Isabelle Algebraic Library
- $Id$
- Author: Clemens Ballarin, started 24 September 1999
+(* Author: Clemens Ballarin, started 24 September 1999
+
+The Isabelle Algebraic Library.
*)
(* Preliminaries from set and number theory *)
@@ -23,8 +22,7 @@
];
-(*** Old development, based on axiomatic type classes.
- Will be withdrawn in future. ***)
+(*** Old development, based on axiomatic type classes ***)
no_document use_thys [
"abstract/Abstract", (*The ring theory*)
--- a/src/HOL/Algebra/Ring.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,13 +1,12 @@
-(*
- Title: The algebraic hierarchy of rings
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
+(* Title: The algebraic hierarchy of rings
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
*)
theory Ring
imports FiniteProduct
-uses ("ringsimp.ML") begin
-
+uses ("ringsimp.ML")
+begin
section {* The Algebraic Hierarchy of Rings *}
@@ -19,12 +18,13 @@
text {* Derived operations. *}
-constdefs (structure R)
+definition
a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
- "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+ where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+definition
a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
- "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
+ where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
locale abelian_monoid =
fixes G (structure)
@@ -198,9 +198,9 @@
This definition makes it easy to lift lemmas from @{term finprod}.
*}
-definition finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
- "finsum G f A == finprod (| carrier = carrier G,
- mult = add G, one = zero G |) f A"
+definition
+ finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
+ "finsum G f A = finprod (| carrier = carrier G, mult = add G, one = zero G |) f A"
syntax
"_finsum" :: "index => idt => 'a set => 'b => 'b"
@@ -599,6 +599,7 @@
from R show ?thesis by algebra
qed
+
subsubsection {* Sums over Finite Sets *}
lemma (in ring) finsum_ldistr:
@@ -728,12 +729,13 @@
subsection {* Morphisms *}
-constdefs (structure R S)
+definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
- "ring_hom R S == {h. h \<in> carrier R -> carrier S &
+ where "ring_hom R S =
+ {h. h \<in> carrier R -> carrier S &
(ALL x y. x \<in> carrier R & y \<in> carrier R -->
- h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
- h \<one> = \<one>\<^bsub>S\<^esub>}"
+ h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
+ h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
lemma ring_hom_memI:
fixes R (structure) and S (structure)
--- a/src/HOL/Algebra/RingHom.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/RingHom.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: HOL/Algebra/RingHom.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/RingHom.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory RingHom
@@ -100,6 +99,7 @@
(rule R.is_cring, rule S.is_cring, rule homh)
qed
+
subsection {* The Kernel of a Ring Homomorphism *}
--"the kernel of a ring homomorphism is an ideal"
--- a/src/HOL/Algebra/Sylow.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/Sylow.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,9 +1,10 @@
(* Title: HOL/Algebra/Sylow.thy
- ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
*)
-theory Sylow imports Coset Exponent begin
+theory Sylow
+imports Coset Exponent
+begin
text {*
See also \cite{Kammueller-Paulson:1999}.
--- a/src/HOL/Algebra/UnivPoly.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- Title: HOL/Algebra/UnivPoly.thy
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
+(* Title: HOL/Algebra/UnivPoly.thy
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
Contributions, in particular on long division, by Jesus Aransay.
*)
@@ -10,7 +9,6 @@
imports Module RingHom
begin
-
section {* Univariate Polynomials *}
text {*
@@ -54,11 +52,12 @@
monom :: "['a, nat] => 'p"
coeff :: "['p, nat] => 'a"
-definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
- where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+definition
+ up :: "('a, 'm) ring_scheme => (nat => 'a) set"
+ where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
- where UP_def: "UP R == (|
+ where "UP R = (|
carrier = up R,
mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
@@ -428,7 +427,8 @@
using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
qed (simp_all add: R1 R2)
-subsection{*Polynomials over a commutative ring for a commutative ring*}
+
+subsection {*Polynomials over a commutative ring for a commutative ring*}
theorem UP_cring:
"cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
@@ -711,8 +711,9 @@
subsection {* The Degree Function *}
-definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
- where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
+definition
+ deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
+ where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
context UP_ring
begin
@@ -1173,8 +1174,8 @@
definition
eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
'a => 'b, 'b, nat => 'a] => 'b"
- where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
- \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i"
+ where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
+ \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
context UP
begin
@@ -1472,6 +1473,7 @@
lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>"
using lcoeff_nonzero [OF p_not_zero p_in_R] .
+
subsection{*The long division algorithm: some previous facts.*}
lemma coeff_minus [simp]:
@@ -1854,11 +1856,11 @@
by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
ring_hom_cring_axioms.intro UP_cring.intro)
-definition INTEG :: "int ring"
- where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+definition
+ INTEG :: "int ring"
+ where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
-lemma INTEG_cring:
- "cring INTEG"
+lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
zadd_zminus_inverse2 zadd_zmult_distrib)
--- a/src/HOL/Algebra/abstract/Abstract.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/Abstract.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- Summary theory of the development of abstract algebra
- $Id$
- Author: Clemens Ballarin, started 17 July 1997
+(* Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of abstract algebra.
*)
theory Abstract
--- a/src/HOL/Algebra/abstract/Factor.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,10 +1,11 @@
-(*
- Factorisation within a factorial domain
- $Id$
- Author: Clemens Ballarin, started 25 November 1997
+(* Author: Clemens Ballarin, started 25 November 1997
+
+Factorisation within a factorial domain.
*)
-theory Factor imports Ring2 begin
+theory Factor
+imports Ring2
+begin
definition
Factorisation :: "['a::ring, 'a list, 'a] => bool" where
--- a/src/HOL/Algebra/abstract/Field.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/Field.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,9 +1,11 @@
-(*
- Properties of abstract class field
- Author: Clemens Ballarin, started 15 November 1997
+(* Author: Clemens Ballarin, started 15 November 1997
+
+Properties of abstract class field.
*)
-theory Field imports Factor PID begin
+theory Field
+imports Factor PID
+begin
instance field < "domain"
apply intro_classes
--- a/src/HOL/Algebra/abstract/Ideal2.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,9 +1,11 @@
-(*
- Ideals for commutative rings
- Author: Clemens Ballarin, started 24 September 1999
+(* Author: Clemens Ballarin, started 24 September 1999
+
+Ideals for commutative rings.
*)
-theory Ideal2 imports Ring2 begin
+theory Ideal2
+imports Ring2
+begin
definition
is_ideal :: "('a::ring) set => bool" where
@@ -28,8 +30,8 @@
(* is_ideal *)
lemma is_idealI:
- "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
- !! a. a:I ==> - a : I; 0 : I;
+ "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
+ !! a. a:I ==> - a : I; 0 : I;
!! a r. a:I ==> a * r : I |] ==> is_ideal I"
unfolding is_ideal_def by blast
@@ -241,7 +243,7 @@
apply force
done
-lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
+lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
==> is_ideal (Union (I`UNIV))"
apply (rule is_idealI)
apply auto
--- a/src/HOL/Algebra/abstract/PID.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/PID.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,9 +1,11 @@
-(*
- Principle ideal domains
- Author: Clemens Ballarin, started 5 October 1999
+(* Author: Clemens Ballarin, started 5 October 1999
+
+Principle ideal domains.
*)
-theory PID imports Ideal2 begin
+theory PID
+imports Ideal2
+begin
instance pid < factorial
apply intro_classes
--- a/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 22 10:25:44 2010 +0100
@@ -30,16 +30,17 @@
and divide_def: "a / b = a * inverse b"
begin
-definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
- assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
+definition
+ assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
+ where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
-definition irred :: "'a \<Rightarrow> bool" where
- irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
- & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
+definition
+ irred :: "'a \<Rightarrow> bool" where
+ "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
-definition prime :: "'a \<Rightarrow> bool" where
- prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
- & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+definition
+ prime :: "'a \<Rightarrow> bool" where
+ "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
end
--- a/src/HOL/Algebra/abstract/RingHomo.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- Ring homomorphism
- $Id$
- Author: Clemens Ballarin, started 15 April 1997
+(* Author: Clemens Ballarin, started 15 April 1997
+
+Ring homomorphism.
*)
header {* Ring homomorphism *}
--- a/src/HOL/Algebra/document/root.tex Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/document/root.tex Mon Mar 22 10:25:44 2010 +0100
@@ -1,5 +1,3 @@
-% $Id$
-
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage{isabelle,isabellesym}
--- a/src/HOL/Algebra/poly/LongDiv.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,9 +1,11 @@
-(*
- Experimental theory: long division of polynomials
- Author: Clemens Ballarin, started 23 June 1999
+(* Author: Clemens Ballarin, started 23 June 1999
+
+Experimental theory: long division of polynomials.
*)
-theory LongDiv imports PolyHomo begin
+theory LongDiv
+imports PolyHomo
+begin
definition
lcoeff :: "'a::ring up => 'a" where
--- a/src/HOL/Algebra/poly/PolyHomo.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,10 +1,11 @@
-(*
- Universal property and evaluation homomorphism of univariate polynomials
- $Id$
- Author: Clemens Ballarin, started 15 April 1997
+(* Author: Clemens Ballarin, started 15 April 1997
+
+Universal property and evaluation homomorphism of univariate polynomials.
*)
-theory PolyHomo imports UnivPoly2 begin
+theory PolyHomo
+imports UnivPoly2
+begin
definition
EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
--- a/src/HOL/Algebra/poly/Polynomial.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/poly/Polynomial.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- Summary theory of the development of (not instantiated) polynomials
- $Id$
- Author: Clemens Ballarin, started 17 July 1997
+(* Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of (not instantiated) polynomials.
*)
theory Polynomial
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Mon Mar 22 10:25:44 2010 +0100
@@ -1,7 +1,6 @@
-(*
- Title: Univariate Polynomials
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
+(* Title: Univariate Polynomials
+ Author: Clemens Ballarin, started 9 December 1996
+ Copyright: Clemens Ballarin
*)
header {* Univariate Polynomials *}
@@ -15,6 +14,7 @@
declare strong_setsum_cong [cong]
+
section {* Definition of type up *}
definition
@@ -47,16 +47,16 @@
section {* Constants *}
definition
- coeff :: "['a up, nat] => ('a::zero)" where
- "coeff p n = Rep_UP p n"
+ coeff :: "['a up, nat] => ('a::zero)"
+ where "coeff p n = Rep_UP p n"
definition
- monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where
- "monom a n = Abs_UP (%i. if i=n then a else 0)"
+ monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
+ where "monom a n = Abs_UP (%i. if i=n then a else 0)"
definition
- smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where
- "a *s p = Abs_UP (%i. a * Rep_UP p i)"
+ smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70)
+ where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
proof -
@@ -132,7 +132,7 @@
begin
definition
- up_mult_def: "p * q = Abs_UP (%n::nat. setsum
+ up_mult_def: "p * q = Abs_UP (%n::nat. setsum
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
instance ..
@@ -149,7 +149,7 @@
THE x. a * x = 1 else 0)"
definition
- up_divide_def: "(a :: 'a up) / b = a * inverse b"
+ up_divide_def: "(a :: 'a up) / b = a * inverse b"
instance ..
@@ -479,11 +479,12 @@
finally show ?thesis .
qed
+
section {* The degree function *}
definition
- deg :: "('a::zero) up => nat" where
- "deg p = (LEAST n. bound n (coeff p))"
+ deg :: "('a::zero) up => nat"
+ where "deg p = (LEAST n. bound n (coeff p))"
lemma deg_aboveI:
"(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
--- a/src/HOL/Algebra/ringsimp.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Mon Mar 22 10:25:44 2010 +0100
@@ -1,4 +1,4 @@
-(* Author: Clemens Ballarin
+(* Author: Clemens Ballarin
Normalisation method for locales ring and cring.
*)
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 10:25:44 2010 +0100
@@ -63,9 +63,8 @@
THEN' Boogie_Tactics.drop_assert_at_tac
THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
in
-fun boogie_vc (vc_name, vc_opts) lthy =
+fun boogie_vc (vc_name, vc_opts) thy =
let
- val thy = ProofContext.theory_of lthy
val vc = get_vc thy vc_name
fun extract vc l =
@@ -92,16 +91,16 @@
| _ => (pair ts, K I))
val discharge = fold (Boogie_VCs.discharge o pair vc_name)
- fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
+ fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
| after_qed _ = I
in
- lthy
+ ProofContext.init thy
|> fold Variable.auto_fixes ts
- |> (fn lthy1 => lthy1
+ |> (fn ctxt1 => ctxt1
|> prepare
- |-> (fn us => fn lthy2 => lthy2
+ |-> (fn us => fn ctxt2 => ctxt2
|> Proof.theorem_i NONE (fn thmss => fn ctxt =>
- let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
+ let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
end
@@ -300,7 +299,7 @@
"Enter into proof mode for a specific verification condition."
OuterKeyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
- (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))
+ (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
val quick_timeout = 5
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 10:25:44 2010 +0100
@@ -238,10 +238,14 @@
|> split_list_kind thy o Termtab.dest
in
fun add_axioms verbose axs thy =
- let val (used, new) = mark_axioms thy (name_axioms axs)
+ let
+ val (used, new) = mark_axioms thy (name_axioms axs)
+ fun add (n, t) =
+ Specification.axiomatization [] [((Binding.name n, []), [t])] #>>
+ hd o hd o snd
in
thy
- |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new)
+ |> fold_map add new
|-> Context.theory_map o fold Boogie_Axioms.add_thm
|> log verbose "The following axioms were added:" (map fst new)
|> (fn thy' => log verbose "The following axioms already existed:"
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 10:25:44 2010 +0100
@@ -27,6 +27,9 @@
val state_of_vc: theory -> string -> string list * string list
val close: theory -> theory
val is_closed: theory -> bool
+
+ val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
+ theory -> theory
end
structure Boogie_VCs: BOOGIE_VCS =
@@ -252,30 +255,35 @@
(* the VC store *)
-fun err_vcs () = error "undischarged Boogie verification conditions found"
+fun err_unfinished () = error "An unfinished Boogie environment is still open."
+
+fun err_vcs names = error (Pretty.string_of
+ (Pretty.big_list "Undischarged Boogie verification conditions found:"
+ (map Pretty.str names)))
structure VCs = Theory_Data
(
- type T = (vc * thm) Symtab.table option
+ type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
val empty = NONE
val extend = I
fun merge (NONE, NONE) = NONE
- | merge _ = err_vcs ()
+ | merge _ = err_unfinished ()
)
-fun prep thy t = vc_of_term t |> (fn vc => (vc, thm_of thy vc))
+fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))
fun set vcs thy = VCs.map (fn
- NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs))
- | SOME _ => err_vcs ()) thy
+ NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
+ | SOME _ => err_unfinished ()) thy
fun lookup thy name =
(case VCs.get thy of
- SOME vcs => Option.map fst (Symtab.lookup vcs name)
+ SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
| NONE => NONE)
fun discharge (name, prf) =
- VCs.map (Option.map (Symtab.map_entry name (join prf)))
+ let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
+ in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end
datatype state = Proved | NotProved | PartiallyProved
@@ -284,21 +292,35 @@
SOME vc => names_of vc
| NONE => ([], []))
+fun state_of_vc' (vc, _) =
+ (case names_of vc of
+ ([], _) => Proved
+ | (_, []) => NotProved
+ | (_, _) => PartiallyProved)
+
fun state_of thy =
(case VCs.get thy of
- SOME vcs => Symtab.dest vcs |> map (apsnd (fst #> names_of #> (fn
- ([], _) => Proved
- | (_, []) => NotProved
- | (_, _) => PartiallyProved)))
+ SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
| NONE => [])
+fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t
+
fun close thy = thy |> VCs.map (fn
- SOME _ =>
- if forall (fn (_, Proved) => true | _ => false) (state_of thy)
- then NONE
- else err_vcs ()
+ SOME (vcs, g) =>
+ let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
+ in
+ Symtab.dest vcs
+ |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
+ |> (fn names => if null names then NONE else err_vcs names)
+ end
| NONE => NONE)
val is_closed = is_none o VCs.get
+fun rewrite_vcs f g thy =
+ let
+ fun rewr (_, (t, _)) = vc_of_term (f thy t)
+ |> (fn vc => (vc, (t, thm_of thy vc)))
+ in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
+
end
--- a/src/HOL/Code_Evaluation.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy Mon Mar 22 10:25:44 2010 +0100
@@ -87,13 +87,14 @@
let
val t = list_comb (Const (c, tys ---> ty),
map Free (Name.names Name.context "a" tys));
- val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
- (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+ val (arg, rhs) =
+ pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+ (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
val cty = Thm.ctyp_of thy ty;
in
@{thm term_of_anything}
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
- |> Thm.varifyT
+ |> Thm.varifyT_global
end;
fun add_term_of_code tyco raw_vs raw_cs thy =
let
@@ -131,7 +132,7 @@
in
@{thm term_of_anything}
|> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
- |> Thm.varifyT
+ |> Thm.varifyT_global
end;
fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
let
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Mar 22 10:25:44 2010 +0100
@@ -3438,7 +3438,7 @@
| mk_result prec NONE = @{term "UNIV :: real set"}
fun realify t = let
- val t = Logic.varify t
+ val t = Logic.varify_global t
val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t [])
val t = Term.subst_TVars m t
in t end
--- a/src/HOL/Imperative_HOL/Array.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Mon Mar 22 10:25:44 2010 +0100
@@ -163,7 +163,7 @@
code_type array (SML "_/ array")
code_const Array (SML "raise/ (Fail/ \"bare Array\")")
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
-code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
+code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
@@ -177,7 +177,7 @@
code_type array (OCaml "_/ array")
code_const Array (OCaml "failwith/ \"bare Array\"")
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
-code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
+code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
--- a/src/HOL/Import/proof_kernel.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML Mon Mar 22 10:25:44 2010 +0100
@@ -1418,7 +1418,7 @@
val _ = message "INST_TYPE:"
val _ = if_debug pth hth
val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
- val th1 = Thm.varifyT th
+ val th1 = Thm.varifyT_global th
val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
val tyinst = map (fn (bef, iS) =>
(case try (Lib.assoc (TFree bef)) lambda of
@@ -2028,7 +2028,7 @@
names'
(thy1,th)
val _ = ImportRecorder.add_specification names' th
- val res' = Thm.unvarify res
+ val res' = Thm.unvarify_global res
val hth = HOLThm(rens,res')
val rew = rewrite_hol4_term (concl_of res') thy'
val th = equal_elim rew res'
--- a/src/HOL/Import/shuffler.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Import/shuffler.ML Mon Mar 22 10:25:44 2010 +0100
@@ -265,7 +265,7 @@
let
val cU = ctyp_of thy U
val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
- val (rens, thm') = Thm.varifyT'
+ val (rens, thm') = Thm.varifyT_global'
(remove (op = o apsnd fst) name tfrees) thm
val mid =
case rens of
@@ -592,7 +592,7 @@
fun process [] = NONE
| process ((name,th)::thms) =
let
- val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
+ val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
val triv_th = trivial rhs
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
--- a/src/HOL/Library/Infinite_Set.thy Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Mon Mar 22 10:25:44 2010 +0100
@@ -52,6 +52,9 @@
lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
by simp
+lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+ by simp
+
lemma infinite_super:
assumes T: "S \<subseteq> T" and S: "infinite S"
shows "infinite T"
--- a/src/HOL/Mutabelle/mutabelle.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Mon Mar 22 10:25:44 2010 +0100
@@ -218,7 +218,7 @@
val typeSignature = #tsig (Sign.rep_sg consSig)
in
if ((consNameStr = forbNameStr)
- andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT forbType))))
+ andalso (Type.typ_instance typeSignature (consType,(Logic.varifyT_global forbType))))
then true
else in_list_forb consSig (consNameStr,consType) xs
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Mar 22 10:25:44 2010 +0100
@@ -849,7 +849,7 @@
fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
let
- val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
+ val _ $ (_ $ (Rep $ x)) = Logic.unvarify_global (prop_of th);
val Type ("fun", [T, U]) = fastype_of Rep;
val permT = mk_permT (Type (atom, []));
val pi = Free ("pi", permT);
@@ -1394,7 +1394,7 @@
(pnames ~~ map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induct_aux)))) @
map (fn (_, f) =>
- let val f' = Logic.varify f
+ let val f' = Logic.varify_global f
in (cterm_of thy9 f',
cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
end) fresh_fs) induct_aux;
@@ -1677,14 +1677,14 @@
val induct_aux_rec = Drule.cterm_instantiate
(map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
- (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
+ (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
fresh_fs @
map (fn (((P, T), (x, U)), Q) =>
- (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
+ (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
(pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
- map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
+ map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
rec_unique_frees)) induct_aux;
fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
--- a/src/HOL/SMT/Tools/smt_translate.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML Mon Mar 22 10:25:44 2010 +0100
@@ -126,11 +126,11 @@
let
fun dest (t, bn) =
let val (n, T) = Term.dest_Const t
- in (n, (Logic.varifyT T, K (SOME o pair bn))) end
+ in (n, (Logic.varifyT_global T, K (SOME o pair bn))) end
in Symtab.make (AList.group (op =) (map dest entries)) end
fun builtin_add (t, f) tab =
- let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
+ let val (n, T) = apsnd Logic.varifyT_global (Term.dest_Const t)
in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
fun builtin_lookup tab thy (n, T) ts =
--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Mar 22 10:25:44 2010 +0100
@@ -46,7 +46,7 @@
in
SOME {case_name = case_name,
constructors = map (fn (cname, dts') =>
- Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
+ Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
end
| NONE => NONE;
@@ -87,7 +87,7 @@
val (_, Ty) = dest_Const c
val Ts = binder_types Ty;
val names = Name.variant_list used
- (Datatype_Prop.make_tnames (map Logic.unvarifyT Ts));
+ (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
val ty = body_type Ty;
val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
raise CASE_ERROR ("type mismatch", ~1)
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Mar 22 10:25:44 2010 +0100
@@ -310,7 +310,7 @@
(#case_rewrites o Datatype_Data.the_info thy) tyco;
val thms as hd_thm :: _ = raw_thms
|> Conjunction.intr_balanced
- |> Thm.unvarify
+ |> Thm.unvarify_global
|> Conjunction.elim_balanced (length raw_thms)
|> map Simpdata.mk_meta_eq
|> map Drule.zero_var_indexes
@@ -332,7 +332,7 @@
|> Thm.implies_intr asm
|> Thm.generalize ([], params) 0
|> AxClass.unoverload thy
- |> Thm.varifyT
+ |> Thm.varifyT_global
end;
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Mar 22 10:25:44 2010 +0100
@@ -128,7 +128,7 @@
(Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
- val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []);
+ val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *)
tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
@@ -139,7 +139,7 @@
(fold_rev (fn (f, p) => fn prf =>
(case head_of (strip_abs_body f) of
Free (s, T) =>
- let val T' = Logic.varifyT T
+ let val T' = Logic.varifyT_global T
in Abst (s, SOME T', Proofterm.prf_abstract_over
(Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
end
@@ -149,8 +149,8 @@
val r' =
if null is then r
- else Logic.varify (fold_rev lambda
- (map Logic.unvarify ivs1 @ filter_out is_unit
+ else Logic.varify_global (fold_rev lambda
+ (map Logic.unvarify_global ivs1 @ filter_out is_unit
(map (head_of o strip_abs_body) rec_fns)) r);
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
@@ -179,7 +179,7 @@
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);
- val y = Var (("y", 0), Logic.varifyT T);
+ val y = Var (("y", 0), Logic.varifyT_global T);
val y' = Free ("y", T);
val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
@@ -200,10 +200,10 @@
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf = forall_intr_prf (y, forall_intr_prf (P,
fold_rev (fn (p, r) => fn prf =>
- forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
+ forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
(Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
- val r' = Logic.varify (Abs ("y", T,
+ val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 22 10:25:44 2010 +0100
@@ -566,7 +566,7 @@
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
- |> Logic.varify,
+ |> Logic.varify_global,
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
else case Typedef.get_info_global thy s of
(* FIXME handle multiple typedef interpretations (!??) *)
@@ -599,7 +599,7 @@
handle Type.TYPE_MATCH =>
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
fun varify_and_instantiate_type thy T1 T1' T2 =
- instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2)
+ instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
(* theory -> typ -> typ -> styp *)
fun repair_constr_type thy body_T' T =
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 22 10:25:44 2010 +0100
@@ -326,7 +326,7 @@
(* theory -> typ * typ -> bool *)
fun varified_type_match thy (candid_T, pat_T) =
- strict_type_match thy (candid_T, Logic.varifyT pat_T)
+ strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
(* atom_pool -> (string * string) * (string * string) -> scope -> nut list
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 10:25:44 2010 +0100
@@ -404,7 +404,7 @@
(let
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
- let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
+ let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
in (maxidx_of_term t', t'::ts) end;
val (i, cs') = List.foldr varify (~1, []) cs;
val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 22 10:25:44 2010 +0100
@@ -87,7 +87,7 @@
(* theory -> term -> (string list, term list list) *)
fun dest_code_eqn eqn = let
- val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
+ val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn))
val (func, args) = strip_comb lhs
in ((func, args), rhs) end;
@@ -372,7 +372,7 @@
*)
val thy'' = Fun_Pred.map
- (fold Item_Net.update (map (apfst Logic.varify)
+ (fold Item_Net.update (map (apfst Logic.varify_global)
(distinct (op =) funs ~~ (#preds ind_result)))) thy'
(*val _ = print_specs thy'' specs*)
in
@@ -397,7 +397,7 @@
| lookup_pred _ = NONE
*)
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
- val intro_t = (Logic.unvarify o prop_of) intro
+ val intro_t = Logic.unvarify_global (prop_of intro)
val (prems, concl) = Logic.strip_horn intro_t
val frees = map fst (Term.add_frees intro_t [])
fun rewrite prem names =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Mar 22 10:25:44 2010 +0100
@@ -182,8 +182,8 @@
val new_defs = map new_def assms
val (definition, thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> PureThy.add_axioms (map_index
- (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs)
+ |> fold_map Drule.add_axiom (map_index
+ (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs)
in
(lhs, ((full_constname, definition) :: defs, thy'))
end
@@ -313,7 +313,7 @@
fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
let
val vars = map Var (Term.add_vars abs_arg [])
- val abs_arg' = Logic.unvarify abs_arg
+ val abs_arg' = Logic.unvarify_global abs_arg
val frees = map Free (Term.add_frees abs_arg' [])
val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
((Long_Name.base_name constname) ^ "_hoaux")
@@ -326,7 +326,8 @@
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
|> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
in
- (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
+ (list_comb (Logic.varify_global const, vars),
+ ((full_constname, [definition])::new_defs, thy'))
end
| replace_abs_arg arg (new_defs, thy) =
if (is_predT (fastype_of arg)) then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 10:25:44 2010 +0100
@@ -271,7 +271,7 @@
in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT
+ |> Thm.varifyT_global
end;
--- a/src/HOL/Tools/choice_specification.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML Mon Mar 22 10:25:44 2010 +0100
@@ -44,9 +44,9 @@
let
fun process [] (thy,tm) =
let
- val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
+ val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy
in
- (thy',hd thms)
+ (thy', thm)
end
| process ((thname,cname,covld)::cos) (thy,tm) =
case tm of
@@ -90,9 +90,9 @@
| collect_consts (tm as Const _,tms) = insert (op aconv) tm tms
| collect_consts ( _,tms) = tms
-(* Complementing Type.varify... *)
+(* Complementing Type.varify_global... *)
-fun unvarify t fmap =
+fun unvarify_global t fmap =
let
val fmap' = map Library.swap fmap
fun unthaw (f as (a, S)) =
@@ -135,7 +135,7 @@
val prop = myfoldr HOLogic.mk_conj (map fst props'')
val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
- val (vmap, prop_thawed) = Type.varify [] prop
+ val (vmap, prop_thawed) = Type.varify_global [] prop
val thawed_prop_consts = collect_consts (prop_thawed,[])
val (altcos,overloaded) = Library.split_list cos
val (names,sconsts) = Library.split_list altcos
@@ -145,14 +145,14 @@
fun proc_const c =
let
- val (_, c') = Type.varify [] c
+ val (_, c') = Type.varify_global [] c
val (cname,ctyp) = dest_Const c'
in
case filter (fn t => let val (name,typ) = dest_Const t
in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
end) thawed_prop_consts of
[] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
- | [cf] => unvarify cf vmap
+ | [cf] => unvarify_global cf vmap
| _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
end
val proc_consts = map proc_const consts
--- a/src/HOL/Tools/inductive_realizer.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Mar 22 10:25:44 2010 +0100
@@ -70,9 +70,9 @@
val params = map dest_Var (take nparms ts);
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
- map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
+ map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
filter_out (equal Extraction.nullT) (map
- (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
+ (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)),
NoSyn);
in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
map constr_of_intr intrs)
@@ -339,13 +339,13 @@
let
val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
val s' = Long_Name.base_name s;
- val T' = Logic.unvarifyT T;
+ val T' = Logic.unvarifyT_global T;
in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
|> distinct (op = o pairself (#1 o #1))
|> map (apfst (apfst (apfst Binding.name)))
|> split_list;
- val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
+ val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T))
(List.take (snd (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
@@ -357,7 +357,7 @@
no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
- subst_atomic rlzpreds' (Logic.unvarify rintr)))
+ subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.root_path;
val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
@@ -383,7 +383,7 @@
(used @ rnames) (replicate (length intrs) "s");
val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
let
- val (P, Q) = strip_one name (Logic.unvarify rlz);
+ val (P, Q) = strip_one name (Logic.unvarify_global rlz);
val Q' = strip_all' [] rnames' Q
in
(Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
@@ -446,7 +446,7 @@
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
- val rlz' = strip_all (Logic.unvarify rlz);
+ val rlz' = strip_all (Logic.unvarify_global rlz);
val rews = map mk_meta_eq case_thms;
val thm = Goal.prove_global thy []
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
--- a/src/HOL/Tools/meson.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/meson.ML Mon Mar 22 10:25:44 2010 +0100
@@ -669,7 +669,7 @@
fun make_meta_clause th =
let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
in
- (zero_var_indexes o Thm.varifyT o thaw 0 o
+ (zero_var_indexes o Thm.varifyT_global o thaw 0 o
negated_asm_of_head o make_horn resolution_clause_rules) fth
end;
--- a/src/HOL/Tools/old_primrec.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/old_primrec.ML Mon Mar 22 10:25:44 2010 +0100
@@ -35,7 +35,7 @@
fun unify_consts thy cs intr_ts =
(let
fun varify t (i, ts) =
- let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
+ let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
in (maxidx_of_term t', t'::ts) end;
val (i, cs') = fold_rev varify cs (~1, []);
val (i', intr_ts') = fold_rev varify intr_ts (i, []);
@@ -281,7 +281,7 @@
thy'
|> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
val simps'' = maps snd simps';
- val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
+ val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
in
thy''
|> note (("simps",
--- a/src/HOL/Tools/quickcheck_generators.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Mon Mar 22 10:25:44 2010 +0100
@@ -316,7 +316,7 @@
fun perhaps_constrain thy insts raw_vs =
let
fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
- (Logic.varifyT T, sort);
+ (Logic.varifyT_global T, sort);
val vtab = Vartab.empty
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
|> fold meet_random insts;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Mar 22 10:25:44 2010 +0100
@@ -16,7 +16,7 @@
open Proofterm;
val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
- Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
+ Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
(** eliminate meta-equality rules **)
--- a/src/HOL/Tools/typecopy.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOL/Tools/typecopy.ML Mon Mar 22 10:25:44 2010 +0100
@@ -61,7 +61,7 @@
let
val exists_thm =
UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
+ |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
val inject' = inject OF [exists_thm, exists_thm];
val proj_def = inverse OF [exists_thm];
val info = {
@@ -95,7 +95,7 @@
typ = ty_rep, ... } = get_info thy tyco;
(* FIXME handle multiple typedef interpretations (!??) *)
val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
- val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
+ val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
val ty = Type (tyco, map TFree vs);
val proj = Const (proj, ty --> ty_rep);
val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
@@ -109,7 +109,7 @@
THEN ALLGOALS (rtac @{thm refl});
fun mk_eq_refl thy = @{thm HOL.eq_refl}
|> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
|> AxClass.unoverload thy;
in
thy
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 22 10:25:44 2010 +0100
@@ -54,13 +54,8 @@
val abs_iso_bind = Binding.qualified true "abs_iso" dbind;
val rep_iso_bind = Binding.qualified true "rep_iso" dbind;
- val (abs_iso_thm, thy) =
- yield_singleton PureThy.add_axioms
- ((abs_iso_bind, abs_iso_eqn), []) thy;
-
- val (rep_iso_thm, thy) =
- yield_singleton PureThy.add_axioms
- ((rep_iso_bind, rep_iso_eqn), []) thy;
+ val (abs_iso_thm, thy) = Drule.add_axiom (abs_iso_bind, abs_iso_eqn) thy;
+ val (rep_iso_thm, thy) = Drule.add_axiom (rep_iso_bind, rep_iso_eqn) thy;
val result =
{
@@ -88,9 +83,7 @@
val lub_take_bind = Binding.qualified true "lub_take" dbind;
- val (lub_take_thm, thy) =
- yield_singleton PureThy.add_axioms
- ((lub_take_bind, lub_take_eqn), []) thy;
+ val (lub_take_thm, thy) = Drule.add_axiom (lub_take_bind, lub_take_eqn) thy;
in
(lub_take_thm, thy)
end;
--- a/src/Provers/Arith/abel_cancel.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Mon Mar 22 10:25:44 2010 +0100
@@ -88,7 +88,7 @@
val sum_conv =
Simplifier.mk_simproc "cancel_sums"
- (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc);
+ (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
(*A simproc to cancel like terms on the opposite sides of relations:
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 10:25:44 2010 +0100
@@ -541,7 +541,7 @@
(if count <> warning_count_max then []
else ["\n(Reached maximal message count -- disabling future warnings)"])));
warning "Linear arithmetic should have refuted the assumptions.\n\
- \Please inform Tobias Nipkow (nipkow@in.tum.de).")
+ \Please inform Tobias Nipkow.")
end;
in fls end
handle FalseE thm => trace_thm ctxt "False reached early:" thm
--- a/src/Pure/Isar/class.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/class.ML Mon Mar 22 10:25:44 2010 +0100
@@ -257,7 +257,7 @@
| t => t);
val raw_pred = Locale.intros_of thy class
|> fst
- |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
+ |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
of [] => NONE
| [thm] => SOME thm;
--- a/src/Pure/Isar/class_target.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Mar 22 10:25:44 2010 +0100
@@ -16,12 +16,13 @@
val rules: theory -> class -> thm option * thm
val these_params: theory -> sort -> (string * (class * (string * typ))) list
val these_defs: theory -> sort -> thm list
- val these_operations: theory -> sort -> (string * (class * (typ * term))) list
+ val these_operations: theory -> sort
+ -> (string * (class * (typ * term))) list
val print_classes: theory -> unit
val begin: class list -> sort -> Proof.context -> Proof.context
val init: class -> theory -> Proof.context
- val declare: class -> (binding * mixfix) * term -> theory -> theory
+ val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
val class_prefix: string -> string
val refresh_syntax: class -> Proof.context -> Proof.context
@@ -253,8 +254,8 @@
(* class context syntax *)
-fun these_unchecks thy =
- map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
+fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
+ o these_operations thy;
fun redeclare_const thy c =
let val b = Long_Name.base_name c
@@ -317,25 +318,25 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
-fun declare class ((c, mx), dict) thy =
+fun declare class ((c, mx), (type_params, dict)) thy =
let
val morph = morphism thy class;
val b = Morphism.binding morph c;
val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
val c' = Sign.full_name thy b;
val dict' = Morphism.term morph dict;
- val ty' = Term.fastype_of dict';
- val def_eq = Logic.mk_equals (Const (c', ty'), dict')
+ val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
+ val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
|> map_types Type.strip_sorts;
in
thy
|> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
|> snd
|> Thm.add_def false false (b_def, def_eq)
- |>> Thm.varifyT
+ |>> Thm.varifyT_global
|-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
#> snd
- #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
+ #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
|> Sign.add_const_constraint (c', SOME ty')
end;
@@ -347,7 +348,7 @@
val c' = Sign.full_name thy b;
val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
val ty' = Term.fastype_of rhs';
- val rhs'' = map_types Logic.varifyT rhs';
+ val rhs'' = map_types Logic.varifyT_global rhs';
in
thy
|> Sign.add_abbrev (#1 prmode) (b, rhs'')
@@ -530,7 +531,7 @@
val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
fun after_qed' results =
- Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
+ Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
#> after_qed;
in
lthy
--- a/src/Pure/Isar/code.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/code.ML Mon Mar 22 10:25:44 2010 +0100
@@ -337,7 +337,7 @@
(Binding.qualified_name tyco, n) | _ => I) decls
end;
-fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
+fun cert_signature thy = Logic.varifyT_global 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);
@@ -374,7 +374,7 @@
let
val _ = Thm.cterm_of thy (Const (c, raw_ty));
val ty = subst_signature thy c raw_ty;
- val ty_decl = (Logic.unvarifyT o const_typ thy) c;
+ val ty_decl = (Logic.unvarifyT_global o const_typ thy) c;
fun last_typ c_ty ty =
let
val tfrees = Term.add_tfreesT ty [];
@@ -684,7 +684,7 @@
(fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
in
thm
- |> Thm.varifyT
+ |> Thm.varifyT_global
|> Thm.certify_instantiate (inst, [])
|> pair subst
end;
@@ -697,7 +697,7 @@
val ty_abs = (fastype_of o snd o dest_comb) lhs;
val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs));
val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
- in (c, (Thm.varifyT o zero_var_indexes) raw_concrete_thm) end;
+ in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end;
fun add_rhss_of_eqn thy t =
let
@@ -706,7 +706,8 @@
| add_const _ = I
in fold_aterms add_const t end;
-fun dest_eqn thy = apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify;
+fun dest_eqn thy =
+ apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify_global;
abstype cert = Equations of thm * bool list
| Projection of term * string
@@ -811,14 +812,14 @@
val thms = if null propers then [] else
cert_thm
|> Local_Defs.expand [snd (get_head thy cert_thm)]
- |> Thm.varifyT
+ |> Thm.varifyT_global
|> Conjunction.elim_balanced (length propers);
in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
| equations_of_cert thy (Projection (t, tyco)) =
let
val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
val tyscm = typscheme_projection thy t;
- val t' = map_types Logic.varifyT t;
+ val t' = map_types Logic.varifyT_global t;
in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
| equations_of_cert thy (Abstract (abs_thm, tyco)) =
let
@@ -827,22 +828,24 @@
val _ = fold_aterms (fn Const (c, _) => if c = abs
then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
else I | _ => I) (Thm.prop_of abs_thm);
- in (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT abs_thm), true))]) end;
+ in
+ (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))])
+ end;
fun pretty_cert thy (cert as Equations _) =
(map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
o snd o equations_of_cert thy) cert
| pretty_cert thy (Projection (t, _)) =
- [Syntax.pretty_term_global thy (map_types Logic.varifyT t)]
+ [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
| pretty_cert thy (Abstract (abs_thm, tyco)) =
- [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT) abs_thm];
+ [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
fun bare_thms_of_cert thy (cert as Equations _) =
(map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
o snd o equations_of_cert thy) cert
| bare_thms_of_cert thy (Projection _) = []
| bare_thms_of_cert thy (Abstract (abs_thm, tyco)) =
- [Thm.varifyT (snd (concretify_abs thy tyco abs_thm))];
+ [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))];
end;
@@ -1157,7 +1160,7 @@
(del_eqns abs
#> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
#> change_fun_spec false rep ((K o Proj)
- (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco))
+ (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
#> Abstype_Interpretation.data (tyco, serial ()));
in
thy
--- a/src/Pure/Isar/constdefs.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/constdefs.ML Mon Mar 22 10:25:44 2010 +0100
@@ -56,7 +56,7 @@
|> Sign.add_consts_i [(b, T, mx)]
|> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => (* FIXME thm vs. atts !? *)
- Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
+ Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
Code.add_default_eqn thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/expression.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/expression.ML Mon Mar 22 10:25:44 2010 +0100
@@ -162,7 +162,7 @@
val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
(* type inference and contexts *)
- val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
+ val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
val res = Syntax.check_terms ctxt arg;
@@ -346,7 +346,7 @@
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
- Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
+ Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
val inst'' = map2 TypeInfer.constrain parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
--- a/src/Pure/Isar/isar_cmd.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Mar 22 10:25:44 2010 +0100
@@ -14,7 +14,7 @@
val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
- val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+ val add_axioms: (Attrib.binding * string) list -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
@@ -164,16 +164,14 @@
in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
-(* axioms *)
+(* old-style axioms *)
-fun add_axms f args thy =
- f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
-val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
-
-fun add_defs ((unchecked, overloaded), args) =
- add_axms
- (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
+fun add_defs ((unchecked, overloaded), args) thy =
+ thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
+ (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
+ |> snd;
(* declarations *)
--- a/src/Pure/Isar/isar_syn.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 22 10:25:44 2010 +0100
@@ -178,11 +178,9 @@
(* axioms and definitions *)
-val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
-
val _ =
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
- (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
+ (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
val opt_unchecked_overloaded =
Scan.optional (P.$$$ "(" |-- P.!!!
@@ -191,7 +189,8 @@
val _ =
OuterSyntax.command "defs" "define constants" K.thy_decl
- (opt_unchecked_overloaded -- Scan.repeat1 named_spec
+ (opt_unchecked_overloaded --
+ Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
>> (Toplevel.theory o IsarCmd.add_defs));
--- a/src/Pure/Isar/obtain.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Mar 22 10:25:44 2010 +0100
@@ -197,7 +197,7 @@
val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
- val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
+ val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
val (prems, ctxt'') =
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
@@ -252,7 +252,7 @@
val vars' =
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
(map snd vars @ replicate (length ys) NoSyn);
- val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
+ val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
in ((vars', rule''), ctxt') end;
fun inferred_type (binding, _, mx) ctxt =
--- a/src/Pure/Isar/overloading.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/overloading.ML Mon Mar 22 10:25:44 2010 +0100
@@ -13,7 +13,7 @@
val define: bool -> binding -> string * term -> theory -> thm * theory
val operation: Proof.context -> binding -> (string * bool) option
val pretty: Proof.context -> Pretty.T
-
+
type improvable_syntax
val add_improvable_syntax: Proof.context -> Proof.context
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
--- a/src/Pure/Isar/theory_target.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Mar 22 10:25:44 2010 +0100
@@ -227,7 +227,7 @@
(if is_locale then
Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
#-> (fn (lhs, _) =>
- let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
+ let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
end)
@@ -277,7 +277,7 @@
in
lthy'
|> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
- |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
+ |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
|> Local_Defs.add_def ((b, NoSyn), t)
end;
--- a/src/Pure/Proof/extraction.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Mar 22 10:25:44 2010 +0100
@@ -206,7 +206,7 @@
fun read_condeq thy =
let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify (Syntax.read_prop_global thy' s)
+ let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
in
(map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
@@ -732,7 +732,7 @@
in
thy'
|> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
- Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
+ Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
(Thm.forall_elim_var 0) (forall_intr_frees
(ProofChecker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
--- a/src/Pure/Proof/proof_syntax.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Mon Mar 22 10:25:44 2010 +0100
@@ -217,7 +217,7 @@
fun read_proof thy =
let val rd = read_term thy proofT
- in fn ty => fn s => proof_of_term thy ty (Logic.varify (rd s)) end;
+ in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
fun proof_syntax prf =
let
--- a/src/Pure/Proof/proofchecker.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Proof/proofchecker.ML Mon Mar 22 10:25:44 2010 +0100
@@ -36,7 +36,7 @@
fun thm_of_atom thm Ts =
let
val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
- val (fmap, thm') = Thm.varifyT' [] thm;
+ val (fmap, thm') = Thm.varifyT_global' [] thm;
val ctye = map (pairself (Thm.ctyp_of thy))
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
in
--- a/src/Pure/Tools/find_consts.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/Tools/find_consts.ML Mon Mar 22 10:25:44 2010 +0100
@@ -68,7 +68,7 @@
fun pretty_const ctxt (nm, ty) =
let
- val ty' = Logic.unvarifyT ty;
+ val ty' = Logic.unvarifyT_global ty;
in
Pretty.block
[Pretty.quote (Pretty.str nm), Pretty.fbrk,
--- a/src/Pure/axclass.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/axclass.ML Mon Mar 22 10:25:44 2010 +0100
@@ -309,7 +309,7 @@
|-> (fn const' as Const (c'', _) =>
Thm.add_def false true
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
- #>> Thm.varifyT
+ #>> Thm.varifyT_global
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
#> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
#> snd
@@ -467,7 +467,7 @@
(* definition *)
- val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
+ val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss;
val class_eq =
Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
@@ -521,7 +521,7 @@
val names = name args;
in
thy
- |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+ |> fold_map Drule.add_axiom (map Binding.name names ~~ specs)
|-> fold add
end;
--- a/src/Pure/codegen.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/codegen.ML Mon Mar 22 10:25:44 2010 +0100
@@ -474,7 +474,7 @@
(**** retrieve definition of constant ****)
fun is_instance T1 T2 =
- Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
+ Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
--- a/src/Pure/conjunction.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/conjunction.ML Mon Mar 22 10:25:44 2010 +0100
@@ -75,7 +75,8 @@
val A_B = read_prop "A &&& B";
val conjunction_def =
- Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
+ Thm.unvarify_global
+ (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
--- a/src/Pure/defs.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/defs.ML Mon Mar 22 10:25:44 2010 +0100
@@ -34,7 +34,7 @@
let
val prt_args =
if null args then []
- else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
+ else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
in Pretty.block (Pretty.str c :: prt_args) end;
fun plain_args args =
--- a/src/Pure/display.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/display.ML Mon Mar 22 10:25:44 2010 +0100
@@ -131,9 +131,9 @@
fun prt_sort S = Syntax.pretty_sort ctxt S;
fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
- val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
+ val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
- val prt_term_no_vars = prt_term o Logic.unvarify;
+ val prt_term_no_vars = prt_term o Logic.unvarify_global;
fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
--- a/src/Pure/drule.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/drule.ML Mon Mar 22 10:25:44 2010 +0100
@@ -77,6 +77,7 @@
val flexflex_unique: thm -> thm
val export_without_context: thm -> thm
val export_without_context_open: thm -> thm
+ val add_axiom: (binding * term) -> theory -> thm * theory
val store_thm: binding -> thm -> thm
val store_standard_thm: binding -> thm -> thm
val store_thm_open: binding -> thm -> thm
@@ -312,7 +313,7 @@
Thm.forall_elim_vars (maxidx + 1)
#> Thm.strip_shyps
#> zero_var_indexes
- #> Thm.varifyT);
+ #> Thm.varifyT_global);
val export_without_context =
flexflex_unique
@@ -320,6 +321,12 @@
#> Thm.close_derivation;
+(* old-style axioms *)
+
+fun add_axiom (b, prop) =
+ Thm.add_axiom (b, prop) #-> (fn thm => PureThy.add_thm ((b, export_without_context thm), []));
+
+
(*Convert all Vars in a theorem to Frees. Also return a function for
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.
Similar code in type/freeze_thaw*)
@@ -691,7 +698,7 @@
local
val A = certify (Free ("A", propT));
- val axiom = Thm.unvarify o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+ val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
val prop_def = axiom "Pure.prop_def";
val term_def = axiom "Pure.term_def";
val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -762,7 +769,8 @@
val sort_constraint_eq =
store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
(Thm.equal_intr
- (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
+ (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
+ (Thm.unvarify_global sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
end;
--- a/src/Pure/goal.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/goal.ML Mon Mar 22 10:25:44 2010 +0100
@@ -129,7 +129,8 @@
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
val global_prop =
- cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+ cert (Term.map_types Logic.varifyT_global
+ (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
|> Thm.weaken_sorts (Variable.sorts_of ctxt);
val global_result = result |> Future.map
(Drule.flexflex_unique #>
--- a/src/Pure/logic.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/logic.ML Mon Mar 22 10:25:44 2010 +0100
@@ -38,6 +38,7 @@
val class_of_const: string -> class
val mk_of_class: typ * class -> term
val dest_of_class: term -> typ * class
+ val mk_of_sort: typ * sort -> term list
val name_classrel: string * string -> string
val mk_classrel: class * class -> term
val dest_classrel: term -> class * class
@@ -68,10 +69,10 @@
val list_rename_params: string list * term -> term
val assum_pairs: int * term -> (term*term)list
val assum_problems: int * term -> (term -> term) * term list * term
- val varifyT: typ -> typ
- val unvarifyT: typ -> typ
- val varify: term -> term
- val unvarify: term -> term
+ val varifyT_global: typ -> typ
+ val unvarifyT_global: typ -> typ
+ val varify_global: term -> term
+ val unvarify_global: term -> term
val get_goal: term -> int -> term
val goal_params: term -> int -> term * term list
val prems_of_goal: term -> int -> term list
@@ -217,7 +218,7 @@
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
-(* class membership *)
+(* class/sort membership *)
fun mk_of_class (ty, c) =
Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
@@ -225,6 +226,8 @@
fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
| dest_of_class t = raise TERM ("dest_of_class", [t]);
+fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
+
(* class relations *)
@@ -465,35 +468,35 @@
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
-fun varifyT_same ty = ty
+fun varifyT_global_same ty = ty
|> Term_Subst.map_atypsT_same
(fn TFree (a, S) => TVar ((a, 0), S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
-fun unvarifyT_same ty = ty
+fun unvarifyT_global_same ty = ty
|> Term_Subst.map_atypsT_same
(fn TVar ((a, 0), S) => TFree (a, S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
-val varifyT = Same.commit varifyT_same;
-val unvarifyT = Same.commit unvarifyT_same;
+val varifyT_global = Same.commit varifyT_global_same;
+val unvarifyT_global = Same.commit unvarifyT_global_same;
-fun varify tm = tm
+fun varify_global tm = tm
|> Same.commit (Term_Subst.map_aterms_same
(fn Free (x, T) => Var ((x, 0), T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| _ => raise Same.SAME))
- |> Same.commit (Term_Subst.map_types_same varifyT_same)
+ |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
-fun unvarify tm = tm
+fun unvarify_global tm = tm
|> Same.commit (Term_Subst.map_aterms_same
(fn Var ((x, 0), T) => Free (x, T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
| _ => raise Same.SAME))
- |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
+ |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
--- a/src/Pure/meta_simplifier.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/meta_simplifier.ML Mon Mar 22 10:25:44 2010 +0100
@@ -612,8 +612,8 @@
make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
-(* FIXME avoid global thy and Logic.varify *)
-fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
+(* FIXME avoid global thy and Logic.varify_global *)
+fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
--- a/src/Pure/more_thm.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/more_thm.ML Mon Mar 22 10:25:44 2010 +0100
@@ -59,7 +59,7 @@
(ctyp * ctyp) list * (cterm * cterm) list
val certify_instantiate:
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
- val unvarify: thm -> thm
+ val unvarify_global: thm -> thm
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> thm * theory
val add_def: bool -> bool -> binding * term -> theory -> thm * theory
@@ -295,12 +295,12 @@
Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
-(* unvarify: global schematic variables *)
+(* unvarify_global: global schematic variables *)
-fun unvarify th =
+fun unvarify_global th =
let
val prop = Thm.full_prop_of th;
- val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
+ val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
@@ -322,24 +322,33 @@
(* rules *)
+fun stripped_sorts thy t =
+ let
+ val tfrees = rev (map TFree (Term.add_tfrees t []));
+ val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
+ val strip = tfrees ~~ tfrees';
+ val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
+ val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
+ in (strip, recover, t') end;
+
fun add_axiom (b, prop) thy =
let
- val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b;
- val thy' = thy |> Theory.add_axioms_i [(b', prop)];
- val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
- in (axm, thy') end;
+ val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+ val (strip, recover, prop') = stripped_sorts thy prop;
+ val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
+ val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
+ val thy' =
+ Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
+ val axm' = Thm.axiom thy' (Sign.full_name thy' b');
+ val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
+ in (thm, thy') end;
fun add_def unchecked overloaded (b, prop) thy =
let
- val tfrees = rev (map TFree (Term.add_tfrees prop []));
- val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
- val strip_sorts = tfrees ~~ tfrees';
- val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
-
- val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
+ val (strip, recover, prop') = stripped_sorts thy prop;
val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
val axm' = Thm.axiom thy' (Sign.full_name thy' b);
- val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
+ val thm = unvarify_global (Thm.instantiate (recover, []) axm');
in (thm, thy') end;
--- a/src/Pure/proofterm.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/proofterm.ML Mon Mar 22 10:25:44 2010 +0100
@@ -812,24 +812,24 @@
val f = Free ("f", aT --> bT);
val g = Free ("g", aT --> bT);
-local open Logic in
-
val equality_axms =
- [("reflexive", mk_equals (x, x)),
- ("symmetric", mk_implies (mk_equals (x, y), mk_equals (y, x))),
- ("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
- ("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
- ("equal_elim", list_implies ([mk_equals (A, B), A], B)),
- ("abstract_rule", mk_implies
- (all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))),
- ("combination", list_implies
- ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))];
+ [("reflexive", Logic.mk_equals (x, x)),
+ ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
+ ("transitive",
+ Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
+ ("equal_intr",
+ Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
+ ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
+ ("abstract_rule",
+ Logic.mk_implies
+ (Logic.all x
+ (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+ ("combination", Logic.list_implies
+ ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
equal_elim_axm, abstract_rule_axm, combination_axm] =
- map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms;
-
-end;
+ map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
val reflexive = reflexive_axm % NONE;
--- a/src/Pure/pure_thy.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/pure_thy.ML Mon Mar 22 10:25:44 2010 +0100
@@ -32,8 +32,6 @@
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
-> theory -> (string * thm list) list * theory
- val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
- val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
val add_defs: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
@@ -202,21 +200,16 @@
(* store axioms as theorems *)
local
- fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
- fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
- fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy =>
+ fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
let
- val named_ax = [(b, ax)];
- val thy' = add named_ax thy;
- val thm = hd (get_axs thy' named_ax);
+ val thy' = add [(b, prop)] thy;
+ val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
in
val add_defs = add_axm o Theory.add_defs_i false;
val add_defs_unchecked = add_axm o Theory.add_defs_i true;
- val add_axioms = add_axm Theory.add_axioms_i;
val add_defs_cmd = add_axm o Theory.add_defs false;
val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
- val add_axioms_cmd = add_axm Theory.add_axioms;
end;
@@ -369,6 +362,6 @@
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"
#> add_thmss [((Binding.name "nothing", []), [])] #> snd
- #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms)));
+ #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
end;
--- a/src/Pure/sign.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/sign.ML Mon Mar 22 10:25:44 2010 +0100
@@ -441,7 +441,7 @@
val c = full_name thy b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
- val T' = Logic.varifyT T;
+ val T' = Logic.varifyT_global T;
in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
val args = map prep raw_args;
in
@@ -486,7 +486,7 @@
fun add_const_constraint (c, opt_T) thy =
let
fun prepT raw_T =
- let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
+ let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
in cert_term thy (Const (c, T)); T end
handle TYPE (msg, _, _) => error msg;
in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
--- a/src/Pure/theory.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/theory.ML Mon Mar 22 10:25:44 2010 +0100
@@ -28,8 +28,7 @@
val at_end: (theory -> theory option) -> theory -> theory
val begin_theory: string -> theory list -> theory
val end_theory: theory -> theory
- val add_axioms_i: (binding * term) list -> theory -> theory
- val add_axioms: (binding * string) list -> theory -> theory
+ val add_axiom: binding * term -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
@@ -171,23 +170,14 @@
cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
-(* add_axioms(_i) *)
+(* add_axiom *)
-local
-
-fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
+fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
let
- val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
- val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
+ val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
+ val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
in axioms' end);
-in
-
-val add_axioms_i = gen_add_axioms cert_axm;
-val add_axioms = gen_add_axioms read_axm;
-
-end;
-
(** add constant definitions **)
@@ -200,7 +190,7 @@
val consts = Sign.consts_of thy;
fun prep const =
let val Const (c, T) = Sign.no_vars pp (Const const)
- in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
+ in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
val lhs_vars = Term.add_tfreesT (#2 lhs) [];
val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
@@ -229,7 +219,7 @@
let
val declT = Sign.the_const_constraint thy c
handle TYPE (msg, _, _) => error msg;
- val T' = Logic.varifyT T;
+ val T' = Logic.varifyT_global T;
fun message txt =
[Pretty.block [Pretty.str "Specification of constant ",
@@ -269,7 +259,7 @@
let val axms = map (prep_axm thy) raw_axms in
thy
|> map_defs (fold (check_def thy unchecked overloaded) axms)
- |> add_axioms_i axms
+ |> fold add_axiom axms
end;
in
--- a/src/Pure/thm.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/thm.ML Mon Mar 22 10:25:44 2010 +0100
@@ -137,8 +137,8 @@
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
- val varifyT: thm -> thm
- val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ val varifyT_global: thm -> thm
+ val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
@@ -1231,7 +1231,7 @@
raise THM ("unconstrainT: not a type variable", 0, [th]);
val T' = TVar ((x, i), []);
val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
- val constraints = map (curry Logic.mk_of_class T') S;
+ val constraints = Logic.mk_of_sort (T', S);
in
Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
@@ -1244,11 +1244,11 @@
end;
(* Replace all TFrees not fixed or in the hyps by new TVars *)
-fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
+fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
let
val tfrees = fold Term.add_tfrees hyps fixed;
val prop1 = attach_tpairs tpairs prop;
- val (al, prop2) = Type.varify tfrees prop1;
+ val (al, prop2) = Type.varify_global tfrees prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
(al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der,
@@ -1261,7 +1261,7 @@
prop = prop3}))
end;
-val varifyT = #2 o varifyT' [];
+val varifyT_global = #2 o varifyT_global' [];
(* Replace all TVars by new TFrees *)
fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
--- a/src/Pure/type.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Pure/type.ML Mon Mar 22 10:25:44 2010 +0100
@@ -54,7 +54,7 @@
(*special treatment of type vars*)
val strip_sorts: typ -> typ
val no_tvars: typ -> typ
- val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
+ val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
val legacy_freeze_type: typ -> typ
val legacy_freeze_thaw: term -> term * (term -> term)
@@ -284,9 +284,9 @@
commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
-(* varify *)
+(* varify_global *)
-fun varify fixed t =
+fun varify_global fixed t =
let
val fs = Term.fold_types (Term.fold_atyps
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
--- a/src/Tools/Code/code_thingol.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Mar 22 10:25:44 2010 +0100
@@ -613,7 +613,7 @@
let
val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
- val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
+ val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in
ensure_const thy algbr eqngr c
--- a/src/Tools/IsaPlanner/isand.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Mon Mar 22 10:25:44 2010 +0100
@@ -213,7 +213,7 @@
let
val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
- in #2 (Thm.varifyT' skiptfrees th) end;
+ in #2 (Thm.varifyT_global' skiptfrees th) end;
(* change schematic/meta vars to fresh free vars, avoiding name clashes
with "names" *)
--- a/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 22 10:25:44 2010 +0100
@@ -297,7 +297,7 @@
|> Drule.implies_intr_list cprems
|> Drule.forall_intr_list frees_of_fixed_vars
|> Drule.forall_elim_list vars
- |> Thm.varifyT' othertfrees
+ |> Thm.varifyT_global' othertfrees
|-> K Drule.zero_var_indexes
end;
--- a/src/Tools/nbe.ML Mon Mar 22 10:25:07 2010 +0100
+++ b/src/Tools/nbe.ML Mon Mar 22 10:25:44 2010 +0100
@@ -102,12 +102,12 @@
o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props;
in Drule.implies_elim_list thm prem_thms end;
in ct
- |> Drule.cterm_rule Thm.varifyT
+ |> Drule.cterm_rule Thm.varifyT_global
|> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
(((v, 0), sort), TFree (v, sort'))) vs, []))
|> Drule.cterm_rule Thm.freezeT
|> conv
- |> Thm.varifyT
+ |> Thm.varifyT_global
|> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
|> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
(((v, 0), []), TVar ((v, 0), sort))) vs, [])