# HG changeset patch # User haftmann # Date 1242497909 -7200 # Node ID e5d01f8a916db1c71b905407a7409dd22bee0749 # Parent 7893975cc5273d9015ecfe4e1621da44f09290dc# Parent b458b4ac570f979fa1993f093419b3bef8b0c2bb merged diff -r b458b4ac570f -r e5d01f8a916d src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/Bali/Example.thy Sat May 16 20:18:29 2009 +0200 @@ -1075,10 +1075,7 @@ lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \name=foo,parTs=[NT]\ = {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) , [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" diff -r b458b4ac570f -r e5d01f8a916d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/HOL.thy Sat May 16 20:18:29 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)" diff -r b458b4ac570f -r e5d01f8a916d src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/Library/Binomial.thy Sat May 16 20:18:29 2009 +0200 @@ -88,9 +88,7 @@ lemma card_s_0_eq_empty: "finite A ==> card {B. B \ 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 \ M ==> {s. s <= insert x M & card(s) = Suc k} diff -r b458b4ac570f -r e5d01f8a916d src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Sat May 16 20:18:29 2009 +0200 @@ -69,10 +69,10 @@ lemma subcls1: "subcls1 E = (\C D. (C, D) \ {(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: diff -r b458b4ac570f -r e5d01f8a916d src/HOL/NanoJava/TypeRel.thy --- a/src/HOL/NanoJava/TypeRel.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Sat May 16 20:18:29 2009 +0200 @@ -56,7 +56,7 @@ "subcls1 = (SIGMA C: {C. is_class C} . {D. C\Object \ 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" diff -r b458b4ac570f -r e5d01f8a916d src/HOL/Set.thy --- a/src/HOL/Set.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOL/Set.thy Sat May 16 20:18:29 2009 +0200 @@ -1034,6 +1034,29 @@ subsubsection {* Set reasoning tools *} +text{* Elimination of @{text"{x. \ & x=t & \}"}. *} + +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]"}. diff -r b458b4ac570f -r e5d01f8a916d src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Sat May 16 20:16:49 2009 +0200 +++ b/src/HOLCF/Algebraic.thy Sat May 16 20:18:29 2009 +0200 @@ -29,6 +29,11 @@ thus "P i j" using step trans by (rule less_Suc_induct) qed +definition + eventual_iterate :: "('a \ 'a::cpo) \ ('a \ 'a)" +where + "eventual_iterate f = eventual (\n. iterate n\f)" + text {* A pre-deflation is like a deflation, but not idempotent. *} locale pre_deflation = @@ -103,9 +108,10 @@ abbreviation d :: "'a \ 'a" where - "d \ eventual (\n. iterate n\f)" + "d \ eventual_iterate f" lemma MOST_d: "MOST n. P (iterate n\f) \ P d" +unfolding eventual_iterate_def using eventually_constant_iterate by (rule MOST_eventual) lemma f_d: "f\(d\x) = d\x" @@ -134,6 +140,7 @@ proof fix x :: 'a have "d \ range (\n. iterate n\f)" + unfolding eventual_iterate_def using eventually_constant_iterate by (rule eventual_mem_range) then obtain n where n: "d = iterate n\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 \ finite_deflation (eventual_iterate d)" +by (rule pre_deflation.finite_deflation_d) + +lemma pre_deflation_oo: assumes "finite_deflation d" assumes f: "\x. f\x \ x" shows "pre_deflation (d oo f)" @@ -171,13 +186,13 @@ lemma eventual_iterate_oo_fixed_iff: assumes "finite_deflation d" assumes f: "\x. f\x \ x" - shows "eventual (\n. iterate n\(d oo f))\x = x \ d\x = x \ f\x = x" + shows "eventual_iterate (d oo f)\x = x \ d\x = x \ f\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 (\n. iterate n\?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: "\n. A n \ B n" + shows "eventual A \ eventual B" +proof - + from A have "MOST n. A n = eventual A" + by (rule MOST_eq_eventual) + then have "MOST n. eventual A \ B n" + by (rule MOST_mono) (erule subst, rule below) + with B show "eventual A \ eventual B" + by (rule MOST_eventual) +qed + +lemma eventual_iterate_mono: + assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \ g" + shows "eventual_iterate f \ 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 \ g`]) +done + +lemma cont2cont_eventual_iterate_oo: + assumes d: "finite_deflation d" + assumes cont: "cont f" and below: "\x y. f x\y \ y" + shows "cont (\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 \ 'b" + assume Y: "chain Y" + with cont have fY: "chain (\i. f (Y i))" + by (rule ch2ch_cont) + assume eY: "chain (\i. ?e (Y i))" + have lub_below: "\x. f (\i. Y i)\x \ x" + by (rule admD [OF _ Y], simp add: cont, rule below) + have "deflation (?e (\i. Y i))" + apply (rule pre_deflation.deflation_d) + apply (rule pre_deflation_oo [OF d lub_below]) + done + then show "?e (\i. Y i) \ (\i. ?e (Y i))" + proof (rule deflation.belowI) + fix x :: 'a + assume "?e (\i. Y i)\x = x" + hence "d\x = x" and "f (\i. Y i)\x = x" + by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below]) + hence "(\i. f (Y i)\x) = x" + apply (simp only: cont2contlubE [OF cont Y]) + apply (simp only: contlub_cfun_fun [OF fY]) + done + have "compact (d\x)" + using d by (rule finite_deflation.compact) + then have "compact x" + using `d\x = x` by simp + then have "compact (\i. f (Y i)\x)" + using `(\i. f (Y i)\x) = x` by simp + then have "\n. max_in_chain n (\i. f (Y i)\x)" + by - (rule compact_imp_max_in_chain, simp add: fY, assumption) + then obtain n where n: "max_in_chain n (\i. f (Y i)\x)" .. + then have "f (Y n)\x = x" + using `(\i. f (Y i)\x) = x` fY by (simp add: maxinch_is_thelub) + with `d\x = x` have "?e (Y n)\x = x" + by (simp add: eventual_iterate_oo_fixed_iff [OF d below]) + moreover have "?e (Y n)\x \ (\i. ?e (Y i)\x)" + by (rule is_ub_thelub, simp add: eY) + ultimately have "x \ (\i. ?e (Y i))\x" + by (simp add: contlub_cfun_fun eY) + also have "(\i. ?e (Y i))\x \ 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 "(\i. ?e (Y i))\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 \ ('a \ 'a) \ ('a \ 'a)" +where + "defl_approx i d = eventual_iterate (approx i oo d)" + +lemma finite_deflation_defl_approx: + "deflation d \ 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 \ 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 \ defl_approx i d\x = x \ approx i\x = x \ d\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: + "\a \ b; deflation a; deflation b\ \ defl_approx i a \ 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: "\x y. f x\y \ y" + shows "cont (\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 \ 'a fin_defl \ 'a fin_defl" where - "fd_take i d = Abs_fin_defl (eventual (\n. iterate n\(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 (\n. iterate n\(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)\x = x \ approx i\x = x \ Rep_fin_defl d\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 \ d" apply (rule fin_defl_belowI) @@ -463,6 +612,41 @@ interpretation cast: deflation "cast\d" by (rule deflation_cast) +lemma cast_approx: "cast\(approx n\A) = defl_approx n (cast\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\(approx i\A)\x = x \ approx i\x = x \ cast\A\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\A) = cast\(approx i\A)" +by (rule cast_approx [symmetric]) + +lemma cast_below_imp_below: "cast\A \ cast\B \ A \ 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\A" in alg_defl.compact_imp_principal) +apply (rule compact_approx) +apply (cut_tac x="approx i\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\(\i. alg_defl_principal (Abs_fin_defl (approx i)))\x = x" apply (subst contlub_cfun_arg) apply (rule chainI) diff -r b458b4ac570f -r e5d01f8a916d src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Sat May 16 20:16:49 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat May 16 20:18:29 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; diff -r b458b4ac570f -r e5d01f8a916d src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Sat May 16 20:16:49 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Sat May 16 20:18:29 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; diff -r b458b4ac570f -r e5d01f8a916d src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Sat May 16 20:16:49 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sat May 16 20:18:29 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 = diff -r b458b4ac570f -r e5d01f8a916d src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Sat May 16 20:16:49 2009 +0200 +++ b/src/Provers/quantifier1.ML Sat May 16 20:18:29 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;