--- a/src/HOL/Bali/Example.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/Bali/Example.thy Sat May 16 20:18:05 2009 +0200
@@ -1075,10 +1075,7 @@
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> =
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
, [Class Base])}"
-apply (unfold max_spec_def)
-apply (simp (no_asm) add: appl_methds_Base_foo)
-apply auto
-done
+by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
section "well-typedness"
--- a/src/HOL/HOL.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/HOL.thy Sat May 16 20:18:05 2009 +0200
@@ -1050,8 +1050,7 @@
"(P | False) = P" "(False | P) = P"
"(P | P) = P" "(P | (P | Q)) = (P | Q)" and
"(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x"
- -- {* needed for the one-point-rule quantifier simplification procs *}
- -- {* essential for termination!! *} and
+ and
"!!P. (EX x. x=t & P(x)) = P(t)"
"!!P. (EX x. t=x & P(x)) = P(t)"
"!!P. (ALL x. x=t --> P(x)) = P(t)"
--- a/src/HOL/Library/Binomial.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Sat May 16 20:18:05 2009 +0200
@@ -88,9 +88,7 @@
lemma card_s_0_eq_empty:
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
- apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
- apply (simp cong add: rev_conj_cong)
- done
+by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
lemma choose_deconstruct: "finite M ==> x \<notin> M
==> {s. s <= insert x M & card(s) = Suc k}
--- a/src/HOL/MicroJava/BV/BVExample.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sat May 16 20:18:05 2009 +0200
@@ -69,10 +69,10 @@
lemma subcls1:
"subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
- apply (simp add: subcls1_def2)
- apply (simp add: name_defs class_defs system_defs E_def class_def)
- apply (auto simp: expand_fun_eq split: split_if_asm)
- done
+apply (simp add: subcls1_def2 del:singleton_conj_conv2)
+apply (simp add: name_defs class_defs system_defs E_def class_def)
+apply (auto simp: expand_fun_eq split: split_if_asm)
+done
text {* The subclass relation is acyclic; hence its converse is well founded: *}
lemma notin_rtrancl:
--- a/src/HOL/NanoJava/TypeRel.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Sat May 16 20:18:05 2009 +0200
@@ -56,7 +56,7 @@
"subcls1 =
(SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
apply (unfold subcls1_def is_class_def)
-apply auto
+apply (auto split:split_if_asm)
done
lemma finite_subcls1: "finite subcls1"
--- a/src/HOL/Set.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOL/Set.thy Sat May 16 20:18:05 2009 +0200
@@ -1034,6 +1034,29 @@
subsubsection {* Set reasoning tools *}
+text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
+
+lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
+by auto
+
+lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
+by auto
+
+ML{*
+ local
+ val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+ ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+ DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+ in
+ val defColl_regroup = Simplifier.simproc (the_context ())
+ "defined Collect" ["{x. P x & Q x}"]
+ (Quantifier1.rearrange_Coll Coll_perm_tac)
+ end;
+
+ Addsimprocs [defColl_regroup];
+
+*}
+
text {*
Rewrite rules for boolean case-splitting: faster than @{text
"split_if [split]"}.
--- a/src/HOLCF/Algebraic.thy Fri May 15 16:39:19 2009 +0200
+++ b/src/HOLCF/Algebraic.thy Sat May 16 20:18:05 2009 +0200
@@ -29,6 +29,11 @@
thus "P i j" using step trans by (rule less_Suc_induct)
qed
+definition
+ eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
+where
+ "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
+
text {* A pre-deflation is like a deflation, but not idempotent. *}
locale pre_deflation =
@@ -103,9 +108,10 @@
abbreviation
d :: "'a \<rightarrow> 'a"
where
- "d \<equiv> eventual (\<lambda>n. iterate n\<cdot>f)"
+ "d \<equiv> eventual_iterate f"
lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
+unfolding eventual_iterate_def
using eventually_constant_iterate by (rule MOST_eventual)
lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
@@ -134,6 +140,7 @@
proof
fix x :: 'a
have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
+ unfolding eventual_iterate_def
using eventually_constant_iterate
by (rule eventual_mem_range)
then obtain n where n: "d = iterate n\<cdot>f" ..
@@ -153,9 +160,17 @@
by (simp add: d_fixed_iff)
qed
+lemma deflation_d: "deflation d"
+using finite_deflation_d
+by (rule finite_deflation_imp_deflation)
+
end
-lemma pre_deflation_d_f:
+lemma finite_deflation_eventual_iterate:
+ "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
+by (rule pre_deflation.finite_deflation_d)
+
+lemma pre_deflation_oo:
assumes "finite_deflation d"
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
shows "pre_deflation (d oo f)"
@@ -171,13 +186,13 @@
lemma eventual_iterate_oo_fixed_iff:
assumes "finite_deflation d"
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
- shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
+ shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
proof -
interpret d: finite_deflation d by fact
let ?e = "d oo f"
interpret e: pre_deflation "d oo f"
using `finite_deflation d` f
- by (rule pre_deflation_d_f)
+ by (rule pre_deflation_oo)
let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
show ?thesis
apply (subst e.d_fixed_iff)
@@ -192,6 +207,94 @@
done
qed
+lemma eventual_mono:
+ assumes A: "eventually_constant A"
+ assumes B: "eventually_constant B"
+ assumes below: "\<And>n. A n \<sqsubseteq> B n"
+ shows "eventual A \<sqsubseteq> eventual B"
+proof -
+ from A have "MOST n. A n = eventual A"
+ by (rule MOST_eq_eventual)
+ then have "MOST n. eventual A \<sqsubseteq> B n"
+ by (rule MOST_mono) (erule subst, rule below)
+ with B show "eventual A \<sqsubseteq> eventual B"
+ by (rule MOST_eventual)
+qed
+
+lemma eventual_iterate_mono:
+ assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
+ shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
+unfolding eventual_iterate_def
+apply (rule eventual_mono)
+apply (rule pre_deflation.eventually_constant_iterate [OF f])
+apply (rule pre_deflation.eventually_constant_iterate [OF g])
+apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
+done
+
+lemma cont2cont_eventual_iterate_oo:
+ assumes d: "finite_deflation d"
+ assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+ shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
+ (is "cont ?e")
+proof (rule contI2)
+ show "monofun ?e"
+ apply (rule monofunI)
+ apply (rule eventual_iterate_mono)
+ apply (rule pre_deflation_oo [OF d below])
+ apply (rule pre_deflation_oo [OF d below])
+ apply (rule monofun_cfun_arg)
+ apply (erule cont2monofunE [OF cont])
+ done
+next
+ fix Y :: "nat \<Rightarrow> 'b"
+ assume Y: "chain Y"
+ with cont have fY: "chain (\<lambda>i. f (Y i))"
+ by (rule ch2ch_cont)
+ assume eY: "chain (\<lambda>i. ?e (Y i))"
+ have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
+ by (rule admD [OF _ Y], simp add: cont, rule below)
+ have "deflation (?e (\<Squnion>i. Y i))"
+ apply (rule pre_deflation.deflation_d)
+ apply (rule pre_deflation_oo [OF d lub_below])
+ done
+ then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
+ proof (rule deflation.belowI)
+ fix x :: 'a
+ assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
+ hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
+ by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
+ hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
+ apply (simp only: cont2contlubE [OF cont Y])
+ apply (simp only: contlub_cfun_fun [OF fY])
+ done
+ have "compact (d\<cdot>x)"
+ using d by (rule finite_deflation.compact)
+ then have "compact x"
+ using `d\<cdot>x = x` by simp
+ then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
+ using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
+ then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
+ by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
+ then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
+ then have "f (Y n)\<cdot>x = x"
+ using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
+ with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
+ by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
+ moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
+ by (rule is_ub_thelub, simp add: eY)
+ ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
+ by (simp add: contlub_cfun_fun eY)
+ also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
+ apply (rule deflation.below)
+ apply (rule admD [OF adm_deflation eY])
+ apply (rule pre_deflation.deflation_d)
+ apply (rule pre_deflation_oo [OF d below])
+ done
+ finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
+ qed
+qed
+
+
subsection {* Type constructor for finite deflations *}
defaultsort profinite
@@ -214,6 +317,10 @@
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp
+lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
+using finite_deflation_Rep_fin_defl
+by (rule finite_deflation_imp_deflation)
+
interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)
@@ -244,27 +351,69 @@
subsection {* Take function for finite deflations *}
definition
+ defl_approx :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
+where
+ "defl_approx i d = eventual_iterate (approx i oo d)"
+
+lemma finite_deflation_defl_approx:
+ "deflation d \<Longrightarrow> finite_deflation (defl_approx i d)"
+unfolding defl_approx_def
+apply (rule pre_deflation.finite_deflation_d)
+apply (rule pre_deflation_oo)
+apply (rule finite_deflation_approx)
+apply (erule deflation.below)
+done
+
+lemma deflation_defl_approx:
+ "deflation d \<Longrightarrow> deflation (defl_approx i d)"
+apply (rule finite_deflation_imp_deflation)
+apply (erule finite_deflation_defl_approx)
+done
+
+lemma defl_approx_fixed_iff:
+ "deflation d \<Longrightarrow> defl_approx i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
+unfolding defl_approx_def
+apply (rule eventual_iterate_oo_fixed_iff)
+apply (rule finite_deflation_approx)
+apply (erule deflation.below)
+done
+
+lemma defl_approx_below:
+ "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_approx i a \<sqsubseteq> defl_approx i b"
+apply (rule deflation.belowI)
+apply (erule deflation_defl_approx)
+apply (simp add: defl_approx_fixed_iff)
+apply (erule (1) deflation.belowD)
+apply (erule conjunct2)
+done
+
+lemma cont2cont_defl_approx:
+ assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+ shows "cont (\<lambda>x. defl_approx i (f x))"
+unfolding defl_approx_def
+using finite_deflation_approx assms
+by (rule cont2cont_eventual_iterate_oo)
+
+definition
fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
where
- "fd_take i d = Abs_fin_defl (eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d)))"
+ "fd_take i d = Abs_fin_defl (defl_approx i (Rep_fin_defl d))"
lemma Rep_fin_defl_fd_take:
- "Rep_fin_defl (fd_take i d) =
- eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d))"
+ "Rep_fin_defl (fd_take i d) = defl_approx i (Rep_fin_defl d)"
unfolding fd_take_def
apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
-apply (rule pre_deflation.finite_deflation_d)
-apply (rule pre_deflation_d_f)
-apply (rule finite_deflation_approx)
-apply (rule Rep_fin_defl.below)
+apply (rule finite_deflation_defl_approx)
+apply (rule deflation_Rep_fin_defl)
done
lemma fd_take_fixed_iff:
"Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
unfolding Rep_fin_defl_fd_take
-by (rule eventual_iterate_oo_fixed_iff
- [OF finite_deflation_approx Rep_fin_defl.below])
+apply (rule defl_approx_fixed_iff)
+apply (rule deflation_Rep_fin_defl)
+done
lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
apply (rule fin_defl_belowI)
@@ -463,6 +612,41 @@
interpretation cast: deflation "cast\<cdot>d"
by (rule deflation_cast)
+lemma cast_approx: "cast\<cdot>(approx n\<cdot>A) = defl_approx n (cast\<cdot>A)"
+apply (rule alg_defl.principal_induct)
+apply (rule adm_eq)
+apply simp
+apply (simp add: cont2cont_defl_approx cast.below)
+apply (simp only: approx_alg_defl_principal)
+apply (simp only: cast_alg_defl_principal)
+apply (simp only: Rep_fin_defl_fd_take)
+done
+
+lemma cast_approx_fixed_iff:
+ "cast\<cdot>(approx i\<cdot>A)\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> cast\<cdot>A\<cdot>x = x"
+apply (simp only: cast_approx)
+apply (rule defl_approx_fixed_iff)
+apply (rule deflation_cast)
+done
+
+lemma defl_approx_cast: "defl_approx i (cast\<cdot>A) = cast\<cdot>(approx i\<cdot>A)"
+by (rule cast_approx [symmetric])
+
+lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
+apply (rule profinite_below_ext)
+apply (drule_tac i=i in defl_approx_below)
+apply (rule deflation_cast)
+apply (rule deflation_cast)
+apply (simp only: defl_approx_cast)
+apply (cut_tac x="approx i\<cdot>A" in alg_defl.compact_imp_principal)
+apply (rule compact_approx)
+apply (cut_tac x="approx i\<cdot>B" in alg_defl.compact_imp_principal)
+apply (rule compact_approx)
+apply clarsimp
+apply (simp add: cast_alg_defl_principal)
+apply (simp add: below_fin_defl_def)
+done
+
lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
apply (subst contlub_cfun_arg)
apply (rule chainI)
--- a/src/HOLCF/Tools/domain/domain_extender.ML Fri May 15 16:39:19 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat May 16 20:18:05 2009 +0200
@@ -6,11 +6,13 @@
signature DOMAIN_EXTENDER =
sig
- val add_domain_cmd: string -> (string list * binding * mixfix *
- (binding * (bool * binding option * string) list * mixfix) list) list
+ val add_domain_cmd: string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
- val add_domain: string -> (string list * binding * mixfix *
- (binding * (bool * binding option * typ) list * mixfix) list) list
+ val add_domain: string ->
+ ((string * string option) list * binding * mixfix *
+ (binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
end;
@@ -22,7 +24,7 @@
(* ----- general testing and preprocessing of constructor list -------------- *)
fun check_and_sort_domain
(dtnvs : (string * typ list) list)
- (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list)
+ (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
(sg : theory)
: ((string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list) list =
@@ -73,9 +75,15 @@
quote (string_of_typ sg t) ^
" with different arguments"))
| analyse indirect (TVar _) = Imposs "extender:analyse";
- fun check_pcpo T = if pcpo_type sg T then T
- else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
- val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false)));
+ fun check_pcpo lazy T =
+ let val ok = if lazy then cpo_type else pcpo_type
+ in if ok sg T then T else error
+ ("Constructor argument type is not of sort pcpo: " ^
+ string_of_typ sg T)
+ end;
+ fun analyse_arg (lazy, sel, T) =
+ (lazy, sel, check_pcpo lazy (analyse false T));
+ fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
in ((dname,distinct_typevars), map analyse_con cons') end;
in ListPair.map analyse_equation (dtnvs,cons'')
end; (* let *)
@@ -85,12 +93,16 @@
fun gen_add_domain
(prep_typ : theory -> 'a -> typ)
(comp_dnam : string)
- (eqs''' : (string list * binding * mixfix *
+ (eqs''' : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy''' : theory) =
let
+ fun readS (SOME s) = Syntax.read_sort_global thy''' s
+ | readS NONE = Sign.defaultS thy''';
+ fun readTFree (a, s) = TFree (a, readS s);
+
val dtnvs = map (fn (vs,dname:binding,mx,_) =>
- (dname, map (Syntax.read_typ_global thy''') vs, mx)) eqs''';
+ (dname, map readTFree vs, mx)) eqs''';
val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
@@ -148,10 +160,10 @@
val cons_decl =
P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
-val type_var' =
- (P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
+val type_var' : (string * string option) parser =
+ (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
-val type_args' =
+val type_args' : (string * string option) list parser =
type_var' >> single ||
P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
Scan.succeed [];
@@ -164,11 +176,12 @@
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
P.and_list1 domain_decl;
-fun mk_domain (opt_name : string option, doms : (((string list * binding) * mixfix) *
+fun mk_domain (opt_name : string option,
+ doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
- val specs : (string list * binding * mixfix *
+ val specs : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list =
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
--- a/src/HOLCF/Tools/domain/domain_library.ML Fri May 15 16:39:19 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Sat May 16 20:18:05 2009 +0200
@@ -52,6 +52,7 @@
signature DOMAIN_LIBRARY =
sig
val Imposs : string -> 'a;
+ val cpo_type : theory -> typ -> bool;
val pcpo_type : theory -> typ -> bool;
val string_of_typ : theory -> typ -> string;
@@ -190,6 +191,7 @@
| index_vnames([],occupied) = [];
in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
+fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 15 16:39:19 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sat May 16 20:18:05 2009 +0200
@@ -12,6 +12,8 @@
sig
val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+ val quiet_mode: bool ref;
+ val trace_domain: bool ref;
end;
structure Domain_Theorems :> DOMAIN_THEOREMS =
--- a/src/Provers/quantifier1.ML Fri May 15 16:39:19 2009 +0200
+++ b/src/Provers/quantifier1.ML Sat May 16 20:18:05 2009 +0200
@@ -21,11 +21,21 @@
"!x. x=t --> P(x)" is covered by the congreunce rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
As must be "? x. t=x & P(x)".
-
And similarly for the bounded quantifiers.
Gries etc call this the "1 point rules"
+
+The above also works for !x1..xn. and ?x1..xn by moving the defined
+qunatifier inside first, but not for nested bounded quantifiers.
+
+For set comprehensions the basic permutations
+ ... & x = t & ... -> x = t & (... & ...)
+ ... & t = x & ... -> t = x & (... & ...)
+are also exported.
+
+To avoid looping, NONE is returned if the term cannot be rearranged,
+esp if x=t/t=x sits at the front already.
*)
signature QUANTIFIER1_DATA =
@@ -61,6 +71,7 @@
val rearrange_ex: theory -> simpset -> term -> thm option
val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option
+ val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
end;
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -70,29 +81,28 @@
(* FIXME: only test! *)
fun def xs eq =
- let val n = length xs
- in case dest_eq eq of
- SOME(c,s,t) =>
- s = Bound n andalso not(loose_bvar1(t,n)) orelse
- t = Bound n andalso not(loose_bvar1(s,n))
- | NONE => false
- end;
+ (case dest_eq eq of
+ SOME(c,s,t) =>
+ let val n = length xs
+ in s = Bound n andalso not(loose_bvar1(t,n)) orelse
+ t = Bound n andalso not(loose_bvar1(s,n)) end
+ | NONE => false);
-fun extract_conj xs t = case dest_conj t of NONE => NONE
+fun extract_conj fst xs t = case dest_conj t of NONE => NONE
| SOME(conj,P,Q) =>
- (if def xs P then SOME(xs,P,Q) else
+ (if not fst andalso def xs P then SOME(xs,P,Q) else
if def xs Q then SOME(xs,Q,P) else
- (case extract_conj xs P of
+ (case extract_conj false xs P of
SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
- | NONE => (case extract_conj xs Q of
+ | NONE => (case extract_conj false xs Q of
SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q')
| NONE => NONE)));
-fun extract_imp xs t = case dest_imp t of NONE => NONE
- | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
- else (case extract_conj xs P of
+fun extract_imp fst xs t = case dest_imp t of NONE => NONE
+ | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
+ else (case extract_conj false xs P of
SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
- | NONE => (case extract_imp xs Q of
+ | NONE => (case extract_imp false xs Q of
NONE => NONE
| SOME(xs,eq,Q') =>
SOME(xs,eq,imp$P$Q')));
@@ -100,8 +110,8 @@
fun extract_quant extract q =
let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
if qa = q then exqu ((qC,x,T)::xs) Q else NONE
- | exqu xs P = extract xs P
- in exqu end;
+ | exqu xs P = extract (null xs) xs P
+ in exqu [] end;
fun prove_conv tac thy tu =
Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
@@ -147,7 +157,7 @@
in quant xs (qC $ Abs(x,T,Q)) end;
fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
- (case extract_quant extract_imp q [] P of
+ (case extract_quant extract_imp q P of
NONE => NONE
| SOME(xs,eq,Q) =>
let val R = quantify all x T xs (imp $ eq $ Q)
@@ -155,7 +165,7 @@
| rearrange_all _ _ _ = NONE;
fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
- (case extract_imp [] P of
+ (case extract_imp true [] P of
NONE => NONE
| SOME(xs,eq,Q) => if not(null xs) then NONE else
let val R = imp $ eq $ Q
@@ -163,7 +173,7 @@
| rearrange_ball _ _ _ _ = NONE;
fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
- (case extract_quant extract_conj q [] P of
+ (case extract_quant extract_conj q P of
NONE => NONE
| SOME(xs,eq,Q) =>
let val R = quantify ex x T xs (conj $ eq $ Q)
@@ -171,10 +181,17 @@
| rearrange_ex _ _ _ = NONE;
fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
- (case extract_conj [] P of
+ (case extract_conj true [] P of
NONE => NONE
| SOME(xs,eq,Q) => if not(null xs) then NONE else
SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
| rearrange_bex _ _ _ _ = NONE;
+fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
+ (case extract_conj true [] P of
+ NONE => NONE
+ | SOME(_,eq,Q) =>
+ let val R = Coll $ Abs(x,T, conj $ eq $ Q)
+ in SOME(prove_conv tac thy (F,R)) end);
+
end;