author haftmann Sat, 16 May 2009 20:18:05 +0200 changeset 31187 7893975cc527 parent 31184 6dc73ea0dbc0 (current diff) parent 31168 138eae508556 (diff) child 31188 e5d01f8a916d
merged
```--- 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 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: rev_conj_cong)
-  done

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: name_defs class_defs system_defs E_def class_def)
-  apply (auto simp: expand_fun_eq split: split_if_asm)
-  done
+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;
+
+
+*}
+
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 @@
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 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 (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 simp
+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
+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
+    ((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
+    ((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 @@
(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
+      | readS NONE = Sign.defaultS thy''';
+
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;```