# HG changeset patch # User bulwahn # Date 1292435114 -3600 # Node ID 5391d34b0f4c1107a25b870294234be8f9f37912 # Parent f4d3acf0c4cc0c489d91bb5ac2a724ec464afa50# Parent 5a9543f95cc62734e756a34fcf4ba16a0df96c0f merged diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Import/replay.ML Wed Dec 15 18:45:14 2010 +0100 @@ -2,11 +2,9 @@ Author: Sebastian Skalberg (TU Muenchen) *) -structure Replay = +structure Replay = (* FIXME proper signature *) struct -structure P = ProofKernel - open ProofKernel open ImportRecorder @@ -17,12 +15,12 @@ fun replay_proof int_thms thyname thmname prf thy = let val _ = ImportRecorder.start_replay_proof thyname thmname - fun rp (PRefl tm) thy = P.REFL tm thy + fun rp (PRefl tm) thy = ProofKernel.REFL tm thy | rp (PInstT(p,lambda)) thy = let val (thy',th) = rp' p thy in - P.INST_TYPE lambda th thy' + ProofKernel.INST_TYPE lambda th thy' end | rp (PSubst(prfs,ctxt,prf)) thy = let @@ -34,52 +32,52 @@ end) prfs (thy,[]) val (thy'',th) = rp' prf thy' in - P.SUBST ths ctxt th thy'' + ProofKernel.SUBST ths ctxt th thy'' end | rp (PAbs(prf,v)) thy = let val (thy',th) = rp' prf thy in - P.ABS v th thy' + ProofKernel.ABS v th thy' end | rp (PDisch(prf,tm)) thy = let val (thy',th) = rp' prf thy in - P.DISCH tm th thy' + ProofKernel.DISCH tm th thy' end | rp (PMp(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.MP th1 th2 thy2 + ProofKernel.MP th1 th2 thy2 end - | rp (PHyp tm) thy = P.ASSUME tm thy + | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy | rp (PDef(seg,name,rhs)) thy = - (case P.get_def seg name rhs thy of + (case ProofKernel.get_def seg name rhs thy of (thy',SOME res) => (thy',res) | (thy',NONE) => if seg = thyname - then P.new_definition seg name rhs thy' + then ProofKernel.new_definition seg name rhs thy' else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname)) - | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE" + | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE" | rp (PSpec(prf,tm)) thy = let val (thy',th) = rp' prf thy in - P.SPEC tm th thy' + ProofKernel.SPEC tm th thy' end | rp (PInst(prf,theta)) thy = let val (thy',th) = rp' prf thy in - P.INST theta th thy' + ProofKernel.INST theta th thy' end | rp (PGen(prf,v)) thy = let val (thy',th) = rp' prf thy - val p = P.GEN v th thy' + val p = ProofKernel.GEN v th thy' in p end @@ -87,91 +85,91 @@ let val (thy',th) = rp' prf thy in - P.GEN_ABS opt vl th thy' + ProofKernel.GEN_ABS opt vl th thy' end | rp (PImpAS(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.IMP_ANTISYM th1 th2 thy2 + ProofKernel.IMP_ANTISYM th1 th2 thy2 end | rp (PSym prf) thy = let val (thy1,th) = rp' prf thy in - P.SYM th thy1 + ProofKernel.SYM th thy1 end | rp (PTrans(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.TRANS th1 th2 thy2 + ProofKernel.TRANS th1 th2 thy2 end | rp (PComb(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.COMB th1 th2 thy2 + ProofKernel.COMB th1 th2 thy2 end | rp (PEqMp(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.EQ_MP th1 th2 thy2 + ProofKernel.EQ_MP th1 th2 thy2 end | rp (PEqImp prf) thy = let val (thy',th) = rp' prf thy in - P.EQ_IMP_RULE th thy' + ProofKernel.EQ_IMP_RULE th thy' end | rp (PExists(prf,ex,wit)) thy = let val (thy',th) = rp' prf thy in - P.EXISTS ex wit th thy' + ProofKernel.EXISTS ex wit th thy' end | rp (PChoose(v,prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.CHOOSE v th1 th2 thy2 + ProofKernel.CHOOSE v th1 th2 thy2 end | rp (PConj(prf1,prf2)) thy = let val (thy1,th1) = rp' prf1 thy val (thy2,th2) = rp' prf2 thy1 in - P.CONJ th1 th2 thy2 + ProofKernel.CONJ th1 th2 thy2 end | rp (PConjunct1 prf) thy = let val (thy',th) = rp' prf thy in - P.CONJUNCT1 th thy' + ProofKernel.CONJUNCT1 th thy' end | rp (PConjunct2 prf) thy = let val (thy',th) = rp' prf thy in - P.CONJUNCT2 th thy' + ProofKernel.CONJUNCT2 th thy' end | rp (PDisj1(prf,tm)) thy = let val (thy',th) = rp' prf thy in - P.DISJ1 th tm thy' + ProofKernel.DISJ1 th tm thy' end | rp (PDisj2(prf,tm)) thy = let val (thy',th) = rp' prf thy in - P.DISJ2 tm th thy' + ProofKernel.DISJ2 tm th thy' end | rp (PDisjCases(prf,prf1,prf2)) thy = let @@ -179,25 +177,25 @@ val (thy1,th1) = rp' prf1 thy' val (thy2,th2) = rp' prf2 thy1 in - P.DISJ_CASES th th1 th2 thy2 + ProofKernel.DISJ_CASES th th1 th2 thy2 end | rp (PNotI prf) thy = let val (thy',th) = rp' prf thy in - P.NOT_INTRO th thy' + ProofKernel.NOT_INTRO th thy' end | rp (PNotE prf) thy = let val (thy',th) = rp' prf thy in - P.NOT_ELIM th thy' + ProofKernel.NOT_ELIM th thy' end | rp (PContr(prf,tm)) thy = let val (thy',th) = rp' prf thy in - P.CCONTR tm th thy' + ProofKernel.CCONTR tm th thy' end | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)" | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)" @@ -226,7 +224,7 @@ | SOME th => (thy,th)) else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")") | NONE => - (case P.get_thm thyname' thmname thy of + (case ProofKernel.get_thm thyname' thmname thy of (thy',SOME res) => (thy',res) | (thy',NONE) => if thyname' = thyname @@ -242,31 +240,31 @@ PTmSpec _ => (thy',th) | PTyDef _ => (thy',th) | PTyIntro _ => (thy',th) - | _ => P.store_thm thyname' thmname th thy' + | _ => ProofKernel.store_thm thyname' thmname th thy' end else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")"))) | NONE => raise ERR "rp'.PDisk" "Not enough information") | PAxm(name,c) => - (case P.get_axiom thyname name thy of + (case ProofKernel.get_axiom thyname name thy of (thy',SOME res) => (thy',res) - | (thy',NONE) => P.new_axiom name c thy') + | (thy',NONE) => ProofKernel.new_axiom name c thy') | PTmSpec(seg,names,prf') => let val (thy',th) = rp' prf' thy in - P.new_specification seg thmname names th thy' + ProofKernel.new_specification seg thmname names th thy' end | PTyDef(seg,name,prf') => let val (thy',th) = rp' prf' thy in - P.new_type_definition seg thmname name th thy' + ProofKernel.new_type_definition seg thmname name th thy' end | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') => let val (thy',th) = rp' prf' thy in - P.type_introduction seg thmname name abs_name rep_name (P,t) th thy' + ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy' end | _ => rp pc thy end @@ -282,7 +280,7 @@ fun setup_int_thms thyname thy = let val fname = - case P.get_proof_dir thyname thy of + case ProofKernel.get_proof_dir thyname thy of SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}} | NONE => error "Cannot find proof files" val is = TextIO.openIn fname @@ -291,7 +289,7 @@ fun get_facts facts = case TextIO.inputLine is of NONE => (case facts of - i::facts => (the (Int.fromString i),map P.protect_factname (rev facts)) + i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts)) | _ => raise ERR "replay_thm" "Bad facts.lst file") | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts) in @@ -349,9 +347,9 @@ | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = add_hol4_type_mapping thyname tycname true fulltyname thy | delta (Indexed_theorem (i, th)) thy = - (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy) - | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy) - | delta (Dump s) thy = P.replay_add_dump s thy + (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy) + | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy) + | delta (Dump s) thy = ProofKernel.replay_add_dump s thy in rps end diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 18:45:14 2010 +0100 @@ -1004,7 +1004,6 @@ (* syntax und parsing *) -structure P = Parse and K = Keyword; val _ = Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/SMT.thy --- a/src/HOL/SMT.thy Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/SMT.thy Wed Dec 15 18:45:14 2010 +0100 @@ -11,7 +11,7 @@ "Tools/SMT/smt_utils.ML" "Tools/SMT/smt_failure.ML" "Tools/SMT/smt_config.ML" - "Tools/SMT/smt_monomorph.ML" + ("Tools/SMT/smt_monomorph.ML") ("Tools/SMT/smt_builtin.ML") ("Tools/SMT/smt_normalize.ML") ("Tools/SMT/smt_translate.ML") @@ -149,6 +149,7 @@ subsection {* Setup *} +use "Tools/SMT/smt_monomorph.ML" use "Tools/SMT/smt_builtin.ML" use "Tools/SMT/smt_normalize.ML" use "Tools/SMT/smt_translate.ML" diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 18:45:14 2010 +0100 @@ -45,8 +45,19 @@ fun is_const pred (n, T) = not (ignored n) andalso pred T fun collect_consts_if pred f = - Thm.prop_of #> - Term.fold_aterms (fn Const c => if is_const pred c then f c else I | _ => I) + let + fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t + | collect (t $ u) = collect t #> collect u + | collect (Abs (_, _, t)) = collect t + | collect (Const c) = if is_const pred c then f c else I + | collect _ = I + and collect_trigger t = + let val dest = these o try HOLogic.dest_list + in fold (fold collect_pat o dest) (dest t) end + and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t + | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t + | collect_pat _ = I + in collect o Thm.prop_of end val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 18:45:14 2010 +0100 @@ -141,7 +141,7 @@ "must have the same kind: " ^ Syntax.string_of_term ctxt t) fun check_trigger_conv ctxt ct = - if proper_quant false proper_trigger (Thm.term_of ct) then Conv.all_conv ct + if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct else check_trigger_error ctxt (Thm.term_of ct) @@ -183,7 +183,7 @@ (case pairself (minimal_pats vs) (Thm.dest_comb ct) of ([], []) => [[ct]] | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') - | _ => [[ct]]) + | _ => []) else [] fun proper_mpat _ _ _ [] = false @@ -227,8 +227,11 @@ in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end + fun has_trigger (@{const SMT.trigger} $ _ $ _) = true + | has_trigger _ = false + fun try_trigger_conv cv ct = - if proper_quant false (K false) (Thm.term_of ct) then Conv.all_conv ct + if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct else Conv.try_conv cv ct fun infer_trigger_conv ctxt = @@ -256,20 +259,20 @@ fun is_weight (@{const SMT.weight} $ w $ t) = (case try HOLogic.dest_number w of - SOME (_, i) => i > 0 andalso has_no_weight t + SOME (_, i) => i >= 0 andalso has_no_weight t | _ => false) | is_weight t = has_no_weight t fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t - | proper_trigger t = has_no_weight t + | proper_trigger t = is_weight t fun check_weight_error ctxt t = - error ("SMT weight must be a positive number and must only occur " ^ + error ("SMT weight must be a non-negative number and must only occur " ^ "under the top-most quantifier and an optional trigger: " ^ Syntax.string_of_term ctxt t) fun check_weight_conv ctxt ct = - if U.under_quant proper_trigger (Thm.term_of ct) then Conv.all_conv ct + if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct else check_weight_error ctxt (Thm.term_of ct) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 18:45:14 2010 +0100 @@ -147,6 +147,8 @@ fun mark t = (case Term.strip_comb t of (u as Const (@{const_name If}, _), ts) => marks u ts + | (u as @{const SMT.weight}, [t1, t2]) => + mark t2 #>> (fn t2' => u $ t1 $ t2') | (u as Const c, ts) => (case B.builtin_num ctxt t of SOME (n, T) => @@ -378,9 +380,7 @@ | replace @{const True} = term_true | replace @{const False} = term_false | replace t = t - in - Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool)) - end + in Term.map_aterms replace (U.prop_of term_bool) end val fol_rules = [ Let_def, @@ -496,14 +496,7 @@ | group_quant _ Ts t = (Ts, t) fun dest_weight (@{const SMT.weight} $ w $ t) = - ((SOME (snd (HOLogic.dest_number w)), t) - handle TERM _ => - (case w of - Var ((s, _), _) => (* FIXME: temporary workaround *) - (case Int.fromString s of - SOME n => (SOME n, t) - | NONE => raise TERM ("bad weight", [w])) - | _ => raise TERM ("bad weight", [w]))) + (SOME (snd (HOLogic.dest_number w)), t) | dest_weight t = (NONE, t) fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) @@ -609,8 +602,7 @@ val (builtins, ts1) = ithms - |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd) - |> map (Envir.eta_contract o Envir.beta_norm) + |> map (Envir.beta_eta_contract o U.prop_of o snd) |> mark_builtins ctxt val ((dtyps, tr_context, ctxt1), ts2) = diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 18:45:14 2010 +0100 @@ -47,6 +47,8 @@ val mk_cprop: cterm -> cterm val dest_cprop: cterm -> cterm val mk_cequals: cterm -> cterm -> cterm + val term_of: cterm -> term + val prop_of: thm -> term (*conversions*) val if_conv: (term -> bool) -> conv -> conv -> conv @@ -177,6 +179,10 @@ val equals = mk_const_pat @{theory} @{const_name "=="} destT1 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu +val dest_prop = (fn @{const Trueprop} $ t => t | t => t) +fun term_of ct = dest_prop (Thm.term_of ct) +fun prop_of thm = dest_prop (Thm.prop_of thm) + (* conversions *) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/z3_proof_literals.ML --- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 18:45:14 2010 +0100 @@ -33,6 +33,7 @@ structure Z3_Proof_Literals: Z3_PROOF_LITERALS = struct +structure U = SMT_Utils structure T = Z3_Proof_Tools @@ -41,10 +42,10 @@ type littab = thm Termtab.table -fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty +fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty -fun insert_lit thm = Termtab.update (`T.prop_of thm) -fun delete_lit thm = Termtab.delete (T.prop_of thm) +fun insert_lit thm = Termtab.update (`U.prop_of thm) +fun delete_lit thm = Termtab.delete (U.prop_of thm) fun lookup_lit lits = Termtab.lookup lits fun get_first_lit f = Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE) @@ -161,9 +162,9 @@ val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty fun explode1 thm = - if Termtab.defined tab (T.prop_of thm) then cons thm + if Termtab.defined tab (U.prop_of thm) then cons thm else - (case dest_rules (T.prop_of thm) of + (case dest_rules (U.prop_of thm) of SOME (rule1, rule2) => explode2 rule1 thm #> explode2 rule2 thm #> @@ -171,12 +172,12 @@ | NONE => cons thm) and explode2 dest_rule thm = - if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm) + if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm) then explode1 (T.compose dest_rule thm) else cons (T.compose dest_rule thm) fun explode0 thm = - if not is_conj andalso is_dneg (T.prop_of thm) + if not is_conj andalso is_dneg (U.prop_of thm) then [T.compose dneg_rule thm] else explode1 thm [] @@ -284,7 +285,7 @@ val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)} fun contra_left conj thm = let - val rules = explode_term conj (T.prop_of thm) + val rules = explode_term conj (U.prop_of thm) fun contra_lits (t, rs) = (case t of @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 18:45:14 2010 +0100 @@ -15,6 +15,7 @@ structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = struct +structure U = SMT_Utils structure P = Z3_Proof_Parser structure T = Z3_Proof_Tools structure L = Z3_Proof_Literals @@ -233,9 +234,9 @@ fun lit_elim conj (p, idx) ct ptab = let val lits = literals_of p in - (case L.lookup_lit lits (T.term_of ct) of + (case L.lookup_lit lits (U.term_of ct) of SOME lit => (Thm lit, ptab) - | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab)) + | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab)) end in val and_elim = lit_elim true @@ -266,7 +267,7 @@ val explode_disj = L.explode false true false val join_disj = L.join false fun unit thm thms th = - let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms + let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms in join_disj (L.make_littab (thms @ explode_disj ts th)) t end fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) @@ -403,7 +404,7 @@ named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] in fun nnf ctxt vars ps ct = - (case T.term_of ct of + (case U.term_of ct of _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => if l aconv r then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 18:45:14 2010 +0100 @@ -6,9 +6,7 @@ signature Z3_PROOF_TOOLS = sig - (*accessing and modifying terms*) - val term_of: cterm -> term - val prop_of: thm -> term + (*modifying terms*) val as_meta_eq: cterm -> cterm (*theorem nets*) @@ -51,12 +49,7 @@ -(* accessing terms *) - -val dest_prop = (fn @{const Trueprop} $ t => t | t => t) - -fun term_of ct = dest_prop (Thm.term_of ct) -fun prop_of thm = dest_prop (Thm.prop_of thm) +(* modifying terms *) fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct)) diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 18:45:14 2010 +0100 @@ -458,7 +458,7 @@ val smt_iter_min_msecs = Unsynchronized.ref 5000 val smt_monomorph_limit = Unsynchronized.ref 4 -fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i = +fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = let val ctxt = Proof.context_of state fun iter timeout iter_num outcome0 time_so_far facts = @@ -482,6 +482,11 @@ else () val birth = Timer.checkRealTimer timer + val _ = + if debug then + Output.urgent_message "Invoking SMT solver..." + else + () val {outcome, used_facts, ...} = SMT_Solver.smt_filter remote iter_timeout state facts i val death = Timer.checkRealTimer timer @@ -489,6 +494,8 @@ if verbose andalso is_some outcome then "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) |> Output.urgent_message + else if debug then + Output.urgent_message "SMT solver returned." else () val outcome0 = if is_none outcome0 then SOME outcome else outcome0 diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 15 18:45:14 2010 +0100 @@ -180,9 +180,11 @@ | (false, _) => run_prover problem prover) provers (false, state) else - provers |> (if blocking then Par_List.map else map) - (run_prover problem) - |> exists fst |> rpair state + provers + |> (if blocking andalso length provers > 1 then Par_List.map + else map) + (run_prover problem) + |> exists fst |> rpair state end val run_atps = run_provers "ATP" no_dangerous_types atp_relevance_fudge diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/TFL/dcterm.ML --- a/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 18:45:14 2010 +0100 @@ -49,9 +49,7 @@ structure Dcterm: DCTERM = struct -structure U = Utils; - -fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg}; +fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg}; fun dest_comb t = Thm.dest_comb t @@ -110,19 +108,19 @@ fun dest_monop expected tm = let fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); - val (c, N) = dest_comb tm handle U.ERR _ => err (); - val name = #Name (dest_const c handle U.ERR _ => err ()); + val (c, N) = dest_comb tm handle Utils.ERR _ => err (); + val name = #Name (dest_const c handle Utils.ERR _ => err ()); in if name = expected then N else err () end; fun dest_binop expected tm = let fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); - val (M, N) = dest_comb tm handle U.ERR _ => err () - in (dest_monop expected M, N) handle U.ERR _ => err () end; + val (M, N) = dest_comb tm handle Utils.ERR _ => err () + in (dest_monop expected M, N) handle Utils.ERR _ => err () end; fun dest_binder expected tm = dest_abs NONE (dest_monop expected tm) - handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); + handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); val dest_neg = dest_monop @{const_name Not} @@ -151,7 +149,7 @@ (*--------------------------------------------------------------------------- * Iterated creation. *---------------------------------------------------------------------------*) -val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); +val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); (*--------------------------------------------------------------------------- * Iterated destruction. (To the "right" in a term.) @@ -160,7 +158,7 @@ let fun dest (p as (ctm,accum)) = let val (M,N) = break ctm in dest (N, M::accum) - end handle U.ERR _ => p + end handle Utils.ERR _ => p in dest (tm,[]) end; @@ -190,7 +188,7 @@ handle TYPE (msg, _, _) => raise ERR "mk_prop" msg | TERM (msg, _) => raise ERR "mk_prop" msg; -fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm; +fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm; end; diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/TFL/post.ML Wed Dec 15 18:45:14 2010 +0100 @@ -18,8 +18,6 @@ structure Tfl: TFL = struct -structure S = USyntax - (* misc *) (*--------------------------------------------------------------------------- @@ -53,16 +51,14 @@ * processing from the definition stage. *---------------------------------------------------------------------------*) local -structure R = Rules -structure U = Utils (* The rest of these local definitions are for the tricky nested case *) -val solved = not o can S.dest_eq o #2 o S.strip_forall o concl +val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl fun id_thm th = - let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); + let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th)))); in lhs aconv rhs end - handle U.ERR _ => false; + handle Utils.ERR _ => false; val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; fun mk_meta_eq r = case concl_of r of @@ -76,16 +72,16 @@ fun join_assums th = let val thy = Thm.theory_of_thm th val tych = cterm_of thy - val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) - val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) - val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) + val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th))) + val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *) + val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) val cntxt = union (op aconv) cntxtl cntxtr in - R.GEN_ALL - (R.DISCH_ALL - (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) + Rules.GEN_ALL + (Rules.DISCH_ALL + (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) end - val gen_all = S.gen_all + val gen_all = USyntax.gen_all in fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = let @@ -117,7 +113,7 @@ in {induction = induction', rules = rules', - tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) + tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl) (simplified@stubborn)} end end; @@ -144,8 +140,8 @@ val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq val {rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) - val {lhs=f,rhs} = S.dest_eq (concl def) - val (_,[R,_]) = S.strip_comb rhs + val {lhs=f,rhs} = USyntax.dest_eq (concl def) + val (_,[R,_]) = USyntax.strip_comb rhs val dummy = Prim.trace_thms "congs =" congs (*the next step has caused simplifier looping in some cases*) val {induction, rules, tcs} = @@ -154,12 +150,12 @@ full_pats_TCs = full_pats_TCs, TCs = TCs} val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) - (R.CONJUNCTS rules) + (Rules.CONJUNCTS rules) in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')), rules = ListPair.zip(rules', rows), tcs = (termination_goals rules') @ tcs} end - handle U.ERR {mesg,func,module} => + handle Utils.ERR {mesg,func,module} => error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); @@ -217,7 +213,7 @@ fun define strict thy cs ss congs wfs fid R seqs = define_i strict thy cs ss congs wfs fid (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) - handle U.ERR {mesg,...} => error mesg; + handle Utils.ERR {mesg,...} => error mesg; (*--------------------------------------------------------------------------- @@ -227,11 +223,11 @@ *---------------------------------------------------------------------------*) fun func_of_cond_eqn tm = - #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm))))))); + #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm))))))); fun defer_i thy congs fid eqs = let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs - val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); + val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules)); val dummy = writeln "Proving induction theorem ..."; val induction = Prim.mk_induction theory {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} @@ -243,7 +239,7 @@ fun defer thy congs fid seqs = defer_i thy congs fid (map (Syntax.read_term_global thy) seqs) - handle U.ERR {mesg,...} => error mesg; + handle Utils.ERR {mesg,...} => error mesg; end; end; diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Wed Dec 15 18:45:14 2010 +0100 @@ -57,16 +57,11 @@ structure Rules: RULES = struct -structure S = USyntax; -structure U = Utils; -structure D = Dcterm; +fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg}; -fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg}; - - -fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm)); -fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm)); +fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm)); +fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm)); fun dest_thm thm = let val {prop,hyps,...} = Thm.rep_thm thm @@ -95,7 +90,7 @@ handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg; fun rbeta th = - (case D.strip_comb (cconcl th) of + (case Dcterm.strip_comb (cconcl th) of (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r) | _ => raise RULES_ERR "rbeta" ""); @@ -108,7 +103,7 @@ * "B" results in something that looks like "A --> B". *---------------------------------------------------------------------------*) -fun ASSUME ctm = Thm.assume (D.mk_prop ctm); +fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm); (*--------------------------------------------------------------------------- @@ -119,7 +114,7 @@ handle THM (msg, _, _) => raise RULES_ERR "MP" msg; (*forces the first argument to be a proposition if necessary*) -fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI +fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg; fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; @@ -131,9 +126,9 @@ end; fun UNDISCH thm = - let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm))) + let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm))) in Thm.implies_elim (thm RS mp) (ASSUME tm) end - handle U.ERR _ => raise RULES_ERR "UNDISCH" "" + handle Utils.ERR _ => raise RULES_ERR "UNDISCH" "" | THM _ => raise RULES_ERR "UNDISCH" ""; fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; @@ -152,7 +147,7 @@ fun CONJUNCT2 thm = thm RS conjunct2 handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg; -fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th]; +fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th]; fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list" | LIST_CONJ [th] = th @@ -168,7 +163,7 @@ val [P,Q] = OldTerm.term_vars prop val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1 in -fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1) +fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1) handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; end; @@ -177,7 +172,7 @@ val [P,Q] = OldTerm.term_vars prop val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2 in -fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2) +fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2) handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; end; @@ -195,10 +190,10 @@ let fun blue ldisjs [] _ = [] | blue ldisjs (th::rst) rdisjs = let val tail = tl rdisjs - val rdisj_tl = D.list_mk_disj tail + val rdisj_tl = Dcterm.list_mk_disj tail in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl) :: blue (ldisjs @ [cconcl th]) rst tail - end handle U.ERR _ => [fold_rev DISJ2 ldisjs th] + end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th] in blue [] thms (map cconcl thms) end; @@ -212,8 +207,8 @@ fun DISJ_CASES th1 th2 th3 = let - val c = D.drop_prop (cconcl th1); - val (disj1, disj2) = D.dest_disj c; + val c = Dcterm.drop_prop (cconcl th1); + val (disj1, disj2) = Dcterm.dest_disj c; val th2' = DISCH disj1 th2; val th3' = DISCH disj2 th3; in @@ -253,12 +248,12 @@ fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (#hyps(rep_thm th)) - val tml = D.strip_disj c + val tml = Dcterm.strip_disj c fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases" | DL th [th1] = PROVE_HYP th th1 | DL th [th1,th2] = DISJ_CASES th th1 th2 | DL th (th1::rst) = - let val tm = #2(D.dest_disj(D.drop_prop(cconcl th))) + let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th))) in DISJ_CASES th th1 (DL (ASSUME tm) rst) end in DL disjth (organize eq tml thl) end; @@ -279,7 +274,7 @@ in thm RS (Thm.forall_elim tm gspec') end end; -fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm; +fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm; val ISPEC = SPEC val ISPECL = fold ISPEC; @@ -323,7 +318,7 @@ fun MATCH_MP th1 th2 = - if (D.is_forall (D.drop_prop(cconcl th1))) + if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1))) then MATCH_MP (th1 RS spec) th2 else MP th1 th2; @@ -345,8 +340,8 @@ fun CHOOSE (fvar, exth) fact = let - val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) - val redex = D.capply lam fvar + val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth))) + val redex = Dcterm.capply lam fvar val thy = Thm.theory_of_cterm redex val t$u = Thm.term_of redex val residue = Thm.cterm_of thy (Term.betapply (t, u)) @@ -364,7 +359,7 @@ val prop = Thm.prop_of thm val P' = cterm_of thy P val x' = cterm_of thy x - val abstr = #2 (D.dest_comb template) + val abstr = #2 (Dcterm.dest_comb template) in thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg @@ -380,7 +375,7 @@ *---------------------------------------------------------------------------*) fun EXISTL vlist th = - fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm) + fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm) vlist th; @@ -397,7 +392,7 @@ let val thy = Thm.theory_of_thm th val tych = cterm_of thy val blist' = map (pairself Thm.term_of) blist - fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M}) + fun ex v M = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M}) in fold_rev (fn (b as (r1,r2)) => fn thm => @@ -443,7 +438,7 @@ (* Object language quantifier, i.e., "!" *) -fun Forall v M = S.mk_forall{Bvar=v, Body=M}; +fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M}; (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) @@ -458,11 +453,11 @@ (Const (@{const_name Trueprop},_) $ lhs) $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs} | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} - | dest_equal tm = S.dest_eq tm; + | dest_equal tm = USyntax.dest_eq tm; fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); -fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a +fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; val is_all = can (dest_all []); @@ -505,13 +500,13 @@ of ([],_) => get (rst, n+1,L) | (vlist,body) => let val eq = Logic.strip_imp_concl body - val (f,args) = S.strip_comb (get_lhs eq) - val (vstrl,_) = S.strip_abs f + val (f,args) = USyntax.strip_comb (get_lhs eq) + val (vstrl,_) = USyntax.strip_abs f val names = Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl) in get (rst, n+1, (names,n)::L) end handle TERM _ => get (rst, n+1, L) - | U.ERR _ => get (rst, n+1, L); + | Utils.ERR _ => get (rst, n+1, L); (* Note: Thm.rename_params_rule counts from 1, not 0 *) fun rename thm = @@ -529,7 +524,7 @@ *---------------------------------------------------------------------------*) fun list_beta_conv tm = - let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th)))) + let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th)))) fun iter [] = Thm.reflexive tm | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v)) in iter end; @@ -553,28 +548,28 @@ * General abstraction handlers, should probably go in USyntax. *---------------------------------------------------------------------------*) fun mk_aabs (vstr, body) = - S.mk_abs {Bvar = vstr, Body = body} - handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body}; + USyntax.mk_abs {Bvar = vstr, Body = body} + handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body}; fun list_mk_aabs (vstrl,tm) = fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; fun dest_aabs used tm = - let val ({Bvar,Body}, used') = S.dest_abs used tm + let val ({Bvar,Body}, used') = USyntax.dest_abs used tm in (Bvar, Body, used') end - handle U.ERR _ => - let val {varstruct, body, used} = S.dest_pabs used tm + handle Utils.ERR _ => + let val {varstruct, body, used} = USyntax.dest_pabs used tm in (varstruct, body, used) end; fun strip_aabs used tm = let val (vstr, body, used') = dest_aabs used tm val (bvs, core, used'') = strip_aabs used' body in (vstr::bvs, core, used'') end - handle U.ERR _ => ([], tm, used); + handle Utils.ERR _ => ([], tm, used); fun dest_combn tm 0 = (tm,[]) | dest_combn tm n = - let val {Rator,Rand} = S.dest_comb tm + let val {Rator,Rand} = USyntax.dest_comb tm val (f,rands) = dest_combn Rator (n-1) in (f,Rand::rands) end; @@ -582,7 +577,7 @@ -local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end +local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end fun mk_fst tm = let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm in Const ("Product_Type.fst", ty --> fty) $ tm end @@ -610,7 +605,7 @@ *---------------------------------------------------------------------------*) fun VSTRUCT_ELIM tych a vstr th = - let val L = S.free_vars_lr vstr + let val L = USyntax.free_vars_lr vstr val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th) val thm2 = forall_intr_list (map tych L) thm1 @@ -641,7 +636,7 @@ in (strip_aabs used f,args) end; -fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M; +fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M; fun dest_impl tm = let val ants = Logic.strip_imp_prems tm @@ -649,7 +644,7 @@ in (ants,get_lhs eq) end; -fun restricted t = is_some (S.find_term +fun restricted t = is_some (USyntax.find_term (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false) t) @@ -675,7 +670,7 @@ val lhs = tych(get_lhs eq) val ss' = Simplifier.add_prems (map ASSUME ants) ss val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs - handle U.ERR _ => Thm.reflexive lhs + handle Utils.ERR _ => Thm.reflexive lhs val dummy = print_thms "proven:" [lhs_eq_lhs1] val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq @@ -693,10 +688,10 @@ val eq1 = Logic.strip_imp_concl imp_body1 val Q = get_lhs eq1 val QeqQ1 = pbeta_reduce (tych Q) - val Q1 = #2(D.dest_eq(cconcl QeqQ1)) + val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1)) val ss' = Simplifier.add_prems (map ASSUME ants1) ss val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1 - handle U.ERR _ => Thm.reflexive Q1 + handle Utils.ERR _ => Thm.reflexive Q1 val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection) @@ -708,7 +703,7 @@ val impth = implies_intr_list ants1 QeeqQ3 val impth1 = impth RS meta_eq_to_obj_eq (* Need to abstract *) - val ant_th = U.itlist2 (PGEN tych) args vstrl impth1 + val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1 in ant_th COMP thm end fun q_eliminate (thm,imp,thy) = @@ -722,7 +717,7 @@ val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' (tych Q) - handle U.ERR _ => Thm.reflexive (tych Q) + handle Utils.ERR _ => Thm.reflexive (tych Q) val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 @@ -740,7 +735,7 @@ (* Assume that the leading constant is ==, *) | _ => thm (* if it is not a ==> *) in SOME(eliminate (rename thm)) end - handle U.ERR _ => NONE (* FIXME handle THM as well?? *) + handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) fun restrict_prover ss thm = let val dummy = say "restrict_prover:" @@ -765,12 +760,12 @@ val rcontext = rev cntxt val cncl = HOLogic.dest_Trueprop o Thm.prop_of val antl = case rcontext of [] => [] - | _ => [S.list_mk_conj(map cncl rcontext)] - val TC = genl(S.list_mk_imp(antl, A)) + | _ => [USyntax.list_mk_conj(map cncl rcontext)] + val TC = genl(USyntax.list_mk_imp(antl, A)) val dummy = print_cterm "func:" (cterm_of thy func) val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC)) val dummy = tc_list := (TC :: !tc_list) - val nestedp = is_some (S.find_term is_func TC) + val nestedp = is_some (USyntax.find_term is_func TC) val dummy = if nestedp then say "nested" else say "not_nested" val th' = if nestedp then raise RULES_ERR "solver" "nested function" else let val cTC = cterm_of thy @@ -782,7 +777,7 @@ end val th'' = th' RS thm in SOME (th'') - end handle U.ERR _ => NONE (* FIXME handle THM as well?? *) + end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) in (if (is_cong thm) then cong_prover else restrict_prover) ss thm end diff -r f4d3acf0c4cc -r 5391d34b0f4c src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 18:45:14 2010 +0100 @@ -42,17 +42,13 @@ val trace = Unsynchronized.ref false; -structure R = Rules; -structure S = USyntax; -structure U = Utils; +fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg}; -fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg}; +val concl = #2 o Rules.dest_thm; +val hyp = #1 o Rules.dest_thm; -val concl = #2 o R.dest_thm; -val hyp = #1 o R.dest_thm; - -val list_mk_type = U.end_itlist (curry (op -->)); +val list_mk_type = Utils.end_itlist (curry (op -->)); fun front_last [] = raise TFL_ERR "front_last" "empty list" | front_last [x] = ([],x) @@ -99,12 +95,12 @@ val (in_group, not_in_group) = fold_rev (fn (row as (p::rst, rhs)) => fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p + let val (pc,args) = USyntax.strip_comb p in if (#1(dest_Const pc) = c) then ((args@rst, rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]) - val col_types = U.take type_of (length L, #1(hd in_group)) + val col_types = Utils.take type_of (length L, #1(hd in_group)) in part{constrs = crst, rows = not_in_group, A = {constructor = c, @@ -142,8 +138,8 @@ val L = binder_types Ty and ty = body_type Ty val ty_theta = ty_match ty colty - val c' = S.inst ty_theta c - val gvars = map (S.inst ty_theta o gv) L + val c' = USyntax.inst ty_theta c + val gvars = map (USyntax.inst ty_theta o gv) L in (c', gvars) end; @@ -155,7 +151,7 @@ fun mk_group name rows = fold_rev (fn (row as ((prfx, p::rst), rhs)) => fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p + let val (pc,args) = USyntax.strip_comb p in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false) then (((prfx,args@rst), rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) @@ -174,7 +170,7 @@ val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows val in_group' = if (null in_group) (* Constructor not given *) - then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))] + then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))] else in_group in part{constrs = crst, @@ -264,7 +260,7 @@ (ListPair.zip (new_formals, groups)) val rec_calls = map mk news val (pat_rect,dtrees) = ListPair.unzip rec_calls - val case_functions = map S.list_mk_abs + val case_functions = map USyntax.list_mk_abs (ListPair.zip (new_formals, dtrees)) val types = map type_of (case_functions@[u]) @ [range_ty] val case_const' = Const(case_const_name, list_mk_type types) @@ -279,11 +275,11 @@ (* Repeated variable occurrences in a pattern are not allowed. *) fun FV_multiset tm = - case (S.dest_term tm) - of S.VAR{Name = c, Ty = T} => [Free(c, T)] - | S.CONST _ => [] - | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand - | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda"; + case (USyntax.dest_term tm) + of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)] + | USyntax.CONST _ => [] + | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand + | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda"; fun no_repeat_vars thy pat = let fun check [] = true @@ -370,10 +366,10 @@ | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort); local val f_eq_wfrec_R_M = - #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY)))) - val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M + #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY)))) + val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M val (fname,_) = dest_Free f - val (wfrec,_) = S.strip_comb rhs + val (wfrec,_) = USyntax.strip_comb rhs in fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) = let val def_name = Long_Name.base_name fid ^ "_def" @@ -422,15 +418,15 @@ fun post_definition meta_tflCongs (theory, (def, pats)) = let val tych = Thry.typecheck theory - val f = #lhs(S.dest_eq(concl def)) - val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def + val f = #lhs(USyntax.dest_eq(concl def)) + val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def val pats' = filter given pats val given_pats = map pat_of pats' val rows = map row_of_pat pats' - val WFR = #ant(S.dest_imp(concl corollary)) - val R = #Rand(S.dest_comb WFR) - val corollary' = R.UNDISCH corollary (* put WF R on assums *) - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') + val WFR = #ant(USyntax.dest_imp(concl corollary)) + val R = #Rand(USyntax.dest_comb WFR) + val corollary' = Rules.UNDISCH corollary (* put WF R on assums *) + val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats val (case_rewrites,context_congs) = extraction_thms theory (*case_ss causes minimal simplification: bodies of case expressions are @@ -440,12 +436,12 @@ (HOL_basic_ss addcongs (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites) val corollaries' = map (Simplifier.simplify case_ss) corollaries - val extract = R.CONTEXT_REWRITE_RULE + val extract = Rules.CONTEXT_REWRITE_RULE (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs) val (rules, TCs) = ListPair.unzip (map extract corollaries') val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules - val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) - val rules1 = R.LIST_CONJ(map mk_cond_rule rules0) + val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR) + val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0) in {rules = rules1, rows = rows, @@ -463,8 +459,8 @@ *---------------------------------------------------------------------------*) fun wfrec_eqns thy fid tflCongs eqns = - let val {lhs,rhs} = S.dest_eq (hd eqns) - val (f,args) = S.strip_comb lhs + let val {lhs,rhs} = USyntax.dest_eq (hd eqns) + val (f,args) = USyntax.strip_comb lhs val (fname,fty) = dest_atom f val (SV,a) = front_last args (* SV = schematic variables *) val g = list_comb(f,SV) @@ -482,22 +478,22 @@ else () val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy - val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY + val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname, Rtype) - val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0 - val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) + val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0 + val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM) val dummy = if !trace then writeln ("ORIGINAL PROTO_DEF: " ^ Syntax.string_of_term_global thy proto_def) else () - val R1 = S.rand WFR - val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM) - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats + val R1 = USyntax.rand WFR + val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM) + val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats val corollaries' = map (rewrite_rule case_rewrites) corollaries - fun extract X = R.CONTEXT_REWRITE_RULE + fun extract X = Rules.CONTEXT_REWRITE_RULE (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X in {proto_def = proto_def, SV=SV, @@ -517,8 +513,8 @@ fun lazyR_def thy fid tflCongs eqns = let val {proto_def,WFR,pats,extracta,SV} = wfrec_eqns thy fid tflCongs eqns - val R1 = S.rand WFR - val f = #lhs(S.dest_eq proto_def) + val R1 = USyntax.rand WFR + val f = #lhs(USyntax.dest_eq proto_def) val (extractants,TCl) = ListPair.unzip extracta val dummy = if !trace then writeln (cat_lines ("Extractants =" :: @@ -526,17 +522,17 @@ else () val TCs = fold_rev (union (op aconv)) TCl [] val full_rqt = WFR::TCs - val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} - val R'abs = S.rand R' + val R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt} + val R'abs = USyntax.rand R' val proto_def' = subst_free[(R1,R')] proto_def val dummy = if !trace then writeln ("proto_def' = " ^ Syntax.string_of_term_global thy proto_def') else () - val {lhs,rhs} = S.dest_eq proto_def' - val (c,args) = S.strip_comb lhs + val {lhs,rhs} = USyntax.dest_eq proto_def' + val (c,args) = USyntax.strip_comb lhs val (name,Ty) = dest_atom c - val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs)) + val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs)) val ([def0], theory) = thy |> Global_Theory.add_defs false @@ -545,31 +541,31 @@ val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def) else () - (* val fconst = #lhs(S.dest_eq(concl def)) *) + (* val fconst = #lhs(USyntax.dest_eq(concl def)) *) val tych = Thry.typecheck theory val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt (*lcp: a lot of object-logic inference to remove*) - val baz = R.DISCH_ALL - (fold_rev R.DISCH full_rqt_prop - (R.LIST_CONJ extractants)) + val baz = Rules.DISCH_ALL + (fold_rev Rules.DISCH full_rqt_prop + (Rules.LIST_CONJ extractants)) val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz) else () val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) val SV' = map tych SV; val SVrefls = map Thm.reflexive SV' - val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x)) + val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x)) SVrefls def) RS meta_eq_to_obj_eq - val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 - val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) + val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0 + val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop) val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon theory Hilbert_Choice*) ML_Context.thm "Hilbert_Choice.tfl_some" handle ERROR msg => cat_error msg "defer_recdef requires theory Main or at least Hilbert_Choice as parent" - val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th + val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th in {theory = theory, R=R1, SV=SV, - rules = fold (U.C R.MP) (R.CONJUNCTS bar) def', + rules = fold (Utils.C Rules.MP) (Rules.CONJUNCTS bar) def', full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), patterns = pats} end; @@ -603,8 +599,8 @@ *---------------------------------------------------------------------------*) fun alpha_ex_unroll (xlist, tm) = - let val (qvars,body) = S.strip_exists tm - val vlist = #2(S.strip_comb (S.rhs body)) + let val (qvars,body) = USyntax.strip_exists tm + val vlist = #2 (USyntax.strip_comb (USyntax.rhs body)) val plist = ListPair.zip (vlist, xlist) val args = map (the o AList.lookup (op aconv) plist) qvars handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence" @@ -634,7 +630,7 @@ fun fail s = raise TFL_ERR "mk_case" s fun mk{rows=[],...} = fail"no rows" | mk{path=[], rows = [([], (thm, bindings))]} = - R.IT_EXISTS (map tych_binding bindings) thm + Rules.IT_EXISTS (map tych_binding bindings) thm | mk{path = u::rstp, rows as (p::_, _)::_} = let val (pat_rectangle,rights) = ListPair.unzip rows val col0 = map hd pat_rectangle @@ -651,8 +647,8 @@ case (ty_info ty_name) of NONE => fail("Not a known datatype: "^ty_name) | SOME{constructors,nchotomy} => - let val thm' = R.ISPEC (tych u) nchotomy - val disjuncts = S.strip_disj (concl thm') + let val thm' = Rules.ISPEC (tych u) nchotomy + val disjuncts = USyntax.strip_disj (concl thm') val subproblems = divide(constructors, rows) val groups = map #group subproblems and new_formals = map #new_formals subproblems @@ -660,17 +656,17 @@ (new_formals, disjuncts) val constraints = map #1 existentials val vexl = map #2 existentials - fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b)) + fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b)) val news = map (fn (nf,rows,c) => {path = nf@rstp, rows = map (expnd c) rows}) - (U.zip3 new_formals groups constraints) + (Utils.zip3 new_formals groups constraints) val recursive_thms = map mk news val build_exists = Library.foldr (fn((x,t), th) => - R.CHOOSE (tych x, R.ASSUME (tych t)) th) + Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th) val thms' = ListPair.map build_exists (vexl, recursive_thms) - val same_concls = R.EVEN_ORS thms' - in R.DISJ_CASESL thm' same_concls + val same_concls = Rules.EVEN_ORS thms' + in Rules.DISJ_CASESL thm' same_concls end end end in mk @@ -688,14 +684,14 @@ val a = Free (aname, T) val v = Free (vname, T) val a_eq_v = HOLogic.mk_eq(a,v) - val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a) - (R.REFL (tych a)) - val th0 = R.ASSUME (tych a_eq_v) + val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a) + (Rules.REFL (tych a)) + val th0 = Rules.ASSUME (tych a_eq_v) val rows = map (fn x => ([x], (th0,[]))) pats in - R.GEN (tych a) - (R.RIGHT_ASSOC - (R.CHOOSE(tych v, ex_th0) + Rules.GEN (tych a) + (Rules.RIGHT_ASSOC + (Rules.CHOOSE(tych v, ex_th0) (mk_case ty_info (vname::aname::names) thy {path=[v], rows=rows}))) end end; @@ -712,57 +708,57 @@ *---------------------------------------------------------------------------*) (* local infix 5 ==> - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} + fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2} in fun build_ih f P (pat,TCs) = - let val globals = S.free_vars_lr pat - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) + let val globals = USyntax.free_vars_lr pat + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm) fun dest_TC tm = - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) - val (R,y,_) = S.dest_relation R_y_pat + let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm)) + val (R,y,_) = USyntax.dest_relation R_y_pat val P_y = if (nested tm) then R_y_pat ==> P$y else P$y in case cntxt of [] => (P_y, (tm,[])) | _ => let - val imp = S.list_mk_conj cntxt ==> P_y - val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs - in (S.list_mk_forall(locals,imp), (tm,locals)) end + val imp = USyntax.list_mk_conj cntxt ==> P_y + val lvs = gen_rems (op aconv) (USyntax.free_vars_lr imp, globals) + val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs + in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end end in case TCs - of [] => (S.list_mk_forall(globals, P$pat), []) + of [] => (USyntax.list_mk_forall(globals, P$pat), []) | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) - val ind_clause = S.list_mk_conj ihs ==> P$pat - in (S.list_mk_forall(globals,ind_clause), TCs_locals) + val ind_clause = USyntax.list_mk_conj ihs ==> P$pat + in (USyntax.list_mk_forall(globals,ind_clause), TCs_locals) end end end; *) local infix 5 ==> - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} + fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2} in fun build_ih f (P,SV) (pat,TCs) = - let val pat_vars = S.free_vars_lr pat + let val pat_vars = USyntax.free_vars_lr pat val globals = pat_vars@SV - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm) fun dest_TC tm = - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) - val (R,y,_) = S.dest_relation R_y_pat + let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm)) + val (R,y,_) = USyntax.dest_relation R_y_pat val P_y = if (nested tm) then R_y_pat ==> P$y else P$y in case cntxt of [] => (P_y, (tm,[])) | _ => let - val imp = S.list_mk_conj cntxt ==> P_y - val lvs = subtract (op aconv) globals (S.free_vars_lr imp) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs - in (S.list_mk_forall(locals,imp), (tm,locals)) end + val imp = USyntax.list_mk_conj cntxt ==> P_y + val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp) + val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs + in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end end in case TCs - of [] => (S.list_mk_forall(pat_vars, P$pat), []) + of [] => (USyntax.list_mk_forall(pat_vars, P$pat), []) | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) - val ind_clause = S.list_mk_conj ihs ==> P$pat - in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals) + val ind_clause = USyntax.list_mk_conj ihs ==> P$pat + in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals) end end end; @@ -776,29 +772,29 @@ *---------------------------------------------------------------------------*) fun prove_case f thy (tm,TCs_locals,thm) = let val tych = Thry.typecheck thy - val antc = tych(#ant(S.dest_imp tm)) - val thm' = R.SPEC_ALL thm - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) - fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) + val antc = tych(#ant(USyntax.dest_imp tm)) + val thm' = Rules.SPEC_ALL thm + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm) + fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC))))) fun mk_ih ((TC,locals),th2,nested) = - R.GENL (map tych locals) - (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2 - else if S.is_imp (concl TC) then R.IMP_TRANS TC th2 - else R.MP th2 TC) + Rules.GENL (map tych locals) + (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2 + else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2 + else Rules.MP th2 TC) in - R.DISCH antc - (if S.is_imp(concl thm') (* recursive calls in this clause *) - then let val th1 = R.ASSUME antc + Rules.DISCH antc + (if USyntax.is_imp(concl thm') (* recursive calls in this clause *) + then let val th1 = Rules.ASSUME antc val TCs = map #1 TCs_locals - val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o - #2 o S.strip_forall) TCs - val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs)) + val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o + #2 o USyntax.strip_forall) TCs + val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs)) TCs_locals - val th2list = map (U.C R.SPEC th1 o tych) ylist + val th2list = map (Utils.C Rules.SPEC th1 o tych) ylist val nlist = map nested TCs - val triples = U.zip3 TClist th2list nlist + val triples = Utils.zip3 TClist th2list nlist val Pylist = map mk_ih triples - in R.MP thm' (R.LIST_CONJ Pylist) end + in Rules.MP thm' (Rules.LIST_CONJ Pylist) end else thm') end; @@ -812,12 +808,12 @@ *---------------------------------------------------------------------------*) fun LEFT_ABS_VSTRUCT tych thm = let fun CHOOSER v (tm,thm) = - let val ex_tm = S.mk_exists{Bvar=v,Body=tm} - in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm) + let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm} + in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm) end - val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm)) - val {lhs,rhs} = S.dest_eq veq - val L = S.free_vars_lr rhs + val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm)) + val {lhs,rhs} = USyntax.dest_eq veq + val L = USyntax.free_vars_lr rhs in #2 (fold_rev CHOOSER L (veq,thm)) end; @@ -830,39 +826,39 @@ *---------------------------------------------------------------------------*) fun mk_induction thy {fconst, R, SV, pat_TCs_list} = let val tych = Thry.typecheck thy - val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM) + val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM) val (pats,TCsl) = ListPair.unzip pat_TCs_list val case_thm = complete_cases thy pats val domain = (type_of o hd) pats val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names) [] (pats::TCsl)) "P" val P = Free(Pname, domain --> HOLogic.boolT) - val Sinduct = R.SPEC (tych P) Sinduction - val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) + val Sinduct = Rules.SPEC (tych P) Sinduction + val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct) val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list val (Rassums,TCl') = ListPair.unzip Rassums_TCl' - val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums)) + val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums)) val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats - val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) + val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum) val proved_cases = map (prove_case fconst thy) tasks val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases)) "v", domain) val vtyped = tych v - val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats - val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') + val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats + val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th') (substs, proved_cases) val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1 - val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases) - val dc = R.MP Sinduct dant - val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc))) - val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty) - val dc' = fold_rev (R.GEN o tych) vars - (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc) + val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases) + val dc = Rules.MP Sinduct dant + val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc))) + val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty) + val dc' = fold_rev (Rules.GEN o tych) vars + (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc) in - R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') + Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc') end -handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation"; +handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation"; @@ -876,15 +872,15 @@ fun simplify_induction thy hth ind = let val tych = Thry.typecheck thy - val (asl,_) = R.dest_thm ind - val (_,tc_eq_tc') = R.dest_thm hth - val tc = S.lhs tc_eq_tc' + val (asl,_) = Rules.dest_thm ind + val (_,tc_eq_tc') = Rules.dest_thm hth + val tc = USyntax.lhs tc_eq_tc' fun loop [] = ind | loop (asm::rst) = if (can (Thry.match_term thy asm) tc) - then R.UNDISCH - (R.MATCH_MP - (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind)) + then Rules.UNDISCH + (Rules.MATCH_MP + (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind)) hth) else loop rst in loop asl @@ -896,7 +892,7 @@ * assumption to the theorem. *---------------------------------------------------------------------------*) fun elim_tc tcthm (rule,induction) = - (R.MP rule tcthm, R.PROVE_HYP tcthm induction) + (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction) fun trace_thms s L = @@ -911,17 +907,17 @@ fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} = let val tych = Thry.typecheck theory - val prove = R.prove strict; + val prove = Rules.prove strict; (*--------------------------------------------------------------------- * Attempt to eliminate WF condition. It's the only assumption of rules *---------------------------------------------------------------------*) val (rules1,induction1) = let val thm = prove(tych(HOLogic.mk_Trueprop - (hd(#1(R.dest_thm rules)))), + (hd(#1(Rules.dest_thm rules)))), wf_tac) - in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction) - end handle U.ERR _ => (rules,induction); + in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction) + end handle Utils.ERR _ => (rules,induction); (*---------------------------------------------------------------------- * The termination condition (tc) is simplified to |- tc = tc' (there @@ -938,14 +934,14 @@ val tc_eq = simplifier tc1 val _ = trace_thms "result: " [tc_eq] in - elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind) - handle U.ERR _ => - (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), + elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind) + handle Utils.ERR _ => + (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq) + (prove(tych(HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq))), terminator))) (r,ind) - handle U.ERR _ => - (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), + handle Utils.ERR _ => + (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq), simplify_induction theory tc_eq ind)) end @@ -963,35 +959,35 @@ * 3. return |- tc = tc' *---------------------------------------------------------------------*) fun simplify_nested_tc tc = - let val tc_eq = simplifier (tych (#2 (S.strip_forall tc))) + let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc))) in - R.GEN_ALL - (R.MATCH_MP Thms.eqT tc_eq - handle U.ERR _ => - (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))), + Rules.GEN_ALL + (Rules.MATCH_MP Thms.eqT tc_eq + handle Utils.ERR _ => + (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq) + (prove(tych(HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq))), terminator)) - handle U.ERR _ => tc_eq)) + handle Utils.ERR _ => tc_eq)) end (*------------------------------------------------------------------- * Attempt to simplify the termination conditions in each rule and * in the induction theorem. *-------------------------------------------------------------------*) - fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm + fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm fun loop ([],extras,R,ind) = (rev R, ind, extras) | loop ((r,ftcs)::rst, nthms, R, ind) = let val tcs = #1(strip_imp (concl r)) val extra_tcs = subtract (op aconv) tcs ftcs val extra_tc_thms = map simplify_nested_tc extra_tcs val (r1,ind1) = fold simplify_tc tcs (r,ind) - val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1 + val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1 in loop(rst, nthms@extra_tc_thms, r2::R, ind1) end - val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs) + val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs) val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1) in - {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras} + {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras} end; diff -r f4d3acf0c4cc -r 5391d34b0f4c src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Wed Dec 15 17:46:46 2010 +0100 +++ b/src/Tools/eqsubst.ML Wed Dec 15 18:45:14 2010 +0100 @@ -119,11 +119,8 @@ end; -structure EqSubst -: EQSUBST -= struct - -structure Z = Zipper; +structure EqSubst: EQSUBST = +struct (* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = @@ -196,11 +193,11 @@ abstracted out) for use in rewriting with RWInst.rw *) fun prep_zipper_match z = let - val t = Z.trm z - val c = Z.ctxt z - val Ts = Z.C.nty_ctxt c + val t = Zipper.trm z + val c = Zipper.ctxt z + val Ts = Zipper.C.nty_ctxt c val (FakeTs', Ts', t') = fakefree_badbounds Ts t - val absterm = mk_foo_match (Z.C.apply c) Ts' t' + val absterm = mk_foo_match (Zipper.C.apply c) Ts' t' in (t', (FakeTs', Ts', absterm)) end; @@ -291,7 +288,7 @@ (* Avoid considering replacing terms which have a var at the head as they always succeed trivially, and uninterestingly. *) fun valid_match_start z = - (case bot_left_leaf_of (Z.trm z) of + (case bot_left_leaf_of (Zipper.trm z) of Var _ => false | _ => true); @@ -302,33 +299,33 @@ fun search_lr_valid validf = let fun sf_valid_td_lr z = - let val here = if validf z then [Z.Here z] else [] in - case Z.trm z - of _ $ _ => [Z.LookIn (Z.move_down_left z)] + let val here = if validf z then [Zipper.Here z] else [] in + case Zipper.trm z + of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] @ here - @ [Z.LookIn (Z.move_down_right z)] - | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)] + @ [Zipper.LookIn (Zipper.move_down_right z)] + | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)] | _ => here end; - in Z.lzy_search sf_valid_td_lr end; + in Zipper.lzy_search sf_valid_td_lr end; (* search from bottom to top, left to right *) fun search_bt_valid validf = let fun sf_valid_td_lr z = - let val here = if validf z then [Z.Here z] else [] in - case Z.trm z - of _ $ _ => [Z.LookIn (Z.move_down_left z), - Z.LookIn (Z.move_down_right z)] @ here - | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here + let val here = if validf z then [Zipper.Here z] else [] in + case Zipper.trm z + of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), + Zipper.LookIn (Zipper.move_down_right z)] @ here + | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here | _ => here end; - in Z.lzy_search sf_valid_td_lr end; + in Zipper.lzy_search sf_valid_td_lr end; fun searchf_unify_gen f (sgn, maxidx, z) lhs = Seq.map (clean_unify_z sgn maxidx lhs) - (Z.limit_apply f z); + (Zipper.limit_apply f z); (* search all unifications *) val searchf_lr_unify_all = @@ -369,9 +366,9 @@ val conclterm = Logic.strip_imp_concl fixedbody; val conclthm = trivify conclterm; val maxidx = Thm.maxidx_of th; - val ft = ((Z.move_down_right (* ==> *) - o Z.move_down_left (* Trueprop *) - o Z.mktop + val ft = ((Zipper.move_down_right (* ==> *) + o Zipper.move_down_left (* Trueprop *) + o Zipper.mktop o Thm.prop_of) conclthm) in ((cfvs, conclthm), (sgn, maxidx, ft)) @@ -487,8 +484,8 @@ val pth = trivify asmt; val maxidx = Thm.maxidx_of th; - val ft = ((Z.move_down_right (* trueprop *) - o Z.mktop + val ft = ((Zipper.move_down_right (* trueprop *) + o Zipper.mktop o Thm.prop_of) pth) in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;