# HG changeset patch # User wenzelm # Date 1426782357 -3600 # Node ID 696d87036f0496b04b9e8bb6ea66d400e5b3a3f3 # Parent d743e0e53f41da1af3f07e43a65a7be42ee3d3bd misc tuning; diff -r d743e0e53f41 -r 696d87036f04 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Mar 19 15:24:40 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Thu Mar 19 17:25:57 2015 +0100 @@ -34,6 +34,8 @@ (** reading instantiations **) +val partition_insts = List.partition (fn ((x, _), _) => String.isPrefix "'" x); + local fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi)); @@ -82,7 +84,7 @@ let val thy = Proof_Context.theory_of ctxt; - val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts; + val (type_insts, term_insts) = partition_insts mixed_insts; (* type instantiations *) @@ -196,80 +198,84 @@ (** tactics **) -(* resolution after lifting and instantation; may refer to parameters of the subgoal *) +(* resolution after lifting and instantiation; may refer to parameters of the subgoal *) -(* FIXME cleanup this mess!!! *) - -fun bires_inst_tac bires_flag ctxt insts thm = +fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) => let val thy = Proof_Context.theory_of ctxt; - (* Separate type and term insts *) - fun has_type_var ((x, _), _) = - (case Symbol.explode x of "'" :: _ => true | _ => false); - val Tinsts = filter has_type_var insts; - val tinsts = filter_out has_type_var insts; + + val (Tinsts, tinsts) = partition_insts mixed_insts; + val goal = Thm.term_of cgoal; - (* Tactic *) - fun tac i st = CSUBGOAL (fn (cgoal, _) => + val params = + Logic.strip_params goal + (*as they are printed: bound variables with the same name are renamed*) + |> Term.rename_wrt_term goal + |> rev; + val (param_names, ctxt') = ctxt + |> Variable.declare_thm thm + |> Thm.fold_terms Variable.declare_constraints st + |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); + + + (* process type insts: Tinsts_env *) + + fun absent xi = + error ("No such variable in theorem: " ^ Term.string_of_vname xi); + + val (rtypes, rsorts) = Drule.types_sorts thm; + fun readT (xi, s) = let - val goal = Thm.term_of cgoal; - val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*) - val params = rev (Term.rename_wrt_term goal params) - (*as they are printed: bound variables with*) - (*the same name are renamed during printing*) + val S = (case rsorts xi of SOME S => S | NONE => absent xi); + val T = Syntax.read_typ ctxt' s; + val U = TVar (xi, S); + in + if Sign.typ_instance thy (T, U) then (U, T) + else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails") + end; + val Tinsts_env = map readT Tinsts; - val (param_names, ctxt') = ctxt - |> Variable.declare_thm thm - |> Thm.fold_terms Variable.declare_constraints st - |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); + + (* preprocess rule: extract vars and their types, apply Tinsts *) - (* Process type insts: Tinsts_env *) - fun absent xi = error - ("No such variable in theorem: " ^ Term.string_of_vname xi); - val (rtypes, rsorts) = Drule.types_sorts thm; - fun readT (xi, s) = - let val S = case rsorts xi of SOME S => S | NONE => absent xi; - val T = Syntax.read_typ ctxt' s; - val U = TVar (xi, S); - in if Sign.typ_instance thy (T, U) then (U, T) - else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails") - end; - val Tinsts_env = map readT Tinsts; - (* Preprocess rule: extract vars and their types, apply Tinsts *) - fun get_typ xi = - (case rtypes xi of - SOME T => typ_subst_atomic Tinsts_env T - | NONE => absent xi); - val (xis, ss) = Library.split_list tinsts; - val Ts = map get_typ xis; + fun get_typ xi = + (case rtypes xi of + SOME T => typ_subst_atomic Tinsts_env T + | NONE => absent xi); + val (xis, ss) = Library.split_list tinsts; + val Ts = map get_typ xis; + + val (ts, envT) = + read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts; + val envT' = + map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env; + val cenv = + map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) + (distinct + (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) + (xis ~~ ts)); + - val (ts, envT) = - read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts; - val envT' = map (fn (ixn, T) => - (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; - val cenv = - map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) - (distinct - (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) - (xis ~~ ts)); - (* Lift and instantiate rule *) - val maxidx = Thm.maxidx_of st; - val paramTs = map #2 params - and inc = maxidx+1 - fun liftvar (Var ((a,j), T)) = - Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T) - | liftvar t = raise TERM("Variable expected", [t]); - fun liftterm t = - fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t); - fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct); - val lifttvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc); - val rule = Drule.instantiate_normalize - (map lifttvar envT', map liftpair cenv) - (Thm.lift_rule cgoal thm) - in - compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i - end) i st; - in tac end; + (* lift and instantiate rule *) + + val maxidx = Thm.maxidx_of st; + val paramTs = map #2 params; + val inc = maxidx + 1; + + fun lift_var (Var ((a, j), T)) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T) + | lift_var t = raise TERM ("Variable expected", [t]); + fun lift_term t = + fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t); + fun lift_inst (cv, ct) = (cterm_fun lift_var cv, cterm_fun lift_term ct); + val lift_tvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc); + + val rule = + Drule.instantiate_normalize + (map lift_tvar envT', map lift_inst cenv) + (Thm.lift_rule cgoal thm); + in + compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i + end) i st; val res_inst_tac = bires_inst_tac false; val eres_inst_tac = bires_inst_tac true;