src/Pure/variable.ML
changeset 20149 54d4ea7927be
parent 20123 88fa41273824
child 20162 d4bcb27686f9
     1.1 --- a/src/Pure/variable.ML	Tue Jul 18 20:01:44 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Jul 18 20:01:45 2006 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val used_types: Context.proof -> string list
     1.5    val is_declared: Context.proof -> string -> bool
     1.6    val is_fixed: Context.proof -> string -> bool
     1.7 +  val newly_fixed: Context.proof -> Context.proof -> string -> bool
     1.8    val def_sort: Context.proof -> indexname -> sort option
     1.9    val def_type: Context.proof -> bool -> indexname -> typ option
    1.10    val default_type: Context.proof -> string -> typ option
    1.11 @@ -44,8 +45,8 @@
    1.12    val import: bool -> thm list -> Context.proof -> thm list * Context.proof
    1.13    val tradeT: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.14    val trade: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.15 +  val focus: cterm -> Context.proof -> ((string * typ) list * cterm) * Context.proof
    1.16    val warn_extra_tfrees: Context.proof -> Context.proof -> unit
    1.17 -  val monomorphic: Context.proof -> term list -> term list
    1.18    val polymorphic: Context.proof -> term list -> term list
    1.19    val hidden_polymorphism: term -> typ -> (indexname * sort) list
    1.20    val add_binds: (indexname * term option) list -> Context.proof -> Context.proof
    1.21 @@ -117,6 +118,7 @@
    1.22  
    1.23  fun is_declared ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1);
    1.24  fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
    1.25 +fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    1.26  
    1.27  
    1.28  
    1.29 @@ -240,7 +242,7 @@
    1.30      val (ys, zs) = split_list (fixes_of ctxt);
    1.31      val names = names_of ctxt;
    1.32      val (xs', names') =
    1.33 -      if is_body ctxt then Name.variants (map Name.skolem xs) names
    1.34 +      if is_body ctxt then Name.variants xs names |>> map Name.skolem
    1.35        else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
    1.36          (xs, fold Name.declare xs names));
    1.37    in ctxt |> new_fixes names' xs xs' end;
    1.38 @@ -248,8 +250,8 @@
    1.39  fun invent_fixes raw_xs ctxt =
    1.40    let
    1.41      val names = names_of ctxt;
    1.42 -    val (xs, names') = Name.variants (map Name.clean raw_xs) names;
    1.43 -    val xs' = map Name.skolem xs;
    1.44 +    val xs = map Name.clean raw_xs;
    1.45 +    val (xs', names') = Name.variants xs names |>> map Name.skolem;
    1.46    in ctxt |> new_fixes names' xs xs' end;
    1.47  
    1.48  end;
    1.49 @@ -355,6 +357,23 @@
    1.50  val trade = gen_trade (import true) export;
    1.51  
    1.52  
    1.53 +(* focus on outer params *)
    1.54 +
    1.55 +fun forall_elim_prop t prop =
    1.56 +  Thm.beta_conversion false (Thm.capply (#2 (Thm.dest_comb prop)) t)
    1.57 +  |> Thm.cprop_of |> Thm.dest_comb |> #2;
    1.58 +
    1.59 +fun focus goal ctxt =
    1.60 +  let
    1.61 +    val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
    1.62 +    val t = Thm.term_of goal;
    1.63 +    val ps = rev (Term.rename_wrt_term t (Term.strip_all_vars t));   (*as they are printed :-*)
    1.64 +    val (xs, Ts) = split_list ps;
    1.65 +    val (xs', ctxt') = invent_fixes xs ctxt;
    1.66 +    val ps' = xs' ~~ Ts;
    1.67 +    val goal' = fold (forall_elim_prop o cert o Free) ps' goal;
    1.68 +  in ((ps', goal'), ctxt') end;
    1.69 +
    1.70  
    1.71  (** implicit polymorphism **)
    1.72  
    1.73 @@ -381,7 +400,7 @@
    1.74    end;
    1.75  
    1.76  
    1.77 -(* monomorphic vs. polymorphic terms *)
    1.78 +(* polymorphic terms *)
    1.79  
    1.80  fun monomorphic ctxt ts =
    1.81    #1 (importT_terms ts (fold declare_term ts ctxt));