src/Tools/IsaPlanner/isand.ML
changeset 49340 25fc6e0da459
parent 49339 d1fcb4de8349
child 52242 2d634bfa1bbf
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 22:00:29 2012 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 23:18:26 2012 +0200
     1.3 @@ -26,13 +26,15 @@
     1.4    (* inserting meta level params for frees in the conditions *)
     1.5    val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
     1.6  
     1.7 +  val variant_names : Proof.context -> term list -> string list -> string list
     1.8 +
     1.9    (* meta level fixed params (i.e. !! vars) *)
    1.10 -  val fix_alls_term : int -> term -> term * term list
    1.11 +  val fix_alls_term : Proof.context -> int -> term -> term * term list
    1.12  
    1.13    val unfix_frees : cterm list -> thm -> thm
    1.14  
    1.15    (* assumptions/subgoals *)
    1.16 -  val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
    1.17 +  val fixed_subgoal_thms : Proof.context -> thm -> thm list * (thm list -> thm)
    1.18  end
    1.19  
    1.20  structure IsaND : ISA_ND =
    1.21 @@ -85,6 +87,15 @@
    1.22                  |> Drule.forall_intr_list cfvs
    1.23      in Drule.compose_single (solth', i, gth) end;
    1.24  
    1.25 +fun variant_names ctxt ts xs =
    1.26 +  let
    1.27 +    val names =
    1.28 +      Variable.names_of ctxt
    1.29 +      |> (fold o fold_aterms)
    1.30 +          (fn Var ((a, _), _) => Name.declare a
    1.31 +            | Free (a, _) => Name.declare a
    1.32 +            | _ => I) ts;
    1.33 +  in fst (fold_map Name.variant xs names) end;
    1.34  
    1.35  (* fix parameters of a subgoal "i", as free variables, and create an
    1.36  exporting function that will use the result of this proved goal to
    1.37 @@ -104,30 +115,26 @@
    1.38       ("As ==> SGi x'" : thm) ->
    1.39       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
    1.40  *)
    1.41 -fun fix_alls_term i t =
    1.42 +fun fix_alls_term ctxt i t =
    1.43      let
    1.44 -      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
    1.45 -      val names = Misc_Legacy.add_term_names (t,varnames);
    1.46        val gt = Logic.get_goal t i;
    1.47        val body = Term.strip_all_body gt;
    1.48        val alls = rev (Term.strip_all_vars gt);
    1.49 -      val fvs = map Free
    1.50 -                    (Name.variant_list names (map fst alls)
    1.51 -                       ~~ (map snd alls));
    1.52 +      val xs = variant_names ctxt [t] (map fst alls);
    1.53 +      val fvs = map Free (xs ~~ map snd alls);
    1.54      in ((subst_bounds (fvs,body)), fvs) end;
    1.55  
    1.56 -fun fix_alls_cterm i th =
    1.57 +fun fix_alls_cterm ctxt i th =
    1.58      let
    1.59        val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
    1.60 -      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
    1.61 +      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
    1.62        val cfvs = rev (map ctermify fvs);
    1.63        val ct_body = ctermify fixedbody
    1.64      in
    1.65        (ct_body, cfvs)
    1.66      end;
    1.67  
    1.68 -fun fix_alls' i =
    1.69 -     (apfst Thm.trivial) o (fix_alls_cterm i);
    1.70 +fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
    1.71  
    1.72  
    1.73  (* hide other goals *)
    1.74 @@ -154,9 +161,9 @@
    1.75       ("SGi x'" : thm) ->
    1.76       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
    1.77  *)
    1.78 -fun fix_alls i th =
    1.79 +fun fix_alls ctxt i th =
    1.80      let
    1.81 -      val (fixed_gth, fixedvars) = fix_alls' i th
    1.82 +      val (fixed_gth, fixedvars) = fix_alls' ctxt i th
    1.83        val (sml_gth, othergoals) = hide_other_goals fixed_gth
    1.84      in
    1.85        (sml_gth, export {fixes = fixedvars,
    1.86 @@ -208,7 +215,7 @@
    1.87     "G" : thm)
    1.88  *)
    1.89  (* requires being given solutions! *)
    1.90 -fun fixed_subgoal_thms th =
    1.91 +fun fixed_subgoal_thms ctxt th =
    1.92      let
    1.93        val (subgoals, expf) = subgoal_thms th;
    1.94  (*       fun export_sg (th, exp) = exp th; *)
    1.95 @@ -217,7 +224,7 @@
    1.96  (*           expf (map export_sg (ths ~~ expfs)); *)
    1.97      in
    1.98        apsnd export_sgs (Library.split_list (map (apsnd export_solution o
    1.99 -                                                 fix_alls 1) subgoals))
   1.100 +                                                 fix_alls ctxt 1) subgoals))
   1.101      end;
   1.102  
   1.103  end;