--- 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
--- 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
*)
--- 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";
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
-
--- 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
--- 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
*)
--- 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.
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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.
--- 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
--- 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
--- 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]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> 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: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
- 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 \<and> q' = C1' @ q"
and same: "rev C1' @ C2' = rev C1 @ C2"
--- 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 \<union> (R O R^*)"
- by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
-
-lemma converse_rtrancl_eq: "R^* = Id \<union> (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) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> 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:
- "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
- by (simp add: rel_pow_plus rel_compI)
-
subsection "Instructions"
text {* There are only three instructions: *}
--- 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
--- 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"];
--- 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}
--- 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 @@
<!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/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;
--- 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
--- 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)))) *)
--- 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)
--- 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 \<Rightarrow> bool"
where
--- 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 \<Rightarrow> '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 \<le> b \<longleftrightarrow> a + b = b"
@@ -55,6 +57,15 @@
"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
@@ -95,22 +106,206 @@
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
-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
+subclass kleene
proof
-
fix a x :: 'a
have [simp]: "1 \<le> star a"
@@ -201,193 +396,19 @@
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
+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 \<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"
+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 \<le> tcl a"
@@ -405,6 +426,9 @@
finally show ?thesis .
qed
+end
+
+
subsection {* Naive Algorithm to generate the transitive closure *}
function (default "\<lambda>x. 0", tailrec, domintros)
@@ -421,31 +445,32 @@
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:
- 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 \<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)
+ thus ?thesis by (simp add:left_distrib right_distrib mult_assoc)
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)
+ 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 \<Longrightarrow> 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
--- 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) =>
--- 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 **)
--- 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) =
--- 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 \<in> R^*"
shows "p \<in> (\<Union>n. R ^^ n)"
--- 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"
--- 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 *)
--- 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);
--- 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);
--- 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
--- 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;
--- 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;
--- 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*)
--- 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;
--- 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
--- 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;
--- 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);
--- 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);
--- 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 *****)
--- 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);
--- 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 ();
--- 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
--- 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;
--- 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);
--- 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;
--- 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
--- 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
--- 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