clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
authorwenzelm
Wed Apr 27 21:50:04 2011 +0200 (2011-04-27)
changeset 424951af81b70cf09
parent 42494 eef1a23c9077
child 42496 65ec88b369fd
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/partial_function.ML
src/Pure/Isar/element.ML
src/Pure/Isar/obtain.ML
src/Pure/goal.ML
src/Pure/subgoal.ML
src/Pure/variable.ML
     1.1 --- a/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 20:58:40 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 21:50:04 2011 +0200
     1.3 @@ -103,10 +103,10 @@
     1.4  (* Called on the INSTANTIATED branches of the congruence rule *)
     1.5  fun mk_branch ctxt t =
     1.6    let
     1.7 -    val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt
     1.8 +    val ((params, impl), ctxt') = Variable.focus t ctxt
     1.9      val (assms, concl) = Logic.strip_horn impl
    1.10    in
    1.11 -    (ctxt', fixes, assms, rhs_of concl)
    1.12 +    (ctxt', map #2 params, assms, rhs_of concl)
    1.13    end
    1.14  
    1.15  fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
     2.1 --- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 20:58:40 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 21:50:04 2011 +0200
     2.3 @@ -9,7 +9,6 @@
     2.4  sig
     2.5    val plural: string -> string -> 'a list -> string
     2.6  
     2.7 -  val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context
     2.8    val dest_all_all: term -> term list * term
     2.9  
    2.10    val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    2.11 @@ -39,19 +38,6 @@
    2.12    | plural sg pl _ = pl
    2.13  
    2.14  
    2.15 -(*term variant of Variable.focus*)
    2.16 -fun focus_term t ctxt =
    2.17 -  let
    2.18 -    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
    2.19 -    val (xs, Ts) = split_list ps;
    2.20 -    val (xs', ctxt') = Variable.variant_fixes xs ctxt;
    2.21 -    val ps' = xs' ~~ Ts;
    2.22 -    val inst = map Free ps'
    2.23 -    val t' = Term.subst_bounds (rev inst, Term.strip_all_body t);
    2.24 -    val ctxt'' = ctxt' |> fold Variable.declare_constraints inst;
    2.25 -  in ((ps', t'), ctxt'') end;
    2.26 -
    2.27 -
    2.28  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    2.29  fun dest_all_all (t as (Const ("all",_) $ _)) =
    2.30    let
     3.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 20:58:40 2011 +0200
     3.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 21:50:04 2011 +0200
     3.3 @@ -55,9 +55,9 @@
     3.4  
     3.5  fun dest_hhf ctxt t =
     3.6    let
     3.7 -    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
     3.8 +    val ((params, imp), ctxt') = Variable.focus t ctxt
     3.9    in
    3.10 -    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    3.11 +    (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    3.12    end
    3.13  
    3.14  fun mk_scheme' ctxt cases concl =
     4.1 --- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 20:58:40 2011 +0200
     4.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 21:50:04 2011 +0200
     4.3 @@ -165,7 +165,7 @@
     4.4          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
     4.5  
     4.6      val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
     4.7 -    val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy;
     4.8 +    val ((_, plain_eqn), _) = Variable.focus eqn lthy;
     4.9  
    4.10      val ((f_binding, fT), mixfix) = the_single fixes;
    4.11      val fname = Binding.name_of f_binding;
     5.1 --- a/src/Pure/Isar/element.ML	Wed Apr 27 20:58:40 2011 +0200
     5.2 +++ b/src/Pure/Isar/element.ML	Wed Apr 27 21:50:04 2011 +0200
     5.3 @@ -223,8 +223,8 @@
     5.4    let
     5.5      val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     5.6      fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
     5.7 -    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
     5.8 -    val As = Logic.strip_imp_prems (Thm.term_of prop');
     5.9 +    val xs = map (fix o #2) ps;
    5.10 +    val As = Logic.strip_imp_prems prop';
    5.11    in ((Binding.empty, (xs, As)), ctxt') end;
    5.12  
    5.13  in
    5.14 @@ -232,7 +232,6 @@
    5.15  fun pretty_statement ctxt kind raw_th =
    5.16    let
    5.17      val thy = Proof_Context.theory_of ctxt;
    5.18 -    val cert = Thm.cterm_of thy;
    5.19  
    5.20      val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
    5.21      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
    5.22 @@ -250,7 +249,7 @@
    5.23      pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
    5.24       (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
    5.25        else
    5.26 -        let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
    5.27 +        let val (clauses, ctxt'') = fold_map obtain cases ctxt'
    5.28          in pretty_stmt ctxt'' (Obtains clauses) end)
    5.29    end |> thm_name kind raw_th;
    5.30  
     6.1 --- a/src/Pure/Isar/obtain.ML	Wed Apr 27 20:58:40 2011 +0200
     6.2 +++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 21:50:04 2011 +0200
     6.3 @@ -196,7 +196,7 @@
     6.4      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
     6.5      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     6.6      val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
     6.7 -    val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
     6.8 +    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
     6.9      val (prems, ctxt'') =
    6.10        Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
    6.11          (Drule.strip_imp_prems stmt) fix_ctxt;
     7.1 --- a/src/Pure/goal.ML	Wed Apr 27 20:58:40 2011 +0200
     7.2 +++ b/src/Pure/goal.ML	Wed Apr 27 21:50:04 2011 +0200
     7.3 @@ -326,7 +326,7 @@
     7.4  
     7.5  fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
     7.6    let
     7.7 -    val ((_, goal'), ctxt') = Variable.focus goal ctxt;
     7.8 +    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
     7.9      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    7.10      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    7.11      val tacs = Rs |> map (fn R =>
     8.1 --- a/src/Pure/subgoal.ML	Wed Apr 27 20:58:40 2011 +0200
     8.2 +++ b/src/Pure/subgoal.ML	Wed Apr 27 21:50:04 2011 +0200
     8.3 @@ -33,7 +33,7 @@
     8.4    let
     8.5      val st = Simplifier.norm_hhf_protect raw_st;
     8.6      val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     8.7 -    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
     8.8 +    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
     8.9  
    8.10      val (asms, concl) =
    8.11        if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
     9.1 --- a/src/Pure/variable.ML	Wed Apr 27 20:58:40 2011 +0200
     9.2 +++ b/src/Pure/variable.ML	Wed Apr 27 21:50:04 2011 +0200
     9.3 @@ -67,7 +67,8 @@
     9.4      (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
     9.5    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
     9.6    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
     9.7 -  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
     9.8 +  val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
     9.9 +  val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
    9.10    val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
    9.11    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
    9.12    val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
    9.13 @@ -516,23 +517,34 @@
    9.14  val trade = gen_trade (import true) export;
    9.15  
    9.16  
    9.17 -(* focus on outermost parameters *)
    9.18 +(* focus on outermost parameters: !!x y z. B *)
    9.19 +
    9.20 +fun focus_params t ctxt =
    9.21 +  let
    9.22 +    val (xs, Ts) =
    9.23 +      split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
    9.24 +    val (xs', ctxt') = variant_fixes xs ctxt;
    9.25 +    val ps = xs' ~~ Ts;
    9.26 +    val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps;
    9.27 +  in ((xs, ps), ctxt'') end;
    9.28 +
    9.29 +fun focus t ctxt =
    9.30 +  let
    9.31 +    val ((xs, ps), ctxt') = focus_params t ctxt;
    9.32 +    val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
    9.33 +  in (((xs ~~ ps), t'), ctxt') end;
    9.34  
    9.35  fun forall_elim_prop t prop =
    9.36    Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
    9.37    |> Thm.cprop_of |> Thm.dest_arg;
    9.38  
    9.39 -fun focus goal ctxt =
    9.40 +fun focus_cterm goal ctxt =
    9.41    let
    9.42      val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
    9.43 -    val t = Thm.term_of goal;
    9.44 -    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
    9.45 -    val (xs, Ts) = split_list ps;
    9.46 -    val (xs', ctxt') = variant_fixes xs ctxt;
    9.47 -    val ps' = ListPair.map (cert o Free) (xs', Ts);
    9.48 +    val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
    9.49 +    val ps' = map (cert o Free) ps;
    9.50      val goal' = fold forall_elim_prop ps' goal;
    9.51 -    val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
    9.52 -  in ((xs ~~ ps', goal'), ctxt'') end;
    9.53 +  in ((xs ~~ ps', goal'), ctxt') end;
    9.54  
    9.55  fun focus_subgoal i st =
    9.56    let
    9.57 @@ -541,7 +553,7 @@
    9.58    in
    9.59      fold bind_term no_binds #>
    9.60      fold (declare_constraints o Var) all_vars #>
    9.61 -    focus (Thm.cprem_of st i)
    9.62 +    focus_cterm (Thm.cprem_of st i)
    9.63    end;
    9.64  
    9.65