# HG changeset patch # User haftmann # Date 1247205584 -7200 # Node ID a290c36e94d638a524f8b5b6194797723200a9dc # Parent 7b7dfbf38034105ad7cfe7dbde6af3aa9fae1ca4# Parent 801aabf9f376710511051d36217ce7cde7c20af0 merged diff -r 801aabf9f376 -r a290c36e94d6 NEWS --- a/NEWS Fri Jul 10 07:59:29 2009 +0200 +++ b/NEWS Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/FOL.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/FOL.thy - ID: $Id$ Author: Lawrence C Paulson and Markus Wenzel *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ROOT.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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"; diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/cladata.ML --- a/src/FOL/cladata.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/cladata.ML Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/cladata.ML - ID: $Id$ Author: Tobias Nipkow Copyright 1996 University of Cambridge diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Classical.thy --- a/src/FOL/ex/Classical.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Classical.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/First_Order_Logic.thy --- a/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/First_Order_Logic.thy - ID: $Id$ Author: Markus Wenzel, TU Munich *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Foundation.thy --- a/src/FOL/ex/Foundation.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Foundation.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/If.thy --- a/src/FOL/ex/If.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/If.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/If.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Intro.thy --- a/src/FOL/ex/Intro.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Intro.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Intro.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Intuitionistic.thy --- a/src/FOL/ex/Intuitionistic.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Intuitionistic.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 - diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Miniscope.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Miniscope.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Nat.thy --- a/src/FOL/ex/Nat.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Nat.thy Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Nat.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Natural_Numbers.thy --- a/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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. diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Prolog.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Propositional_Cla.thy --- a/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Propositional_Int.thy --- a/src/FOL/ex/Propositional_Int.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Propositional_Int.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Quantifiers_Cla.thy --- a/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/ex/Quantifiers_Int.thy --- a/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/fologic.ML --- a/src/FOL/fologic.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/fologic.ML Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/fologic.ML - ID: $Id$ Author: Lawrence C Paulson Abstract syntax operations for FOL. diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/intprover.ML --- a/src/FOL/intprover.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/intprover.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/FOL/simpdata.ML Fri Jul 10 07:59:44 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/simpdata.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/IMP/Compiler.thy Fri Jul 10 07:59:44 2009 +0200 @@ -58,7 +58,7 @@ lemma [simp]: "(\[],q,s\ -n\ \p',q',t\) = (n=0 \ p' = [] \ q' = q \ t = s)" apply(rule iffI) - apply(erule converse_rel_powE, simp, fast) + apply(erule rel_pow_E2, simp, fast) apply simp done @@ -143,7 +143,7 @@ from H C2 obtain p' q' r' where 1: "\instr # tlC2 @ p1 @ p2, C1 @ q,r\ -1\ \p',q',r'\" and n: "\p',q',r'\ -n\ \p2,rev p1 @ rev C2 @ C1 @ q,t\" - by(fastsimp simp add:R_O_Rn_commute) + by(fastsimp simp add:rel_pow_commute) from CL closed_exec1[OF _ 1] C2 obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \ q' = C1' @ q" and same: "rev C1' @ C2' = rev C1 @ C2" diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/IMP/Machines.thy --- a/src/HOL/IMP/Machines.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/IMP/Machines.thy Fri Jul 10 07:59:44 2009 +0200 @@ -2,32 +2,13 @@ imports Natural begin -lemma rtrancl_eq: "R^* = Id \ (R O R^*)" - by (fast intro: rtrancl_into_rtrancl elim: rtranclE) - -lemma converse_rtrancl_eq: "R^* = Id \ (R^* O R)" - by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq) - -lemmas converse_rel_powE = rel_pow_E2 - -lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R" - by (induct n) (simp, simp add: O_assoc [symmetric]) - lemma converse_in_rel_pow_eq: "((x,z) \ R ^^ n) = (n=0 \ z=x \ (\m y. n = Suc m \ (x,y) \ R \ (y,z) \ R ^^ m))" apply(rule iffI) - apply(blast elim:converse_rel_powE) -apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute) + apply(blast elim:rel_pow_E2) +apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute) done -lemma rel_pow_plus: - "R ^^ (m+n) = R ^^ n O R ^^ m" - by (induct n) (simp, simp add: O_assoc) - -lemma rel_pow_plusI: - "\ (x,y) \ R ^^ m; (y,z) \ R ^^ n \ \ (x,z) \ R ^^ (m+n)" - by (simp add: rel_pow_plus rel_compI) - subsection "Instructions" text {* There are only three instructions: *} diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Library/Library/ROOT.ML --- a/src/HOL/Library/Library/ROOT.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Library/Library/ROOT.ML Fri Jul 10 07:59:44 2009 +0200 @@ -1,3 +1,1 @@ -(* $Id$ *) - use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"]; diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Library/Library/document/root.tex --- a/src/HOL/Library/Library/document/root.tex Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Library/Library/document/root.tex Fri Jul 10 07:59:44 2009 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{ifthen} \usepackage[latin1]{inputenc} diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Library/README.html --- a/src/HOL/Library/README.html Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Library/README.html Fri Jul 10 07:59:44 2009 +0200 @@ -1,7 +1,5 @@ - - diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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)))) *) diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/SizeChange/Correctness.thy --- a/src/HOL/SizeChange/Correctness.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/SizeChange/Correctness.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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) diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/SizeChange/Implementation.thy --- a/src/HOL/SizeChange/Implementation.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/SizeChange/Implementation.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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 \ bool" where diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/SizeChange/Kleene_Algebras.thy --- a/src/HOL/SizeChange/Kleene_Algebras.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy Fri Jul 10 07:59:44 2009 +0200 @@ -9,17 +9,19 @@ imports Main begin -text {* A type class of kleene algebras *} +text {* A type class of Kleene algebras *} class star = fixes star :: "'a \ 'a" class idem_add = ab_semigroup_add + assumes add_idem [simp]: "x + x = x" +begin -lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y" - unfolding add_assoc[symmetric] - by simp +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 \ b \ a + b = b" @@ -55,6 +57,15 @@ "x \ z \ y \ z \ x + y \ z" unfolding order_def by (simp add: add_assoc) +lemma less_add[simp]: "a \ a + b" "b \ a + b" +unfolding order_def by (auto simp:add_ac) + +lemma add_est1: "a + b \ c \ a \ c" +using less_add(1) by (rule order_trans) + +lemma add_est2: "a + b \ c \ b \ c" +using less_add(2) by (rule order_trans) + end class pre_kleene = semiring_1 + order_by_add @@ -95,22 +106,206 @@ and star2: "1 + star a * a \ star a" and star3: "a * x \ x \ star a * x \ x" and star4: "x * a \ x \ x * star a \ x" +begin + +lemma star3': + assumes a: "b + a * x \ x" + shows "star a * b \ x" +proof (rule order_trans) + from a have "b \ x" by (rule add_est1) + show "star a * b \ star a * x" + by (rule mult_mono) (auto simp:`b \ x`) + + from a have "a * x \ x" by (rule add_est2) + with star3 show "star a * x \ x" . +qed + +lemma star4': + assumes a: "b + x * a \ x" + shows "b * star a \ x" +proof (rule order_trans) + from a have "b \ x" by (rule add_est1) + show "b * star a \ x * star a" + by (rule mult_mono) (auto simp:`b \ x`) + + from a have "x * a \ x" by (rule add_est2) + with star4 show "x * star a \ 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) \ 1 + a * star a" + apply (rule add_mono, rule) + apply (rule mult_mono, auto) + apply (rule star1) + done + with star3' have "star a * 1 \ 1 + a * star a" . + thus "star a \ 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 \ 1 + star a * a" + apply (rule add_mono, rule) + apply (rule mult_mono, auto) + apply (rule star2) + done + with star4' have "1 * star a \ 1 + star a * a" . + thus "star a \ 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 \ star x" +by (metis less_add(1) star_unfold_left) + +lemma ka1: "x * star x \ 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 \ 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 \ x * star b" + proof (rule star3', rule order_trans) + from a have "a * x \ x * b" by simp + hence "a * x * star b \ x * b * star b" + by (rule mult_mono) auto + thus "x + a * (x * star b) \ x + x * b * star b" + using add_mono by (auto simp: mult_assoc) + show "\ \ x * star b" + proof - + have "x * (1 + b * star b) \ 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 \ star a * x" + proof (rule star4', rule order_trans) + from a have b: "x * b \ a * x" by simp + have "star a * x * b \ star a * a * x" + unfolding mult_assoc + by (rule mult_mono[OF _ b]) auto + thus "x + star a * x * b \ x + star a * a * x" + using add_mono by auto + show "\ \ star a * x" + proof - + have "(1 + star a * a) * x \ 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 "\ = p' * p * star (p' * a * p)" + by (simp add: mult_assoc) + also have "\ = star (p' * a * p)" + by (simp add: assms) + finally show ?thesis . +qed + +lemma x_less_star[simp]: "x \ x * star a" +proof - + have "x \ x * (1 + a * star a)" by (simp add: right_distrib) + also have "\ = x * star a" by (simp only: star_unfold_left) + finally show ?thesis . +qed + +lemma star_mono: "x \ y \ star x \ 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 \ 1 \ 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) \ 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) \ 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) \ 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) + \ star x * star (y * star x)" +by (metis ka16 ka17 left_distrib mult_assoc plus_leI) + +lemma kleene_church_rosser: + "star y * star x \ star x * star y \ star (x + y) \ star x * star y" +oops + +lemma star_decomp: "star (a + b) = star a * star (b * star a)" +oops + +lemma ka22: "y * star x \ star x * star y \ star y * star x \ 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 \ star x * star y \ y * star x \ star x * star y" +by (metis less_star mult_right_mono order_trans zero_minimum) + +lemma ka24: "star (x + y) \ 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 \ star x * star y \ star (star y * star x) \ star x * star y" +oops + +lemma kleene_bubblesort: "y * x \ x * y \ star (x + y) \ star x * star y" +oops + +end + +subsection {* Complete lattices are Kleene algebras *} + +lemma (in complete_lattice) le_SUPI': + assumes "l \ M i" + shows "l \ (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 (\n. a * b ^ n * c)" begin -lemma (in complete_lattice) le_SUPI': - assumes "l \ M i" - shows "l \ (SUP i. M i)" - using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I]) - -end - -instance kleene_by_complete_lattice < kleene +subclass kleene proof - fix a x :: 'a have [simp]: "1 \ star a" @@ -201,193 +396,19 @@ qed qed -lemma less_add[simp]: - fixes a b :: "'a :: order_by_add" - shows "a \ a + b" - and "b \ 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 \ c" - shows "a \ 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 \ c" - shows "b \ c" - using less_add(2) a - by (rule order_trans) - - -lemma star3': - fixes a b x :: "'a :: kleene" - assumes a: "b + a * x \ x" - shows "star a * b \ x" -proof (rule order_trans) - from a have "b \ x" by (rule add_est1) - show "star a * b \ star a * x" - by (rule mult_mono) (auto simp:`b \ x`) - - from a have "a * x \ x" by (rule add_est2) - with star3 show "star a * x \ x" . -qed - - -lemma star4': - fixes a b x :: "'a :: kleene" - assumes a: "b + x * a \ x" - shows "b * star a \ x" -proof (rule order_trans) - from a have "b \ x" by (rule add_est1) - show "b * star a \ x * star a" - by (rule mult_mono) (auto simp:`b \ x`) - - from a have "x * a \ x" by (rule add_est2) - with star4 show "x * star a \ 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) \ 1 + a * star a" - apply (rule add_mono, rule) - apply (rule mult_mono, auto) - apply (rule star1) - done - - with star3' have "star a * 1 \ 1 + a * star a" . - thus "star a \ 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 \ 1 + star a * a" - apply (rule add_mono, rule) - apply (rule mult_mono, auto) - apply (rule star2) - done - - with star4' have "1 * star a \ 1 + star a * a" . - thus "star a \ 1 + star a * a" by simp -qed +end -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 \ x * star b" - proof (rule star3', rule order_trans) - - from a have "a * x \ x * b" by simp - hence "a * x * star b \ x * b * star b" - by (rule mult_mono) auto - thus "x + a * (x * star b) \ x + x * b * star b" - using add_mono by (auto simp: mult_assoc) - - show "\ \ x * star b" - proof - - have "x * (1 + b * star b) \ 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 \ star a * x" - proof (rule star4', rule order_trans) - - from a have b: "x * b \ a * x" by simp - have "star a * x * b \ star a * a * x" - unfolding mult_assoc - by (rule mult_mono[OF _ b]) auto - thus "x + star a * x * b \ x + star a * a * x" - using add_mono by auto - - show "\ \ star a * x" - proof - - have "(1 + star a * a) * x \ 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 "\ = p' * p * star (p' * a * p)" - by (simp add: mult_assoc star_assoc) - also have "\ = star (p' * a * p)" - by (simp add: assms) - finally show ?thesis . -qed - -lemma star_mono: - fixes x y :: "'a :: kleene" - assumes "x \ y" - shows "star x \ star y" - oops - - - -(* Own lemmas *) - - -lemma x_less_star[simp]: - fixes x :: "'a :: kleene" - shows "x \ x * star a" -proof - - have "x \ x * (1 + a * star a)" by (simp add:right_distrib) - also have "\ = x * star a" by (simp only: star_unfold_left) - finally show ?thesis . -qed subsection {* Transitive Closure *} -definition - "tcl (x::'a::kleene) = star x * x" +context kleene +begin -lemma tcl_zero: - "tcl (0::'a::kleene) = 0" - unfolding tcl_def by simp +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 - @@ -395,7 +416,7 @@ 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) + by (simp add:tcl_def mult_assoc) qed lemma less_tcl: "a \ tcl a" @@ -405,6 +426,9 @@ finally show ?thesis . qed +end + + subsection {* Naive Algorithm to generate the transitive closure *} function (default "\x. 0", tailrec, domintros) @@ -421,31 +445,32 @@ in if XA \ 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: - fixes X :: "'a :: kleene" - shows "(X + X * A) * star A = X * star A" + "(X + X * A) * star A = X * star A" proof - have "A * star A \ 1 + A * star A" by simp also have "\ = 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) + thus ?thesis by (simp add:left_distrib right_distrib mult_assoc) qed lemma mk_tcl_lemma2: - fixes X :: "'a :: kleene" shows "X * A \ X \ X * star A = X" - by (rule order_antisym) (auto simp:star4) + by (rule antisym) (auto simp:star4) - - +end lemma mk_tcl_correctness: - fixes A X :: "'a :: {kleene}" + 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) + by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2) + lemma graph_implies_dom: "mk_tcl_graph x y \ mk_tcl_dom x" by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases) @@ -464,6 +489,6 @@ shows "mk_tcl A A = tcl A" using assms mk_tcl_default mk_tcl_correctness unfolding tcl_def - by (auto simp:star_commute) + by auto end diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Tools/Function/decompose.ML --- a/src/HOL/Tools/Function/decompose.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Tools/Function/decompose.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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) => diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Tools/Function/termination.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 **) diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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) = diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/Transitive_Closure.thy Fri Jul 10 07:59:44 2009 +0200 @@ -737,6 +737,9 @@ lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m" by(induct n) auto +lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R" + by (induct n) (simp, simp add: O_assoc [symmetric]) + lemma rtrancl_imp_UN_rel_pow: assumes "p \ R^*" shows "p \ (\n. R ^^ n)" diff -r 801aabf9f376 -r a290c36e94d6 src/HOL/ex/Formal_Power_Series_Examples.thy --- a/src/HOL/ex/Formal_Power_Series_Examples.thy Fri Jul 10 07:59:29 2009 +0200 +++ b/src/HOL/ex/Formal_Power_Series_Examples.thy Fri Jul 10 07:59:44 2009 +0200 @@ -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" diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 *) diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/General/graph.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/General/table.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/Isar/code.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/Isar/expression.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/Isar/rule_insts.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/Isar/theory_target.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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*) diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/consts.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/context.ML --- a/src/Pure/context.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/context.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/drule.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/logic.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/more_thm.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/proofterm.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 *****) diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/term_ord.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/term_subst.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 (); diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/thm.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/type_infer.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Pure/variable.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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); diff -r 801aabf9f376 -r a290c36e94d6 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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; diff -r 801aabf9f376 -r a290c36e94d6 src/Tools/Compute_Oracle/am_interpreter.ML --- a/src/Tools/Compute_Oracle/am_interpreter.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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 diff -r 801aabf9f376 -r a290c36e94d6 src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Fri Jul 10 07:59:29 2009 +0200 +++ b/src/Tools/Compute_Oracle/linker.ML Fri Jul 10 07:59:44 2009 +0200 @@ -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