observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
authorwenzelm
Wed Sep 12 23:18:26 2012 +0200 (2012-09-12)
changeset 4934025fc6e0da459
parent 49339 d1fcb4de8349
child 49343 bcce6988f6fa
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/post.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Wed Sep 12 22:00:29 2012 +0200
     1.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Sep 12 23:18:26 2012 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  signature CASE_SPLIT =
     1.5  sig
     1.6    (* try to recursively split conjectured thm to given list of thms *)
     1.7 -  val splitto : thm list -> thm -> thm
     1.8 +  val splitto : Proof.context -> thm list -> thm -> thm
     1.9  end;
    1.10  
    1.11  structure CaseSplit: CASE_SPLIT =
    1.12 @@ -121,7 +121,7 @@
    1.13  (* Note: This should not be a separate tactic but integrated into the
    1.14  case split done during recdef's case analysis, this would avoid us
    1.15  having to (re)search for variables to split. *)
    1.16 -fun splitto splitths genth =
    1.17 +fun splitto ctxt splitths genth =
    1.18      let
    1.19        val _ = not (null splitths) orelse error "splitto: no given splitths";
    1.20        val thy = Thm.theory_of_thm genth;
    1.21 @@ -142,7 +142,7 @@
    1.22              let
    1.23                val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
    1.24                val split_thm = mk_casesplit_goal_thm thy v gt;
    1.25 -              val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
    1.26 +              val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
    1.27              in
    1.28                expf (map recsplitf subthms)
    1.29              end)
     2.1 --- a/src/HOL/Tools/TFL/post.ML	Wed Sep 12 22:00:29 2012 +0200
     2.2 +++ b/src/HOL/Tools/TFL/post.ML	Wed Sep 12 23:18:26 2012 +0200
     2.3 @@ -166,18 +166,18 @@
     2.4    fun get_related_thms i = 
     2.5        map_filter ((fn (r,x) => if x = i then SOME r else NONE));
     2.6  
     2.7 -  fun solve_eq (th, [], i) =  error "derive_init_eqs: missing rules"
     2.8 -    | solve_eq (th, [a], i) = [(a, i)]
     2.9 -    | solve_eq (th, splitths, i) =
    2.10 +  fun solve_eq _ (th, [], i) =  error "derive_init_eqs: missing rules"
    2.11 +    | solve_eq _ (th, [a], i) = [(a, i)]
    2.12 +    | solve_eq ctxt (th, splitths, i) =
    2.13        (writeln "Proving unsplit equation...";
    2.14        [((Drule.export_without_context o Object_Logic.rulify_no_asm)
    2.15 -          (CaseSplit.splitto splitths th), i)])
    2.16 +          (CaseSplit.splitto ctxt splitths th), i)])
    2.17        handle ERROR s => 
    2.18               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
    2.19  in
    2.20 -fun derive_init_eqs thy rules eqs =
    2.21 -  map (Thm.trivial o Thm.cterm_of thy o HOLogic.mk_Trueprop) eqs
    2.22 -  |> map_index (fn (i, e) => solve_eq (e, (get_related_thms i rules), i))
    2.23 +fun derive_init_eqs ctxt rules eqs =
    2.24 +  map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs
    2.25 +  |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
    2.26    |> flat;
    2.27  end;
    2.28  
    2.29 @@ -192,7 +192,7 @@
    2.30        val (lhs, _) = Logic.dest_equals (prop_of def)
    2.31        val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats def
    2.32        val rules' = 
    2.33 -          if strict then derive_init_eqs thy rules eqs
    2.34 +          if strict then derive_init_eqs ctxt rules eqs
    2.35            else rules
    2.36    in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end;
    2.37  
     3.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 22:00:29 2012 +0200
     3.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 23:18:26 2012 +0200
     3.3 @@ -26,13 +26,15 @@
     3.4    (* inserting meta level params for frees in the conditions *)
     3.5    val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
     3.6  
     3.7 +  val variant_names : Proof.context -> term list -> string list -> string list
     3.8 +
     3.9    (* meta level fixed params (i.e. !! vars) *)
    3.10 -  val fix_alls_term : int -> term -> term * term list
    3.11 +  val fix_alls_term : Proof.context -> int -> term -> term * term list
    3.12  
    3.13    val unfix_frees : cterm list -> thm -> thm
    3.14  
    3.15    (* assumptions/subgoals *)
    3.16 -  val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
    3.17 +  val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
    3.18  end
    3.19  
    3.20  structure IsaND : ISA_ND =
    3.21 @@ -85,6 +87,15 @@
    3.22                  |> Drule.forall_intr_list cfvs
    3.23      in Drule.compose_single (solth', i, gth) end;
    3.24  
    3.25 +fun variant_names ctxt ts xs =
    3.26 +  let
    3.27 +    val names =
    3.28 +      Variable.names_of ctxt
    3.29 +      |> (fold o fold_aterms)
    3.30 +          (fn Var ((a, _), _) => Name.declare a
    3.31 +            | Free (a, _) => Name.declare a
    3.32 +            | _ => I) ts;
    3.33 +  in fst (fold_map Name.variant xs names) end;
    3.34  
    3.35  (* fix parameters of a subgoal "i", as free variables, and create an
    3.36  exporting function that will use the result of this proved goal to
    3.37 @@ -104,30 +115,26 @@
    3.38       ("As ==> SGi x'" : thm) ->
    3.39       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
    3.40  *)
    3.41 -fun fix_alls_term i t =
    3.42 +fun fix_alls_term ctxt i t =
    3.43      let
    3.44 -      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
    3.45 -      val names = Misc_Legacy.add_term_names (t,varnames);
    3.46        val gt = Logic.get_goal t i;
    3.47        val body = Term.strip_all_body gt;
    3.48        val alls = rev (Term.strip_all_vars gt);
    3.49 -      val fvs = map Free
    3.50 -                    (Name.variant_list names (map fst alls)
    3.51 -                       ~~ (map snd alls));
    3.52 +      val xs = variant_names ctxt [t] (map fst alls);
    3.53 +      val fvs = map Free (xs ~~ map snd alls);
    3.54      in ((subst_bounds (fvs,body)), fvs) end;
    3.55  
    3.56 -fun fix_alls_cterm i th =
    3.57 +fun fix_alls_cterm ctxt i th =
    3.58      let
    3.59        val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
    3.60 -      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
    3.61 +      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
    3.62        val cfvs = rev (map ctermify fvs);
    3.63        val ct_body = ctermify fixedbody
    3.64      in
    3.65        (ct_body, cfvs)
    3.66      end;
    3.67  
    3.68 -fun fix_alls' i =
    3.69 -     (apfst Thm.trivial) o (fix_alls_cterm i);
    3.70 +fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
    3.71  
    3.72  
    3.73  (* hide other goals *)
    3.74 @@ -154,9 +161,9 @@
    3.75       ("SGi x'" : thm) ->
    3.76       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
    3.77  *)
    3.78 -fun fix_alls i th =
    3.79 +fun fix_alls ctxt i th =
    3.80      let
    3.81 -      val (fixed_gth, fixedvars) = fix_alls' i th
    3.82 +      val (fixed_gth, fixedvars) = fix_alls' ctxt i th
    3.83        val (sml_gth, othergoals) = hide_other_goals fixed_gth
    3.84      in
    3.85        (sml_gth, export {fixes = fixedvars,
    3.86 @@ -208,7 +215,7 @@
    3.87     "G" : thm)
    3.88  *)
    3.89  (* requires being given solutions! *)
    3.90 -fun fixed_subgoal_thms th =
    3.91 +fun fixed_subgoal_thms ctxt th =
    3.92      let
    3.93        val (subgoals, expf) = subgoal_thms th;
    3.94  (*       fun export_sg (th, exp) = exp th; *)
    3.95 @@ -217,7 +224,7 @@
    3.96  (*           expf (map export_sg (ths ~~ expfs)); *)
    3.97      in
    3.98        apsnd export_sgs (Library.split_list (map (apsnd export_solution o
    3.99 -                                                 fix_alls 1) subgoals))
   3.100 +                                                 fix_alls ctxt 1) subgoals))
   3.101      end;
   3.102  
   3.103  end;
     4.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Sep 12 22:00:29 2012 +0200
     4.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Sep 12 23:18:26 2012 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5    (* Rewrite: give it instantiation infromation, a rule, and the
     4.6    target thm, and it will return the rewritten target thm *)
     4.7 -  val rw :
     4.8 +  val rw : Proof.context ->
     4.9        ((indexname * (sort * typ)) list *  (* type var instantiations *)
    4.10         (indexname * (typ * term)) list)  (* schematic var instantiations *)
    4.11        * (string * typ) list           (* Fake named bounds + types *)
    4.12 @@ -37,16 +37,6 @@
    4.13      in thm3 end;
    4.14  
    4.15  
    4.16 -(* to get the free names of a theorem (including hyps and flexes) *)
    4.17 -fun usednames_of_thm th =
    4.18 -    let val rep = Thm.rep_thm th
    4.19 -      val hyps = #hyps rep
    4.20 -      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    4.21 -      val prop = #prop rep
    4.22 -    in
    4.23 -      List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    4.24 -    end;
    4.25 -
    4.26  (* Given a list of variables that were bound, and a that has been
    4.27  instantiated with free variable placeholders for the bound vars, it
    4.28  creates an abstracted version of the theorem, with local bound vars as
    4.29 @@ -64,22 +54,22 @@
    4.30  note: assumes rule is instantiated
    4.31  *)
    4.32  (* Note, we take abstraction in the order of last abstraction first *)
    4.33 -fun mk_abstractedrule TsFake Ts rule =
    4.34 +fun mk_abstractedrule ctxt TsFake Ts rule =
    4.35      let
    4.36        val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
    4.37  
    4.38        (* now we change the names of temporary free vars that represent
    4.39           bound vars with binders outside the redex *)
    4.40 -      val names = usednames_of_thm rule;
    4.41 -      val (fromnames,tonames,_,Ts') =
    4.42 -          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
    4.43 -                    let val n2 = singleton (Name.variant_list names) n in
    4.44 +
    4.45 +      val ns =
    4.46 +        IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts);
    4.47 +
    4.48 +      val (fromnames, tonames, Ts') =
    4.49 +          fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
    4.50                        (ctermify (Free(faken,ty)) :: rnf,
    4.51                         ctermify (Free(n2,ty)) :: rnt,
    4.52 -                       n2 :: names,
    4.53 -                       (n2,ty) :: Ts'')
    4.54 -                    end)
    4.55 -                (([],[],names, []), TsFake~~Ts);
    4.56 +                       (n2,ty) :: Ts''))
    4.57 +                (TsFake ~~ Ts ~~ ns) ([], [], []);
    4.58  
    4.59        (* rename conflicting free's in the rule to avoid cconflicts
    4.60        with introduced vars from bounds outside in redex *)
    4.61 @@ -105,10 +95,9 @@
    4.62  (* Create a table of vars to be renamed after instantiation - ie
    4.63        other uninstantiated vars in the hyps of the rule
    4.64        ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
    4.65 -fun mk_renamings tgt rule_inst =
    4.66 +fun mk_renamings ctxt tgt rule_inst =
    4.67      let
    4.68 -      val rule_conds = Thm.prems_of rule_inst
    4.69 -      val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
    4.70 +      val rule_conds = Thm.prems_of rule_inst;
    4.71        val (_, cond_vs) =
    4.72            Library.foldl (fn ((tyvs, vs), t) =>
    4.73                      (union (op =) (Misc_Legacy.term_tvars t) tyvs,
    4.74 @@ -116,13 +105,8 @@
    4.75                  (([],[]), rule_conds);
    4.76        val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
    4.77        val vars_to_fix = union (op =) termvars cond_vs;
    4.78 -      val (renamings, _) =
    4.79 -          List.foldr (fn (((n,i),ty), (vs, names')) =>
    4.80 -                    let val n' = singleton (Name.variant_list names') n in
    4.81 -                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
    4.82 -                    end)
    4.83 -                ([], names) vars_to_fix;
    4.84 -    in renamings end;
    4.85 +      val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix);
    4.86 +  in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end;
    4.87  
    4.88  (* make a new fresh typefree instantiation for the given tvar *)
    4.89  fun new_tfree (tv as (ix,sort), (pairs,used)) =
    4.90 @@ -184,7 +168,7 @@
    4.91  first abstraction first.  FakeTs has abstractions using the fake name
    4.92  - ie the name distinct from all other abstractions. *)
    4.93  
    4.94 -fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
    4.95 +fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
    4.96      let
    4.97        (* general signature info *)
    4.98        val target_sign = (Thm.theory_of_thm target_thm);
    4.99 @@ -192,7 +176,7 @@
   4.100        val ctypeify = Thm.ctyp_of target_sign;
   4.101  
   4.102        (* fix all non-instantiated tvars *)
   4.103 -      val (fixtyinsts, othertfrees) =
   4.104 +      val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
   4.105            mk_fixtvar_tyinsts nonfixed_typinsts
   4.106                               [Thm.prop_of rule, Thm.prop_of target_thm];
   4.107        val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   4.108 @@ -236,8 +220,7 @@
   4.109        (* Create a table of vars to be renamed after instantiation - ie
   4.110        other uninstantiated vars in the hyps the *instantiated* rule
   4.111        ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   4.112 -      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
   4.113 -                                   rule_inst;
   4.114 +      val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
   4.115        val cterm_renamings =
   4.116            map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   4.117  
   4.118 @@ -249,7 +232,7 @@
   4.119        val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   4.120        val (cprems, abstract_rule_inst) =
   4.121            rule_inst |> Thm.instantiate ([], cterm_renamings)
   4.122 -                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   4.123 +                    |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
   4.124        val specific_tgt_rule =
   4.125            beta_eta_contract
   4.126              (Thm.combination couter_inst abstract_rule_inst);
     5.1 --- a/src/Tools/eqsubst.ML	Wed Sep 12 22:00:29 2012 +0200
     5.2 +++ b/src/Tools/eqsubst.ML	Wed Sep 12 23:18:26 2012 +0200
     5.3 @@ -260,15 +260,15 @@
     5.4  (* conclthm is a theorem of for just the conclusion *)
     5.5  (* m is instantiation/match information *)
     5.6  (* rule is the equation for substitution *)
     5.7 -fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
     5.8 -    (RWInst.rw m rule conclthm)
     5.9 +fun apply_subst_in_concl ctxt i th (cfvs, conclthm) rule m =
    5.10 +    (RWInst.rw ctxt m rule conclthm)
    5.11        |> IsaND.unfix_frees cfvs
    5.12        |> RWInst.beta_eta_contract
    5.13        |> (fn r => Tactic.rtac r i th);
    5.14  
    5.15  (* substitute within the conclusion of goal i of gth, using a meta
    5.16  equation rule. Note that we assume rule has var indicies zero'd *)
    5.17 -fun prep_concl_subst i gth =
    5.18 +fun prep_concl_subst ctxt i gth =
    5.19      let
    5.20        val th = Thm.incr_indexes 1 gth;
    5.21        val tgt_term = Thm.prop_of th;
    5.22 @@ -277,7 +277,7 @@
    5.23        val ctermify = Thm.cterm_of sgn;
    5.24        val trivify = Thm.trivial o ctermify;
    5.25  
    5.26 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
    5.27 +      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    5.28        val cfvs = rev (map ctermify fvs);
    5.29  
    5.30        val conclterm = Logic.strip_imp_concl fixedbody;
    5.31 @@ -294,12 +294,12 @@
    5.32  (* substitute using an object or meta level equality *)
    5.33  fun eqsubst_tac' ctxt searchf instepthm i th =
    5.34      let
    5.35 -      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
    5.36 +      val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
    5.37        val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
    5.38        fun rewrite_with_thm r =
    5.39            let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
    5.40            in searchf searchinfo lhs
    5.41 -             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
    5.42 +             |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end;
    5.43      in stepthms |> Seq.maps rewrite_with_thm end;
    5.44  
    5.45  
    5.46 @@ -347,11 +347,11 @@
    5.47      SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    5.48  
    5.49  (* apply a substitution inside assumption j, keeps asm in the same place *)
    5.50 -fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
    5.51 +fun apply_subst_in_asm ctxt i th rule ((cfvs, j, ngoalprems, pth),m) =
    5.52      let
    5.53        val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
    5.54        val preelimrule =
    5.55 -          (RWInst.rw m rule pth)
    5.56 +          (RWInst.rw ctxt m rule pth)
    5.57              |> (Seq.hd o prune_params_tac)
    5.58              |> Thm.permute_prems 0 ~1 (* put old asm first *)
    5.59              |> IsaND.unfix_frees cfvs (* unfix any global params *)
    5.60 @@ -380,7 +380,7 @@
    5.61  subgoal i of gth. Note the repetition of work done for each
    5.62  assumption, i.e. this can be made more efficient for search over
    5.63  multiple assumptions.  *)
    5.64 -fun prep_subst_in_asm i gth j =
    5.65 +fun prep_subst_in_asm ctxt i gth j =
    5.66      let
    5.67        val th = Thm.incr_indexes 1 gth;
    5.68        val tgt_term = Thm.prop_of th;
    5.69 @@ -389,7 +389,7 @@
    5.70        val ctermify = Thm.cterm_of sgn;
    5.71        val trivify = Thm.trivial o ctermify;
    5.72  
    5.73 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
    5.74 +      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    5.75        val cfvs = rev (map ctermify fvs);
    5.76  
    5.77        val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
    5.78 @@ -404,8 +404,8 @@
    5.79      in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
    5.80  
    5.81  (* prepare subst in every possible assumption *)
    5.82 -fun prep_subst_in_asms i gth =
    5.83 -    map (prep_subst_in_asm i gth)
    5.84 +fun prep_subst_in_asms ctxt i gth =
    5.85 +    map (prep_subst_in_asm ctxt i gth)
    5.86          ((fn l => Library.upto (1, length l))
    5.87             (Logic.prems_of_goal (Thm.prop_of gth) i));
    5.88  
    5.89 @@ -413,7 +413,7 @@
    5.90  (* substitute in an assumption using an object or meta level equality *)
    5.91  fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
    5.92      let
    5.93 -      val asmpreps = prep_subst_in_asms i th;
    5.94 +      val asmpreps = prep_subst_in_asms ctxt i th;
    5.95        val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
    5.96        fun rewrite_with_thm r =
    5.97            let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
    5.98 @@ -426,7 +426,7 @@
    5.99                                 (occ_search 1 moreasms))
   5.100                                (* find later substs also *)
   5.101            in
   5.102 -            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   5.103 +            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
   5.104            end;
   5.105      in stepthms |> Seq.maps rewrite_with_thm end;
   5.106