--- a/NEWS Fri Jul 10 10:45:30 2009 -0400
+++ b/NEWS Fri Jul 10 10:45:49 2009 -0400
@@ -92,6 +92,10 @@
*** ML ***
+* Renamed functor TableFun to Table, and GraphFun to Graph. (Since
+functors have their own ML name space there is no point to mark them
+separately.) Minor INCOMPATIBILITY.
+
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY.
* Eliminated old Attrib.add_attributes, Method.add_methods and related
--- a/src/FOL/FOL.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/FOL.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/FOL.thy
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
*)
--- a/src/FOL/ROOT.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ROOT.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,7 +1,3 @@
-(* Title: FOL/ROOT.ML
- ID: $Id$
-
-First-Order Logic with Natural Deduction.
-*)
+(* First-Order Logic with Natural Deduction *)
use_thy "FOL";
--- a/src/FOL/cladata.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/cladata.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/cladata.ML
- ID: $Id$
Author: Tobias Nipkow
Copyright 1996 University of Cambridge
--- a/src/FOL/ex/Classical.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Classical.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/Classical
- ID: $Id$
+(* Title: FOL/ex/Classical.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
--- a/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/First_Order_Logic.thy
- ID: $Id$
Author: Markus Wenzel, TU Munich
*)
--- a/src/FOL/ex/Foundation.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Foundation.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/Foundation.ML
- ID: $Id$
+(* Title: FOL/ex/Foundation.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/If.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/If.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/If.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Intro.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Intro.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Intro.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOL/ex/Intuitionistic.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Intuitionistic.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,12 +1,13 @@
-(* Title: FOL/ex/Intuitionistic
- ID: $Id$
+(* Title: FOL/ex/Intuitionistic.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
-header{*Intuitionistic First-Order Logic*}
+header {* Intuitionistic First-Order Logic *}
-theory Intuitionistic imports IFOL begin
+theory Intuitionistic
+imports IFOL
+begin
(*
Single-step ML commands:
@@ -422,4 +423,3 @@
end
-
--- a/src/FOL/ex/Miniscope.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Miniscope.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Miniscope.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
--- a/src/FOL/ex/Nat.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Nat.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Nat.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,11 +1,12 @@
(* Title: FOL/ex/Natural_Numbers.thy
- ID: $Id$
Author: Markus Wenzel, TU Munich
*)
header {* Natural numbers *}
-theory Natural_Numbers imports FOL begin
+theory Natural_Numbers
+imports FOL
+begin
text {*
Theory of the natural numbers: Peano's axioms, primitive recursion.
--- a/src/FOL/ex/Prolog.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Prolog.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/prolog.thy
- ID: $Id$
+(* Title: FOL/ex/Prolog.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Propositional_Cla.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Propositional_Int.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Propositional_Int.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Propositional_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Quantifiers_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Quantifiers_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/fologic.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/fologic.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/fologic.ML
- ID: $Id$
Author: Lawrence C Paulson
Abstract syntax operations for FOL.
--- a/src/FOL/intprover.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/intprover.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
-(* Title: FOL/int-prover
- ID: $Id$
+(* Title: FOL/intprover.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOL/simpdata.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/FOL/simpdata.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: FOL/simpdata.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
--- a/src/HOL/Import/hol4rews.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Import/hol4rews.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,9 +1,8 @@
(* Title: HOL/Import/hol4rews.ML
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
-structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
+structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
type holthm = (term * term) list * thm
--- a/src/HOL/IsaMakefile Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/IsaMakefile Fri Jul 10 10:45:49 2009 -0400
@@ -327,7 +327,7 @@
Library/Finite_Cartesian_Product.thy \
Library/FrechetDeriv.thy Library/Fraction_Field.thy\
Library/Fundamental_Theorem_Algebra.thy \
- Library/Inner_Product.thy Library/Lattice_Syntax.thy \
+ Library/Inner_Product.thy Library/Kleene_Algebra.thy Library/Lattice_Syntax.thy \
Library/Legacy_GCD.thy \
Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy \
Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy \
@@ -710,7 +710,7 @@
HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
-$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL SizeChange/Kleene_Algebras.thy \
+$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL Library/Kleene_Algebra.thy \
SizeChange/Graphs.thy SizeChange/Misc_Tools.thy \
SizeChange/Criterion.thy SizeChange/Correctness.thy \
SizeChange/Interpretation.thy SizeChange/Implementation.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Kleene_Algebra.thy Fri Jul 10 10:45:49 2009 -0400
@@ -0,0 +1,495 @@
+(* Title: HOL/Library/Kleene_Algebra.thy
+ Author: Alexander Krauss, TU Muenchen
+*)
+
+header "Kleene Algebra"
+
+theory Kleene_Algebra
+imports Main
+begin
+
+text {* WARNING: This is work in progress. Expect changes in the future *}
+
+text {* A type class of Kleene algebras *}
+
+class star =
+ fixes star :: "'a \<Rightarrow> 'a"
+
+class idem_add = ab_semigroup_add +
+ assumes add_idem [simp]: "x + x = x"
+begin
+
+lemma add_idem2[simp]: "(x::'a) + (x + y) = x + y"
+unfolding add_assoc[symmetric] by simp
+
+end
+
+class order_by_add = idem_add + ord +
+ assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
+ assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
+begin
+
+lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
+ unfolding order_def .
+
+lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
+ unfolding order_def add_commute .
+
+lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
+ unfolding order_def .
+
+subclass order proof
+ fix x y z :: 'a
+ show "x \<le> x" unfolding order_def by simp
+ show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+ proof (rule ord_intro)
+ assume "x \<le> y" "y \<le> z"
+ have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
+ also have "\<dots> = y + z" by (simp add:`x \<le> y`)
+ also have "\<dots> = z" by (simp add:`y \<le> z`)
+ finally show "x + z = z" .
+ qed
+ show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
+ by (simp add: add_commute)
+ show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
+qed
+
+lemma plus_leI:
+ "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
+ unfolding order_def by (simp add: add_assoc)
+
+lemma less_add[simp]: "a \<le> a + b" "b \<le> a + b"
+unfolding order_def by (auto simp:add_ac)
+
+lemma add_est1: "a + b \<le> c \<Longrightarrow> a \<le> c"
+using less_add(1) by (rule order_trans)
+
+lemma add_est2: "a + b \<le> c \<Longrightarrow> b \<le> c"
+using less_add(2) by (rule order_trans)
+
+end
+
+class pre_kleene = semiring_1 + order_by_add
+begin
+
+subclass pordered_semiring proof
+ fix x y z :: 'a
+
+ assume "x \<le> y"
+
+ show "z + x \<le> z + y"
+ proof (rule ord_intro)
+ have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
+ also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
+ finally show "z + x + (z + y) = z + y" .
+ qed
+
+ show "z * x \<le> z * y"
+ proof (rule ord_intro)
+ from `x \<le> y` have "z * (x + y) = z * y" by simp
+ thus "z * x + z * y = z * y" by (simp add:right_distrib)
+ qed
+
+ show "x * z \<le> y * z"
+ proof (rule ord_intro)
+ from `x \<le> y` have "(x + y) * z = y * z" by simp
+ thus "x * z + y * z = y * z" by (simp add:left_distrib)
+ qed
+qed
+
+lemma zero_minimum [simp]: "0 \<le> x"
+ unfolding order_def by simp
+
+end
+
+class kleene = pre_kleene + star +
+ assumes star1: "1 + a * star a \<le> star a"
+ and star2: "1 + star a * a \<le> star a"
+ and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+ and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
+begin
+
+lemma star3':
+ assumes a: "b + a * x \<le> x"
+ shows "star a * b \<le> x"
+proof (rule order_trans)
+ from a have "b \<le> x" by (rule add_est1)
+ show "star a * b \<le> star a * x"
+ by (rule mult_mono) (auto simp:`b \<le> x`)
+
+ from a have "a * x \<le> x" by (rule add_est2)
+ with star3 show "star a * x \<le> x" .
+qed
+
+lemma star4':
+ assumes a: "b + x * a \<le> x"
+ shows "b * star a \<le> x"
+proof (rule order_trans)
+ from a have "b \<le> x" by (rule add_est1)
+ show "b * star a \<le> x * star a"
+ by (rule mult_mono) (auto simp:`b \<le> x`)
+
+ from a have "x * a \<le> x" by (rule add_est2)
+ with star4 show "x * star a \<le> x" .
+qed
+
+lemma star_unfold_left:
+ shows "1 + a * star a = star a"
+proof (rule antisym, rule star1)
+ have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
+ apply (rule add_mono, rule)
+ apply (rule mult_mono, auto)
+ apply (rule star1)
+ done
+ with star3' have "star a * 1 \<le> 1 + a * star a" .
+ thus "star a \<le> 1 + a * star a" by simp
+qed
+
+lemma star_unfold_right: "1 + star a * a = star a"
+proof (rule antisym, rule star2)
+ have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
+ apply (rule add_mono, rule)
+ apply (rule mult_mono, auto)
+ apply (rule star2)
+ done
+ with star4' have "1 * star a \<le> 1 + star a * a" .
+ thus "star a \<le> 1 + star a * a" by simp
+qed
+
+lemma star_zero[simp]: "star 0 = 1"
+by (fact star_unfold_left[of 0, simplified, symmetric])
+
+lemma star_one[simp]: "star 1 = 1"
+by (metis add_idem2 eq_iff mult_1_right ord_simp2 star3 star_unfold_left)
+
+lemma one_less_star: "1 \<le> star x"
+by (metis less_add(1) star_unfold_left)
+
+lemma ka1: "x * star x \<le> star x"
+by (metis less_add(2) star_unfold_left)
+
+lemma star_mult_idem[simp]: "star x * star x = star x"
+by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
+
+lemma less_star: "x \<le> star x"
+by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
+
+lemma star_simulation:
+ assumes a: "a * x = x * b"
+ shows "star a * x = x * star b"
+proof (rule antisym)
+ show "star a * x \<le> x * star b"
+ proof (rule star3', rule order_trans)
+ from a have "a * x \<le> x * b" by simp
+ hence "a * x * star b \<le> x * b * star b"
+ by (rule mult_mono) auto
+ thus "x + a * (x * star b) \<le> x + x * b * star b"
+ using add_mono by (auto simp: mult_assoc)
+ show "\<dots> \<le> x * star b"
+ proof -
+ have "x * (1 + b * star b) \<le> x * star b"
+ by (rule mult_mono[OF _ star1]) auto
+ thus ?thesis
+ by (simp add:right_distrib mult_assoc)
+ qed
+ qed
+ show "x * star b \<le> star a * x"
+ proof (rule star4', rule order_trans)
+ from a have b: "x * b \<le> a * x" by simp
+ have "star a * x * b \<le> star a * a * x"
+ unfolding mult_assoc
+ by (rule mult_mono[OF _ b]) auto
+ thus "x + star a * x * b \<le> x + star a * a * x"
+ using add_mono by auto
+ show "\<dots> \<le> star a * x"
+ proof -
+ have "(1 + star a * a) * x \<le> star a * x"
+ by (rule mult_mono[OF star2]) auto
+ thus ?thesis
+ by (simp add:left_distrib mult_assoc)
+ qed
+ qed
+qed
+
+lemma star_slide2[simp]: "star x * x = x * star x"
+by (metis star_simulation)
+
+lemma star_idemp[simp]: "star (star x) = star x"
+by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
+
+lemma star_slide[simp]: "star (x * y) * x = x * star (y * x)"
+by (auto simp: mult_assoc star_simulation)
+
+lemma star_one':
+ assumes "p * p' = 1" "p' * p = 1"
+ shows "p' * star a * p = star (p' * a * p)"
+proof -
+ from assms
+ have "p' * star a * p = p' * star (p * p' * a) * p"
+ by simp
+ also have "\<dots> = p' * p * star (p' * a * p)"
+ by (simp add: mult_assoc)
+ also have "\<dots> = star (p' * a * p)"
+ by (simp add: assms)
+ finally show ?thesis .
+qed
+
+lemma x_less_star[simp]: "x \<le> x * star a"
+proof -
+ have "x \<le> x * (1 + a * star a)" by (simp add: right_distrib)
+ also have "\<dots> = x * star a" by (simp only: star_unfold_left)
+ finally show ?thesis .
+qed
+
+lemma star_mono: "x \<le> y \<Longrightarrow> star x \<le> star y"
+by (metis add_commute eq_iff less_star ord_simp2 order_trans star3 star4' star_idemp star_mult_idem x_less_star)
+
+lemma star_sub: "x \<le> 1 \<Longrightarrow> star x = 1"
+by (metis add_commute ord_simp1 star_idemp star_mono star_mult_idem star_one star_unfold_left)
+
+lemma star_unfold2: "star x * y = y + x * star x * y"
+by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
+
+lemma star_absorb_one[simp]: "star (x + 1) = star x"
+by (metis add_commute eq_iff left_distrib less_add(1) less_add(2) mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
+
+lemma star_absorb_one'[simp]: "star (1 + x) = star x"
+by (subst add_commute) (fact star_absorb_one)
+
+lemma ka16: "(y * star x) * star (y * star x) \<le> star x * star (y * star x)"
+by (metis ka1 less_add(1) mult_assoc order_trans star_unfold2)
+
+lemma ka16': "(star x * y) * star (star x * y) \<le> star (star x * y) * star x"
+by (metis ka1 mult_assoc order_trans star_slide x_less_star)
+
+lemma ka17: "(x * star x) * star (y * star x) \<le> star x * star (y * star x)"
+by (metis ka1 mult_assoc mult_right_mono zero_minimum)
+
+lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
+ \<le> star x * star (y * star x)"
+by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
+
+lemma kleene_church_rosser:
+ "star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y"
+oops
+
+lemma star_decomp: "star (a + b) = star a * star (b * star a)"
+oops
+
+lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow> star y * star x \<le> star x * star y"
+by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
+
+lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y"
+by (metis less_star mult_right_mono order_trans zero_minimum)
+
+lemma ka24: "star (x + y) \<le> star (star x * star y)"
+by (metis add_est1 add_est2 less_add(1) mult_assoc order_def plus_leI star_absorb_one star_mono star_slide2 star_unfold2 star_unfold_left x_less_star)
+
+lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
+oops
+
+lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y"
+oops
+
+end
+
+subsection {* Complete lattices are Kleene algebras *}
+
+lemma (in complete_lattice) le_SUPI':
+ assumes "l \<le> M i"
+ shows "l \<le> (SUP i. M i)"
+ using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
+
+class kleene_by_complete_lattice = pre_kleene
+ + complete_lattice + power + star +
+ assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
+begin
+
+subclass kleene
+proof
+ fix a x :: 'a
+
+ have [simp]: "1 \<le> star a"
+ unfolding star_cont[of 1 a 1, simplified]
+ by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
+
+ show "1 + a * star a \<le> star a"
+ apply (rule plus_leI, simp)
+ apply (simp add:star_cont[of a a 1, simplified])
+ apply (simp add:star_cont[of 1 a 1, simplified])
+ apply (subst power_Suc[symmetric])
+ by (intro SUP_leI le_SUPI UNIV_I)
+
+ show "1 + star a * a \<le> star a"
+ apply (rule plus_leI, simp)
+ apply (simp add:star_cont[of 1 a a, simplified])
+ apply (simp add:star_cont[of 1 a 1, simplified])
+ by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
+
+ show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+ proof -
+ assume a: "a * x \<le> x"
+
+ {
+ fix n
+ have "a ^ (Suc n) * x \<le> a ^ n * x"
+ proof (induct n)
+ case 0 thus ?case by (simp add: a)
+ next
+ case (Suc n)
+ hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
+ by (auto intro: mult_mono)
+ thus ?case
+ by (simp add: mult_assoc)
+ qed
+ }
+ note a = this
+
+ {
+ fix n have "a ^ n * x \<le> x"
+ proof (induct n)
+ case 0 show ?case by simp
+ next
+ case (Suc n) with a[of n]
+ show ?case by simp
+ qed
+ }
+ note b = this
+
+ show "star a * x \<le> x"
+ unfolding star_cont[of 1 a x, simplified]
+ by (rule SUP_leI) (rule b)
+ qed
+
+ show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
+ proof -
+ assume a: "x * a \<le> x"
+
+ {
+ fix n
+ have "x * a ^ (Suc n) \<le> x * a ^ n"
+ proof (induct n)
+ case 0 thus ?case by (simp add: a)
+ next
+ case (Suc n)
+ hence "(x * a ^ Suc n) * a \<le> (x * a ^ n) * a"
+ by (auto intro: mult_mono)
+ thus ?case
+ by (simp add: power_commutes mult_assoc)
+ qed
+ }
+ note a = this
+
+ {
+ fix n have "x * a ^ n \<le> x"
+ proof (induct n)
+ case 0 show ?case by simp
+ next
+ case (Suc n) with a[of n]
+ show ?case by simp
+ qed
+ }
+ note b = this
+
+ show "x * star a \<le> x"
+ unfolding star_cont[of x a 1, simplified]
+ by (rule SUP_leI) (rule b)
+ qed
+qed
+
+end
+
+
+subsection {* Transitive Closure *}
+
+context kleene
+begin
+
+definition
+ tcl_def: "tcl x = star x * x"
+
+lemma tcl_zero: "tcl 0 = 0"
+unfolding tcl_def by simp
+
+lemma tcl_unfold_right: "tcl a = a + tcl a * a"
+proof -
+ from star_unfold_right[of a]
+ have "a * (1 + star a * a) = a * star a" by simp
+ from this[simplified right_distrib, simplified]
+ show ?thesis
+ by (simp add:tcl_def mult_assoc)
+qed
+
+lemma less_tcl: "a \<le> tcl a"
+proof -
+ have "a \<le> a + tcl a * a" by simp
+ also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
+ finally show ?thesis .
+qed
+
+end
+
+
+subsection {* Naive Algorithm to generate the transitive closure *}
+
+function (default "\<lambda>x. 0", tailrec, domintros)
+ mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+ "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
+ by pat_completeness simp
+
+declare mk_tcl.simps[simp del] (* loops *)
+
+lemma mk_tcl_code[code]:
+ "mk_tcl A X =
+ (let XA = X * A
+ in if XA \<le> X then X else mk_tcl A (X + XA))"
+ unfolding mk_tcl.simps[of A X] Let_def ..
+
+context kleene
+begin
+
+lemma mk_tcl_lemma1:
+ "(X + X * A) * star A = X * star A"
+proof -
+ have "A * star A \<le> 1 + A * star A" by simp
+ also have "\<dots> = star A" by (simp add:star_unfold_left)
+ finally have "star A + A * star A = star A" by simp
+ hence "X * (star A + A * star A) = X * star A" by simp
+ thus ?thesis by (simp add:left_distrib right_distrib mult_assoc)
+qed
+
+lemma mk_tcl_lemma2:
+ shows "X * A \<le> X \<Longrightarrow> X * star A = X"
+ by (rule antisym) (auto simp:star4)
+
+end
+
+lemma mk_tcl_correctness:
+ fixes X :: "'a::kleene"
+ assumes "mk_tcl_dom (A, X)"
+ shows "mk_tcl A X = X * star A"
+ using assms
+ by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
+
+
+lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
+ by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
+
+lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
+ unfolding mk_tcl_def
+ by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
+
+
+text {* We can replace the dom-Condition of the correctness theorem
+ with something executable *}
+
+lemma mk_tcl_correctness2:
+ fixes A X :: "'a :: {kleene}"
+ assumes "mk_tcl A A \<noteq> 0"
+ shows "mk_tcl A A = tcl A"
+ using assms mk_tcl_default mk_tcl_correctness
+ unfolding tcl_def
+ by auto
+
+end
--- a/src/HOL/Library/Library.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/Library.thy Fri Jul 10 10:45:49 2009 -0400
@@ -34,6 +34,7 @@
Inner_Product
Lattice_Syntax
ListVector
+ Kleene_Algebra
Mapping
Multiset
Nat_Infinity
--- a/src/HOL/Library/Library/ROOT.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/Library/ROOT.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library/document/root.tex Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/Library/document/root.tex Fri Jul 10 10:45:49 2009 -0400
@@ -1,6 +1,3 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{article}
\usepackage{ifthen}
\usepackage[latin1]{inputenc}
--- a/src/HOL/Library/README.html Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/README.html Fri Jul 10 10:45:49 2009 -0400
@@ -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/Library/comm_ring.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/comm_ring.ML Fri Jul 10 10:45:49 2009 -0400
@@ -41,7 +41,7 @@
fun reif_pol T vs (t as Free _) =
let
val one = @{term "1::nat"};
- val i = find_index_eq t vs
+ val i = find_index (fn t' => t' = t) vs
in if i = 0
then pol_PX T $ (pol_Pc T $ cring_one T)
$ one $ (pol_Pc T $ cring_zero T)
--- a/src/HOL/Library/positivstellensatz.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/positivstellensatz.ML Fri Jul 10 10:45:49 2009 -0400
@@ -33,7 +33,7 @@
struct
type key = Key.key;
-structure Tab = TableFun(Key);
+structure Tab = Table(Key);
type 'a T = 'a Tab.table;
val undefined = Tab.empty;
--- a/src/HOL/Library/reflection.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Library/reflection.ML Fri Jul 10 10:45:49 2009 -0400
@@ -103,8 +103,8 @@
NONE => error "index_of : type not found in environements!"
| SOME (tbs,tats) =>
let
- val i = find_index_eq t tats
- val j = find_index_eq t tbs
+ val i = find_index (fn t' => t' = t) tats
+ val j = find_index (fn t' => t' = t) tbs
in (if j = ~1 then
if i = ~1
then (length tbs + length tats,
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -49,7 +48,7 @@
struct
type float = Float.float
-structure Inttab = TableFun(type key = int val ord = rev_order o int_ord);
+structure Inttab = Table(type key = int val ord = rev_order o int_ord);
type vector = string Inttab.table
type matrix = vector Inttab.table
--- a/src/HOL/Matrix/cplex/fspmlp.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,5 +1,4 @@
(* Title: HOL/Matrix/cplex/fspmlp.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -45,9 +44,9 @@
(if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
else GREATER
-structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
+structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
-structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
+structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
--- a/src/HOL/Quickcheck.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Quickcheck.thy Fri Jul 10 10:45:49 2009 -0400
@@ -23,8 +23,8 @@
begin
definition
- "random i = Random.range i o\<rightarrow>
- (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
+ "random i = Random.range 2 o\<rightarrow>
+ (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
instance ..
@@ -97,7 +97,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+instantiation "fun" :: ("{eq, term_of}", random) random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
--- a/src/HOL/SizeChange/Correctness.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/SizeChange/Correctness.thy Fri Jul 10 10:45:49 2009 -0400
@@ -250,7 +250,7 @@
have "tcl A = A * star A"
unfolding tcl_def
- by (simp add: star_commute[of A A A, simplified])
+ by (simp add: star_simulation[of A A A, simplified])
with edge
have "has_edge (A * star A) x G y" by simp
@@ -272,7 +272,7 @@
have "has_edge (star A * A) x G y" by (simp add:tcl_def)
then obtain H H' z
where AH': "has_edge A z H' y" and G: "G = H * H'"
- by (auto simp:in_grcomp)
+ by (auto simp:in_grcomp simp del: star_slide2)
from B
obtain m' e' where "has_edge H' m' e' n"
by (auto simp:G in_grcomp)
--- a/src/HOL/SizeChange/Graphs.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/SizeChange/Graphs.thy Fri Jul 10 10:45:49 2009 -0400
@@ -6,7 +6,7 @@
header {* General Graphs as Sets *}
theory Graphs
-imports Main Misc_Tools Kleene_Algebras
+imports Main Misc_Tools Kleene_Algebra
begin
subsection {* Basic types, Size Change Graphs *}
--- a/src/HOL/SizeChange/Implementation.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/SizeChange/Implementation.thy Fri Jul 10 10:45:49 2009 -0400
@@ -100,7 +100,7 @@
assumes fA: "finite_acg A"
shows "mk_tcl A A = tcl A"
using mk_tcl_finite_terminates[OF fA]
- by (simp only: tcl_def mk_tcl_correctness star_commute)
+ by (simp only: tcl_def mk_tcl_correctness star_simulation)
definition test_SCT :: "nat acg \<Rightarrow> bool"
where
--- a/src/HOL/SizeChange/Kleene_Algebras.thy Fri Jul 10 10:45:30 2009 -0400
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,469 +0,0 @@
-(* Title: HOL/Library/Kleene_Algebras.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header "Kleene Algebras"
-
-theory Kleene_Algebras
-imports Main
-begin
-
-text {* A type class of kleene algebras *}
-
-class star =
- fixes star :: "'a \<Rightarrow> 'a"
-
-class idem_add = ab_semigroup_add +
- assumes add_idem [simp]: "x + x = x"
-
-lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y"
- unfolding add_assoc[symmetric]
- by simp
-
-class order_by_add = idem_add + ord +
- assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
- assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
-begin
-
-lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
- unfolding order_def .
-
-lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
- unfolding order_def add_commute .
-
-lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
- unfolding order_def .
-
-subclass order proof
- fix x y z :: 'a
- show "x \<le> x" unfolding order_def by simp
- show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- proof (rule ord_intro)
- assume "x \<le> y" "y \<le> z"
- have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
- also have "\<dots> = y + z" by (simp add:`x \<le> y`)
- also have "\<dots> = z" by (simp add:`y \<le> z`)
- finally show "x + z = z" .
- qed
- show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
- by (simp add: add_commute)
- show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
-qed
-
-lemma plus_leI:
- "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
- unfolding order_def by (simp add: add_assoc)
-
-end
-
-class pre_kleene = semiring_1 + order_by_add
-begin
-
-subclass pordered_semiring proof
- fix x y z :: 'a
-
- assume "x \<le> y"
-
- show "z + x \<le> z + y"
- proof (rule ord_intro)
- have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
- also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
- finally show "z + x + (z + y) = z + y" .
- qed
-
- show "z * x \<le> z * y"
- proof (rule ord_intro)
- from `x \<le> y` have "z * (x + y) = z * y" by simp
- thus "z * x + z * y = z * y" by (simp add:right_distrib)
- qed
-
- show "x * z \<le> y * z"
- proof (rule ord_intro)
- from `x \<le> y` have "(x + y) * z = y * z" by simp
- thus "x * z + y * z = y * z" by (simp add:left_distrib)
- qed
-qed
-
-lemma zero_minimum [simp]: "0 \<le> x"
- unfolding order_def by simp
-
-end
-
-class kleene = pre_kleene + star +
- assumes star1: "1 + a * star a \<le> star a"
- and star2: "1 + star a * a \<le> star a"
- and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
- and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
-
-class kleene_by_complete_lattice = pre_kleene
- + complete_lattice + power + star +
- assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
-begin
-
-lemma (in complete_lattice) le_SUPI':
- assumes "l \<le> M i"
- shows "l \<le> (SUP i. M i)"
- using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
-
-end
-
-instance kleene_by_complete_lattice < kleene
-proof
-
- fix a x :: 'a
-
- have [simp]: "1 \<le> star a"
- unfolding star_cont[of 1 a 1, simplified]
- by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
-
- show "1 + a * star a \<le> star a"
- apply (rule plus_leI, simp)
- apply (simp add:star_cont[of a a 1, simplified])
- apply (simp add:star_cont[of 1 a 1, simplified])
- apply (subst power_Suc[symmetric])
- by (intro SUP_leI le_SUPI UNIV_I)
-
- show "1 + star a * a \<le> star a"
- apply (rule plus_leI, simp)
- apply (simp add:star_cont[of 1 a a, simplified])
- apply (simp add:star_cont[of 1 a 1, simplified])
- by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
-
- show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
- proof -
- assume a: "a * x \<le> x"
-
- {
- fix n
- have "a ^ (Suc n) * x \<le> a ^ n * x"
- proof (induct n)
- case 0 thus ?case by (simp add: a)
- next
- case (Suc n)
- hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
- by (auto intro: mult_mono)
- thus ?case
- by (simp add: mult_assoc)
- qed
- }
- note a = this
-
- {
- fix n have "a ^ n * x \<le> x"
- proof (induct n)
- case 0 show ?case by simp
- next
- case (Suc n) with a[of n]
- show ?case by simp
- qed
- }
- note b = this
-
- show "star a * x \<le> x"
- unfolding star_cont[of 1 a x, simplified]
- by (rule SUP_leI) (rule b)
- qed
-
- show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
- proof -
- assume a: "x * a \<le> x"
-
- {
- fix n
- have "x * a ^ (Suc n) \<le> x * a ^ n"
- proof (induct n)
- case 0 thus ?case by (simp add: a)
- next
- case (Suc n)
- hence "(x * a ^ Suc n) * a \<le> (x * a ^ n) * a"
- by (auto intro: mult_mono)
- thus ?case
- by (simp add: power_commutes mult_assoc)
- qed
- }
- note a = this
-
- {
- fix n have "x * a ^ n \<le> x"
- proof (induct n)
- case 0 show ?case by simp
- next
- case (Suc n) with a[of n]
- show ?case by simp
- qed
- }
- note b = this
-
- show "x * star a \<le> x"
- unfolding star_cont[of x a 1, simplified]
- by (rule SUP_leI) (rule b)
- qed
-qed
-
-lemma less_add[simp]:
- fixes a b :: "'a :: order_by_add"
- shows "a \<le> a + b"
- and "b \<le> a + b"
- unfolding order_def
- by (auto simp:add_ac)
-
-lemma add_est1:
- fixes a b c :: "'a :: order_by_add"
- assumes a: "a + b \<le> c"
- shows "a \<le> c"
- using less_add(1) a
- by (rule order_trans)
-
-lemma add_est2:
- fixes a b c :: "'a :: order_by_add"
- assumes a: "a + b \<le> c"
- shows "b \<le> c"
- using less_add(2) a
- by (rule order_trans)
-
-
-lemma star3':
- fixes a b x :: "'a :: kleene"
- assumes a: "b + a * x \<le> x"
- shows "star a * b \<le> x"
-proof (rule order_trans)
- from a have "b \<le> x" by (rule add_est1)
- show "star a * b \<le> star a * x"
- by (rule mult_mono) (auto simp:`b \<le> x`)
-
- from a have "a * x \<le> x" by (rule add_est2)
- with star3 show "star a * x \<le> x" .
-qed
-
-
-lemma star4':
- fixes a b x :: "'a :: kleene"
- assumes a: "b + x * a \<le> x"
- shows "b * star a \<le> x"
-proof (rule order_trans)
- from a have "b \<le> x" by (rule add_est1)
- show "b * star a \<le> x * star a"
- by (rule mult_mono) (auto simp:`b \<le> x`)
-
- from a have "x * a \<le> x" by (rule add_est2)
- with star4 show "x * star a \<le> x" .
-qed
-
-
-lemma star_idemp:
- fixes x :: "'a :: kleene"
- shows "star (star x) = star x"
- oops
-
-lemma star_unfold_left:
- fixes a :: "'a :: kleene"
- shows "1 + a * star a = star a"
-proof (rule order_antisym, rule star1)
-
- have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
- apply (rule add_mono, rule)
- apply (rule mult_mono, auto)
- apply (rule star1)
- done
-
- with star3' have "star a * 1 \<le> 1 + a * star a" .
- thus "star a \<le> 1 + a * star a" by simp
-qed
-
-
-lemma star_unfold_right:
- fixes a :: "'a :: kleene"
- shows "1 + star a * a = star a"
-proof (rule order_antisym, rule star2)
-
- have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
- apply (rule add_mono, rule)
- apply (rule mult_mono, auto)
- apply (rule star2)
- done
-
- with star4' have "1 * star a \<le> 1 + star a * a" .
- thus "star a \<le> 1 + star a * a" by simp
-qed
-
-lemma star_zero[simp]:
- shows "star (0::'a::kleene) = 1"
- by (rule star_unfold_left[of 0, simplified])
-
-lemma star_commute:
- fixes a b x :: "'a :: kleene"
- assumes a: "a * x = x * b"
- shows "star a * x = x * star b"
-proof (rule order_antisym)
-
- show "star a * x \<le> x * star b"
- proof (rule star3', rule order_trans)
-
- from a have "a * x \<le> x * b" by simp
- hence "a * x * star b \<le> x * b * star b"
- by (rule mult_mono) auto
- thus "x + a * (x * star b) \<le> x + x * b * star b"
- using add_mono by (auto simp: mult_assoc)
-
- show "\<dots> \<le> x * star b"
- proof -
- have "x * (1 + b * star b) \<le> x * star b"
- by (rule mult_mono[OF _ star1]) auto
- thus ?thesis
- by (simp add:right_distrib mult_assoc)
- qed
- qed
-
- show "x * star b \<le> star a * x"
- proof (rule star4', rule order_trans)
-
- from a have b: "x * b \<le> a * x" by simp
- have "star a * x * b \<le> star a * a * x"
- unfolding mult_assoc
- by (rule mult_mono[OF _ b]) auto
- thus "x + star a * x * b \<le> x + star a * a * x"
- using add_mono by auto
-
- show "\<dots> \<le> star a * x"
- proof -
- have "(1 + star a * a) * x \<le> star a * x"
- by (rule mult_mono[OF star2]) auto
- thus ?thesis
- by (simp add:left_distrib mult_assoc)
- qed
- qed
-qed
-
-lemma star_assoc:
- fixes c d :: "'a :: kleene"
- shows "star (c * d) * c = c * star (d * c)"
- by (auto simp:mult_assoc star_commute)
-
-lemma star_dist:
- fixes a b :: "'a :: kleene"
- shows "star (a + b) = star a * star (b * star a)"
- oops
-
-lemma star_one:
- fixes a p p' :: "'a :: kleene"
- assumes "p * p' = 1" and "p' * p = 1"
- shows "p' * star a * p = star (p' * a * p)"
-proof -
- from assms
- have "p' * star a * p = p' * star (p * p' * a) * p"
- by simp
- also have "\<dots> = p' * p * star (p' * a * p)"
- by (simp add: mult_assoc star_assoc)
- also have "\<dots> = star (p' * a * p)"
- by (simp add: assms)
- finally show ?thesis .
-qed
-
-lemma star_mono:
- fixes x y :: "'a :: kleene"
- assumes "x \<le> y"
- shows "star x \<le> star y"
- oops
-
-
-
-(* Own lemmas *)
-
-
-lemma x_less_star[simp]:
- fixes x :: "'a :: kleene"
- shows "x \<le> x * star a"
-proof -
- have "x \<le> x * (1 + a * star a)" by (simp add:right_distrib)
- also have "\<dots> = x * star a" by (simp only: star_unfold_left)
- finally show ?thesis .
-qed
-
-subsection {* Transitive Closure *}
-
-definition
- "tcl (x::'a::kleene) = star x * x"
-
-lemma tcl_zero:
- "tcl (0::'a::kleene) = 0"
- unfolding tcl_def by simp
-
-lemma tcl_unfold_right: "tcl a = a + tcl a * a"
-proof -
- from star_unfold_right[of a]
- have "a * (1 + star a * a) = a * star a" by simp
- from this[simplified right_distrib, simplified]
- show ?thesis
- by (simp add:tcl_def star_commute mult_ac)
-qed
-
-lemma less_tcl: "a \<le> tcl a"
-proof -
- have "a \<le> a + tcl a * a" by simp
- also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
- finally show ?thesis .
-qed
-
-subsection {* Naive Algorithm to generate the transitive closure *}
-
-function (default "\<lambda>x. 0", tailrec, domintros)
- mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
-where
- "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
- by pat_completeness simp
-
-declare mk_tcl.simps[simp del] (* loops *)
-
-lemma mk_tcl_code[code]:
- "mk_tcl A X =
- (let XA = X * A
- in if XA \<le> X then X else mk_tcl A (X + XA))"
- unfolding mk_tcl.simps[of A X] Let_def ..
-
-lemma mk_tcl_lemma1:
- fixes X :: "'a :: kleene"
- shows "(X + X * A) * star A = X * star A"
-proof -
- have "A * star A \<le> 1 + A * star A" by simp
- also have "\<dots> = star A" by (simp add:star_unfold_left)
- finally have "star A + A * star A = star A" by simp
- hence "X * (star A + A * star A) = X * star A" by simp
- thus ?thesis by (simp add:left_distrib right_distrib mult_ac)
-qed
-
-lemma mk_tcl_lemma2:
- fixes X :: "'a :: kleene"
- shows "X * A \<le> X \<Longrightarrow> X * star A = X"
- by (rule order_antisym) (auto simp:star4)
-
-
-
-
-lemma mk_tcl_correctness:
- fixes A X :: "'a :: {kleene}"
- assumes "mk_tcl_dom (A, X)"
- shows "mk_tcl A X = X * star A"
- using assms
- by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
-
-lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
- by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
-
-lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
- unfolding mk_tcl_def
- by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
-
-
-text {* We can replace the dom-Condition of the correctness theorem
- with something executable *}
-
-lemma mk_tcl_correctness2:
- fixes A X :: "'a :: {kleene}"
- assumes "mk_tcl A A \<noteq> 0"
- shows "mk_tcl A A = tcl A"
- using assms mk_tcl_default mk_tcl_correctness
- unfolding tcl_def
- by (auto simp:star_commute)
-
-end
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 10:45:49 2009 -0400
@@ -111,7 +111,7 @@
else
Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
end
- in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
+ in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
end;
(* make injections for constructors *)
@@ -137,7 +137,7 @@
if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
end
- in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
+ in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
end;
val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
--- a/src/HOL/Tools/Function/decompose.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/Function/decompose.ML Fri Jul 10 10:45:49 2009 -0400
@@ -19,7 +19,7 @@
structure Decompose : DECOMPOSE =
struct
-structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
+structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
--- a/src/HOL/Tools/Function/termination.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/Function/termination.ML Fri Jul 10 10:45:49 2009 -0400
@@ -51,8 +51,8 @@
open FundefLib
val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
-structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
-structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
+structure Term2tab = Table(type key = term * term val ord = term2_ord);
+structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
(** Analyzing binary trees **)
--- a/src/HOL/Tools/inductive.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/inductive.ML Fri Jul 10 10:45:49 2009 -0400
@@ -222,7 +222,7 @@
val k = length params;
val (c, ts) = strip_comb t;
val (xs, ys) = chop k ts;
- val i = find_index_eq c cs;
+ val i = find_index (fn c' => c' = c) cs;
in
if xs = params andalso i >= 0 then
SOME (c, i, ys, chop (length ys)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 10:45:49 2009 -0400
@@ -204,9 +204,9 @@
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
let
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
- val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
- SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
- find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
+ val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
+ SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
+ (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
val fs = maps (fn ((intrs, prems), dummy) =>
let
val fs = map (fn (rule, (ivs, intr)) =>
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Jul 10 10:45:49 2009 -0400
@@ -27,7 +27,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
val size = @{term "i::code_numeral"};
-val size1 = @{term "(i::code_numeral) - 1"};
+val size_pred = @{term "(i::code_numeral) - 1"};
val size' = @{term "j::code_numeral"};
val seed = @{term "s::Random.seed"};
@@ -243,7 +243,7 @@
| mk_random_fun_lift (fT :: fTs) t =
mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
mk_random_fun_lift fTs t;
- val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size');
+ val t = mk_random_fun_lift fTs (nth random_auxs k $ size_pred $ size');
val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
|> the_default 0;
in (SOME size, (t, fTs ---> T)) end;
--- a/src/HOL/Tools/refute.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/refute.ML Fri Jul 10 10:45:49 2009 -0400
@@ -2401,7 +2401,7 @@
(* by our assumption on the order of recursion operators *)
(* and datatypes, this is the index of the datatype *)
(* corresponding to the given recursion operator *)
- val idt_index = find_index_eq s (#rec_names info)
+ val idt_index = find_index (fn s' => s' = s) (#rec_names info)
(* mutually recursive types must have the same type *)
(* parameters, unless the mutual recursion comes from *)
(* indirect recursion *)
@@ -2535,7 +2535,7 @@
(* returned *)
(* interpretation -> int -> int list option *)
fun get_args (Leaf xs) elem =
- if find_index_eq True xs = elem then
+ if find_index (fn x => x = True) xs = elem then
SOME []
else
NONE
@@ -2606,7 +2606,7 @@
(* corresponding recursive argument *)
fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
(* recursive argument is "rec_i params elem" *)
- compute_array_entry i (find_index_eq True xs)
+ compute_array_entry i (find_index (fn x => x = True) xs)
| rec_intr (DatatypeAux.DtRec _) (Node _) =
raise REFUTE ("IDT_recursion_interpreter",
"interpretation for IDT is a node")
@@ -3237,7 +3237,7 @@
def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
(* interpretation -> int list option *)
fun get_args (Leaf xs) =
- if find_index_eq True xs = element then
+ if find_index (fn x => x = True) xs = element then
SOME []
else
NONE
--- a/src/HOL/Tools/res_atp.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/Tools/res_atp.ML Fri Jul 10 10:45:49 2009 -0400
@@ -152,7 +152,7 @@
end;
-structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
+structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
fun count_axiom_consts theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
--- a/src/HOL/ex/Formal_Power_Series_Examples.thy Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy Fri Jul 10 10:45:49 2009 -0400
@@ -184,9 +184,10 @@
qed
lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
- unfolding minus_mult_right Eii_sin_cos by simp
+ unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
-lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d) "by (simp add: fps_eq_iff fps_const_def)
+lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
+ by (simp add: fps_eq_iff fps_const_def)
lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
apply (subst (2) number_of_eq)
@@ -201,7 +202,8 @@
by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
show ?thesis
unfolding Eii_sin_cos minus_mult_commute
- by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
+ by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
+ fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
qed
lemma fps_sin_Eii:
@@ -211,7 +213,7 @@
by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
show ?thesis
unfolding Eii_sin_cos minus_mult_commute
- by (simp add: fps_divide_def fps_const_inverse th)
+ by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
qed
lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"
--- a/src/HOL/ex/predicate_compile.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOL/ex/predicate_compile.ML Fri Jul 10 10:45:49 2009 -0400
@@ -419,8 +419,8 @@
error ("Too few arguments for inductive predicate " ^ name)
else chop (length iss) args;
val k = length args2;
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
- (1 upto b)
+ val perm = map (fn i => (find_index (fn t => t = Bound (b - i)) args2) + 1)
+ (1 upto b)
val partial_mode = (1 upto k) \\ perm
in
if not (partial_mode subset is) then [] else
@@ -627,7 +627,7 @@
val (params, args') = chop (length ms) args
val (inargs, outargs) = get_args is' args'
val b = length vs
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
+ val perm = map (fn i => find_index (fn t => t = Bound (b - i)) args' + 1) (1 upto b)
val outp_perm =
snd (get_args is perm)
|> map (fn i => i - length (filter (fn x => x < i) is'))
--- a/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 10:45:49 2009 -0400
@@ -121,7 +121,7 @@
val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end
--- a/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 10:45:49 2009 -0400
@@ -365,7 +365,7 @@
fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
val mk_ctuple_pat = foldr1 cpair_pat;
fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
+fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
(case cont_eta_contract body of
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 10:45:49 2009 -0400
@@ -391,7 +391,7 @@
|> hd
val (eq as Lineq(_,_,ceq,_),othereqs) =
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
- val v = find_index_eq c ceq
+ val v = find_index (fn v => v = c) ceq
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
(othereqs @ noneqs)
val others = map (elim_var v eq) roth @ ioth
--- a/src/Pure/Concurrent/task_queue.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Concurrent/task_queue.ML Fri Jul 10 10:45:49 2009 -0400
@@ -41,7 +41,7 @@
fun str_of_task (Task (_, i)) = string_of_int i;
fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
-structure Task_Graph = GraphFun(type key = task val ord = task_ord);
+structure Task_Graph = Graph(type key = task val ord = task_ord);
(* groups *)
--- a/src/Pure/General/graph.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/General/graph.ML Fri Jul 10 10:45:49 2009 -0400
@@ -52,7 +52,7 @@
val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
end;
-functor GraphFun(Key: KEY): GRAPH =
+functor Graph(Key: KEY): GRAPH =
struct
(* keys *)
@@ -67,7 +67,7 @@
(* tables and sets of keys *)
-structure Table = TableFun(Key);
+structure Table = Table(Key);
type keys = unit Table.table;
val empty_keys = Table.empty: keys;
@@ -299,5 +299,5 @@
end;
-structure Graph = GraphFun(type key = string val ord = fast_string_ord);
-structure IntGraph = GraphFun(type key = int val ord = int_ord);
+structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure IntGraph = Graph(type key = int val ord = int_ord);
--- a/src/Pure/General/table.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/General/table.ML Fri Jul 10 10:45:49 2009 -0400
@@ -58,7 +58,7 @@
'a list table * 'a list table -> 'a list table (*exception DUP*)
end;
-functor TableFun(Key: KEY): TABLE =
+functor Table(Key: KEY): TABLE =
struct
@@ -409,8 +409,8 @@
end;
-structure Inttab = TableFun(type key = int val ord = int_ord);
-structure Symtab = TableFun(type key = string val ord = fast_string_ord);
-structure Symreltab = TableFun(type key = string * string
+structure Inttab = Table(type key = int val ord = int_ord);
+structure Symtab = Table(type key = string val ord = fast_string_ord);
+structure Symreltab = Table(type key = string * string
val ord = prod_ord fast_string_ord fast_string_ord);
--- a/src/Pure/Isar/class.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/class.ML Fri Jul 10 10:45:49 2009 -0400
@@ -311,7 +311,7 @@
val proto_sub = case TheoryTarget.peek lthy
of {is_class = false, ...} => error "Not in a class context"
| {target, ...} => target;
- val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
+ val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
val expr = ([(sup, (("", false), Expression.Positional []))], []);
val (([props], deps, export), goal_ctxt) =
--- a/src/Pure/Isar/class_target.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/class_target.ML Fri Jul 10 10:45:49 2009 -0400
@@ -242,16 +242,15 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
+ val deps_witss = case some_dep_morph
+ of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
+ | NONE => []
in
thy
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> fold (fn dep_morph => Locale.add_dependency sub (sup,
- dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
- (the_list some_dep_morph)
- |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
- (Locale.get_registrations thy) thy)
+ |> Locale.add_dependencies sub deps_witss export
end;
--- a/src/Pure/Isar/code.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/code.ML Fri Jul 10 10:45:49 2009 -0400
@@ -355,7 +355,7 @@
(* data slots dependent on executable code *)
(*private copy avoids potential conflict of table exceptions*)
-structure Datatab = TableFun(type key = int val ord = int_ord);
+structure Datatab = Table(type key = int val ord = int_ord);
local
--- a/src/Pure/Isar/expression.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/expression.ML Fri Jul 10 10:45:49 2009 -0400
@@ -492,7 +492,7 @@
val export = Variable.export_morphism goal_ctxt context;
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
- val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
+ val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
val exp_typ = Logic.type_map exp_term;
val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in ((propss, deps, export'), goal_ctxt) end;
@@ -796,14 +796,9 @@
let
val target = intern thy raw_target;
val target_ctxt = Locale.init target thy;
-
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-
fun after_qed witss = ProofContext.theory
- (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
- (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
- (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
- (Locale.get_registrations thy) thy));
+ (Locale.add_dependencies target (deps ~~ witss) export);
in Element.witness_proof after_qed propss goal_ctxt end;
in
@@ -860,7 +855,7 @@
end;
fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
- #-> (fn regs => store_eqns_activate regs eqs));
+ #-> (fn regs => store_eqns_activate regs eqs));
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
--- a/src/Pure/Isar/locale.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/locale.ML Fri Jul 10 10:45:49 2009 -0400
@@ -45,7 +45,6 @@
val instance_of: theory -> string -> morphism -> term list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
- val dependencies_of: theory -> string -> (string * morphism) list
(* Storing results *)
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -53,7 +52,6 @@
val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
val add_declaration: string -> declaration -> Proof.context -> Proof.context
- val add_dependency: string -> string * morphism -> theory -> theory
(* Activation *)
val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -69,10 +67,11 @@
val unfold_add: attribute
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
- (* Registrations *)
+ (* Registrations and dependencies *)
val add_registration: string * (morphism * morphism) -> theory -> theory
val amend_registration: morphism -> string * morphism -> theory -> theory
- val get_registrations: theory -> (string * morphism) list
+ val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
+ morphism -> theory -> theory
(* Diagnostic *)
val print_locales: theory -> unit
@@ -338,13 +337,19 @@
(* FIXME consolidate with dependencies, consider one data slot only *)
);
-val get_registrations =
- Registrations.get #> map (#1 #> apsnd op $>);
+fun reg_morph ((name, (base, export)), _) = (name, base $> export);
+
+fun these_registrations thy name = Registrations.get thy
+ |> filter (curry (op =) name o fst o fst)
+ |> map reg_morph;
+
+fun all_registrations thy = Registrations.get thy
+ |> map reg_morph;
fun add_registration (name, (base_morph, export)) thy =
roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
- (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
- (* FIXME |-> put_global_idents ?*)
+ (name, base_morph) (get_idents (Context.Theory thy), thy)
+ (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
fun amend_registration morph (name, base_morph) thy =
let
@@ -364,6 +369,17 @@
end;
+(*** Dependencies ***)
+
+fun add_dependencies loc deps_witss export thy =
+ thy
+ |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
+ (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
+ deps_witss
+ |> (fn thy => fold_rev (Context.theory_map o activate_facts)
+ (all_registrations thy) thy);
+
+
(*** Storing results ***)
(* Theorems *)
@@ -375,12 +391,12 @@
(change_locale loc o apfst o apsnd) (cons (args', stamp ()))
#>
(* Registrations *)
- (fn thy => fold_rev (fn (name, morph) =>
+ (fn thy => fold_rev (fn (_, morph) =>
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
in PureThy.note_thmss kind args'' #> snd end)
- (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+ (these_registrations thy loc) thy))
in ctxt'' end;
@@ -404,11 +420,6 @@
end;
-(* Dependencies *)
-
-fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
-
-
(*** Reasoning about locales ***)
(* Storage for witnesses, intro and unfold rules *)
--- a/src/Pure/Isar/rule_insts.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/rule_insts.ML Fri Jul 10 10:45:49 2009 -0400
@@ -58,7 +58,7 @@
end;
fun instantiate inst =
- TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+ Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
Envir.beta_norm;
fun make_instT f v =
@@ -124,7 +124,7 @@
end;
val type_insts1 = map readT type_insts;
- val instT1 = TermSubst.instantiateT type_insts1;
+ val instT1 = Term_Subst.instantiateT type_insts1;
val vars1 = map (apsnd instT1) vars;
--- a/src/Pure/Isar/theory_target.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/Isar/theory_target.ML Fri Jul 10 10:45:49 2009 -0400
@@ -130,7 +130,7 @@
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
val inst = filter (is_Var o fst) (vars ~~ frees);
val cinstT = map (pairself certT o apfst TVar) instT;
- val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
+ val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
--- a/src/Pure/consts.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/consts.ML Fri Jul 10 10:45:49 2009 -0400
@@ -215,7 +215,7 @@
val vars = map Term.dest_TVar (typargs consts (c, declT));
val inst = vars ~~ Ts handle UnequalLengths =>
raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
- in declT |> TermSubst.instantiateT inst end;
+ in declT |> Term_Subst.instantiateT inst end;
--- a/src/Pure/context.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/context.ML Fri Jul 10 10:45:49 2009 -0400
@@ -97,7 +97,7 @@
(* data kinds and access methods *)
(*private copy avoids potential conflict of table exceptions*)
-structure Datatab = TableFun(type key = int val ord = int_ord);
+structure Datatab = Table(type key = int val ord = int_ord);
local
--- a/src/Pure/drule.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/drule.ML Fri Jul 10 10:45:49 2009 -0400
@@ -278,7 +278,7 @@
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
- val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+ val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
--- a/src/Pure/library.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/library.ML Fri Jul 10 10:45:49 2009 -0400
@@ -97,7 +97,6 @@
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val split_last: 'a list -> 'a list * 'a
val find_index: ('a -> bool) -> 'a list -> int
- val find_index_eq: ''a -> ''a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
val get_first: ('a -> 'b option) -> 'a list -> 'b option
@@ -503,8 +502,6 @@
| find n (x :: xs) = if pred x then n else find (n + 1) xs;
in find 0 end;
-fun find_index_eq x = find_index (equal x);
-
(*find first element satisfying predicate*)
val find_first = List.find;
--- a/src/Pure/logic.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/logic.ML Fri Jul 10 10:45:49 2009 -0400
@@ -476,30 +476,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 ty = ty |> Term.map_atyps
- (fn TFree (a, S) => TVar ((a, 0), S)
- | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
+fun varifyT_option ty = ty
+ |> Term_Subst.map_atypsT_option
+ (fn TFree (a, S) => SOME (TVar ((a, 0), S))
+ | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
-fun unvarifyT ty = ty |> Term.map_atyps
- (fn TVar ((a, 0), S) => TFree (a, S)
- | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
- | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
+fun unvarifyT_option ty = ty
+ |> Term_Subst.map_atypsT_option
+ (fn TVar ((a, 0), S) => SOME (TFree (a, S))
+ | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
+ | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
-fun varify tm =
- tm |> Term.map_aterms
- (fn Free (x, T) => Var ((x, 0), T)
+val varifyT = perhaps varifyT_option;
+val unvarifyT = perhaps unvarifyT_option;
+
+fun varify tm = tm
+ |> perhaps (Term_Subst.map_aterms_option
+ (fn Free (x, T) => SOME (Var ((x, 0), T))
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
- | t => t)
- |> Term.map_types varifyT
+ | _ => NONE))
+ |> perhaps (Term_Subst.map_types_option varifyT_option)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
-fun unvarify tm =
- tm |> Term.map_aterms
- (fn Var ((x, 0), T) => Free (x, T)
+fun unvarify tm = tm
+ |> perhaps (Term_Subst.map_aterms_option
+ (fn Var ((x, 0), T) => SOME (Free (x, T))
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
- | t => t)
- |> Term.map_types unvarifyT
+ | _ => NONE))
+ |> perhaps (Term_Subst.map_types_option unvarifyT_option)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
--- a/src/Pure/more_thm.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/more_thm.ML Fri Jul 10 10:45:49 2009 -0400
@@ -274,7 +274,7 @@
val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
- let val T' = TermSubst.instantiateT instT0 T
+ let val T' = Term_Subst.instantiateT instT0 T
in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
in Thm.instantiate (instT, inst) th end;
@@ -414,4 +414,4 @@
val op aconvc = Thm.aconvc;
-structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);
+structure Thmtab = Table(type key = thm val ord = Thm.thm_ord);
--- a/src/Pure/proofterm.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/proofterm.ML Fri Jul 10 10:45:49 2009 -0400
@@ -441,12 +441,12 @@
(**** substitutions ****)
-fun del_conflicting_tvars envT T = TermSubst.instantiateT
+fun del_conflicting_tvars envT T = Term_Subst.instantiateT
(map_filter (fn ixnS as (_, S) =>
(Type.lookup envT ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
-fun del_conflicting_vars env t = TermSubst.instantiate
+fun del_conflicting_vars env t = Term_Subst.instantiate
(map_filter (fn ixnS as (_, S) =>
(Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
@@ -689,16 +689,16 @@
fun generalize (tfrees, frees) idx =
map_proof_terms_option
- (TermSubst.generalize_option (tfrees, frees) idx)
- (TermSubst.generalizeT_option tfrees idx);
+ (Term_Subst.generalize_option (tfrees, frees) idx)
+ (Term_Subst.generalizeT_option tfrees idx);
(***** instantiation *****)
fun instantiate (instT, inst) =
map_proof_terms_option
- (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
- (TermSubst.instantiateT_option instT);
+ (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
+ (Term_Subst.instantiateT_option instT);
(***** lifting *****)
--- a/src/Pure/term_ord.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/term_ord.ML Fri Jul 10 10:45:49 2009 -0400
@@ -204,6 +204,7 @@
end;
-structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
-structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
-structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
+structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord);
+structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
+structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
--- a/src/Pure/term_subst.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/term_subst.ML Fri Jul 10 10:45:49 2009 -0400
@@ -1,11 +1,15 @@
(* Title: Pure/term_subst.ML
Author: Makarius
-Efficient term substitution -- avoids copying.
+Efficient type/term substitution -- avoids copying.
*)
signature TERM_SUBST =
sig
+ val map_atypsT_option: (typ -> typ option) -> typ -> typ option
+ val map_atyps_option: (typ -> typ option) -> term -> term option
+ val map_types_option: (typ -> typ option) -> term -> term option
+ val map_aterms_option: (term -> term option) -> term -> term option
val generalize: string list * string list -> int -> term -> term
val generalizeT: string list -> int -> typ -> typ
val generalize_option: string list * string list -> int -> term -> term option
@@ -25,15 +29,67 @@
((indexname * sort) * typ) list * ((indexname * typ) * term) list
end;
-structure TermSubst: TERM_SUBST =
+structure Term_Subst: TERM_SUBST =
struct
+(* indication of same result *)
+
+exception SAME;
+
+fun same_fn f x =
+ (case f x of
+ NONE => raise SAME
+ | SOME y => y);
+
+fun option_fn f x =
+ SOME (f x) handle SAME => NONE;
+
+
+(* generic mapping *)
+
+local
+
+fun map_atypsT_same f =
+ let
+ fun typ (Type (a, Ts)) = Type (a, typs Ts)
+ | typ T = f T
+ and typs (T :: Ts) = (typ T :: (typs Ts handle SAME => Ts) handle SAME => T :: typs Ts)
+ | typs [] = raise SAME;
+ in typ end;
+
+fun map_types_same f =
+ let
+ fun term (Const (a, T)) = Const (a, f T)
+ | term (Free (a, T)) = Free (a, f T)
+ | term (Var (v, T)) = Var (v, f T)
+ | term (Bound _) = raise SAME
+ | term (Abs (x, T, t)) =
+ (Abs (x, f T, term t handle SAME => t)
+ handle SAME => Abs (x, T, term t))
+ | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u);
+ in term end;
+
+fun map_aterms_same f =
+ let
+ fun term (Abs (x, T, t)) = Abs (x, T, term t)
+ | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u)
+ | term a = f a;
+ in term end;
+
+in
+
+val map_atypsT_option = option_fn o map_atypsT_same o same_fn;
+val map_atyps_option = option_fn o map_types_same o map_atypsT_same o same_fn;
+val map_types_option = option_fn o map_types_same o same_fn;
+val map_aterms_option = option_fn o map_aterms_same o same_fn;
+
+end;
+
+
(* generalization of fixed variables *)
local
-exception SAME;
-
fun generalizeT_same [] _ _ = raise SAME
| generalizeT_same tfrees idx ty =
let
@@ -84,8 +140,6 @@
fun no_indexes1 inst = map no_index inst;
fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
-exception SAME;
-
fun instantiateT_same maxidx instT ty =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
--- a/src/Pure/thm.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/thm.ML Fri Jul 10 10:45:49 2009 -0400
@@ -995,7 +995,7 @@
val _ = exists bad_term hyps andalso
raise THM ("generalize: variable free in assumptions", 0, [th]);
- val gen = TermSubst.generalize (tfrees, frees) idx;
+ val gen = Term_Subst.generalize (tfrees, frees) idx;
val prop' = gen prop;
val tpairs' = map (pairself gen) tpairs;
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
@@ -1066,7 +1066,7 @@
val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
val (inst', (instT', (thy_ref', shyps'))) =
(thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
- val subst = TermSubst.instantiate_maxidx (instT', inst');
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
val (prop', maxidx1) = subst prop ~1;
val (tpairs', maxidx') =
fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
@@ -1088,8 +1088,8 @@
val Cterm {thy_ref, t, T, sorts, ...} = ct;
val (inst', (instT', (thy_ref', sorts'))) =
(thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
- val subst = TermSubst.instantiate_maxidx (instT', inst');
- val substT = TermSubst.instantiateT_maxidx instT';
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val substT = Term_Subst.instantiateT_maxidx instT';
val (t', maxidx1) = subst t ~1;
val (T', maxidx') = substT T maxidx1;
in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
--- a/src/Pure/type_infer.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/type_infer.ML Fri Jul 10 10:45:49 2009 -0400
@@ -64,7 +64,7 @@
else (inst, used);
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
- in (map o map_types) (TermSubst.instantiateT inst) ts end;
+ in (map o map_types) (Term_Subst.instantiateT inst) ts end;
--- a/src/Pure/variable.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Pure/variable.ML Fri Jul 10 10:45:49 2009 -0400
@@ -360,14 +360,14 @@
fun exportT_terms inner outer =
let val mk_tfrees = exportT_inst inner outer in
fn ts => ts |> map
- (TermSubst.generalize (mk_tfrees ts, [])
+ (Term_Subst.generalize (mk_tfrees ts, [])
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
end;
fun export_terms inner outer =
let val (mk_tfrees, tfrees) = export_inst inner outer in
fn ts => ts |> map
- (TermSubst.generalize (mk_tfrees ts, tfrees)
+ (Term_Subst.generalize (mk_tfrees ts, tfrees)
(fold Term.maxidx_term ts ~1 + 1))
end;
@@ -376,8 +376,8 @@
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
val tfrees = mk_tfrees [];
val idx = Proofterm.maxidx_proof prf ~1 + 1;
- val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
- val gen_typ = TermSubst.generalizeT_option tfrees idx;
+ val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
+ val gen_typ = Term_Subst.generalizeT_option tfrees idx;
in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
@@ -411,18 +411,18 @@
let
val ren = Name.clean #> (if is_open then I else Name.internal);
val (instT, ctxt') = importT_inst ts ctxt;
- val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
+ val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
val inst = vars ~~ map Free (xs ~~ map #2 vars);
in ((instT, inst), ctxt'') end;
fun importT_terms ts ctxt =
let val (instT, ctxt') = importT_inst ts ctxt
- in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
+ in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
fun import_terms is_open ts ctxt =
let val (inst, ctxt') = import_inst is_open ts ctxt
- in (map (TermSubst.instantiate inst) ts, ctxt') end;
+ in (map (Term_Subst.instantiate inst) ts, ctxt') end;
fun importT ths ctxt =
let
@@ -527,9 +527,9 @@
val idx = maxidx_of ctxt' + 1;
val Ts' = (fold o fold_types o fold_atyps)
(fn T as TFree _ =>
- (case TermSubst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
+ (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
| _ => I) ts [];
- val ts' = map (TermSubst.generalize (types, []) idx) ts;
+ val ts' = map (Term_Subst.generalize (types, []) idx) ts;
in (rev Ts', ts') end;
fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
--- a/src/Tools/Code/code_preproc.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Tools/Code/code_preproc.ML Fri Jul 10 10:45:49 2009 -0400
@@ -224,7 +224,7 @@
fun default_typscheme_of thy c =
let
- val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
+ val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
o Type.strip_sorts o Sign.the_const_type thy) c;
in case AxClass.class_of_param thy c
of SOME class => ([(Name.aT, [class])], ty)
@@ -253,7 +253,7 @@
type var = const * int;
structure Vargraph =
- GraphFun(type key = var val ord = prod_ord const_ord int_ord);
+ Graph(type key = var val ord = prod_ord const_ord int_ord);
datatype styp = Tyco of string * styp list | Var of var | Free;
--- a/src/Tools/Compute_Oracle/am_interpreter.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Fri Jul 10 10:45:49 2009 -0400
@@ -16,7 +16,7 @@
| CApp of closure * closure | CAbs of closure
| Closure of (closure list) * closure
-structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
+structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord);
datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table
--- a/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 10:45:49 2009 -0400
@@ -167,8 +167,6 @@
| machine_of_prog (ProgHaskell _) = HASKELL
| machine_of_prog (ProgSML _) = SML
-structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
-
type naming = int -> string
fun default_naming i = "v_" ^ Int.toString i
--- a/src/Tools/Compute_Oracle/linker.ML Fri Jul 10 10:45:30 2009 -0400
+++ b/src/Tools/Compute_Oracle/linker.ML Fri Jul 10 10:45:49 2009 -0400
@@ -54,8 +54,8 @@
fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
-structure Consttab = TableFun(type key = constant val ord = constant_ord);
-structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord);
+structure Consttab = Table(type key = constant val ord = constant_ord);
+structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
fun typ_of_constant (Constant (_, _, ty)) = ty
@@ -72,7 +72,7 @@
fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
(list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
-structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
+structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
fun substtab_union c = Substtab.fold Substtab.update c
fun substtab_unions [] = Substtab.empty
@@ -382,7 +382,7 @@
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
-structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
+structure CThmtab = Table(type key = cthm val ord = cthm_ord)
fun remove_duplicates ths =
let