# HG changeset patch # User wenzelm # Date 1427209071 -3600 # Node ID f05ef8c62e4f3b8b13612c5b56000870e9185546 # Parent d453c69596cc0d546f76c813de63621e8f4830d3 admit dummy patterns in instantiations; clarified context; diff -r d453c69596cc -r f05ef8c62e4f NEWS --- a/NEWS Tue Mar 24 11:53:18 2015 +0100 +++ b/NEWS Tue Mar 24 15:57:51 2015 +0100 @@ -66,6 +66,10 @@ these variables become schematic in the instantiated theorem. This behaviour is analogous to 'for' in attributes "where" and "of". +* Explicit instantiation via attributes "where", "of", and proof methods +"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns +("_") that stand for anonymous local variables. + * Command "class_deps" takes optional sort arguments constraining the search space. diff -r d453c69596cc -r f05ef8c62e4f src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Tue Mar 24 11:53:18 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Tue Mar 24 15:57:51 2015 +0100 @@ -68,18 +68,18 @@ else error_var "Bad sort for instantiation of type variable: " (xi, pos) end; -fun read_terms ctxt ss Ts = +fun read_terms ss Ts ctxt = let fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; - val ts = map2 parse Ts ss; + val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt; val ts' = map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts - |> Syntax.check_terms ctxt - |> Variable.polymorphic ctxt; + |> Syntax.check_terms ctxt' + |> Variable.polymorphic ctxt'; val Ts' = map Term.fastype_of ts'; val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty; val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; - in (ts', tyenv') end; + in ((ts', tyenv'), ctxt') end; fun make_instT f v = let @@ -95,7 +95,7 @@ in -fun read_insts ctxt mixed_insts thm = +fun read_insts thm mixed_insts ctxt = let val (type_insts, term_insts) = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts; @@ -110,7 +110,7 @@ (*term instantiations*) val (xs, ss) = split_list term_insts; val Ts = map (the_type vars1) xs; - val (ts, inferred) = read_terms ctxt ss Ts; + val ((ts, inferred), ctxt') = read_terms ss Ts ctxt; (*implicit type instantiations*) val instT2 = Term_Subst.instantiateT inferred; @@ -121,7 +121,7 @@ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; val inst_vars = map_filter (make_inst inst2) vars2; - in (inst_tvars, inst_vars) end; + in ((inst_tvars, inst_vars), ctxt') end; end; @@ -134,13 +134,13 @@ val ctxt' = ctxt |> Variable.declare_thm thm |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2; - val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm; + val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt'; in thm |> Drule.instantiate_normalize - (map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars, - map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars) - |> singleton (Variable.export ctxt' ctxt) + (map (apply2 (Thm.ctyp_of ctxt'') o apfst TVar) inst_tvars, + map (apply2 (Thm.cterm_of ctxt'') o apfst Var) inst_vars) + |> singleton (Variable.export ctxt'' ctxt) |> Rule_Cases.save thm end; @@ -225,7 +225,7 @@ val (fixed, fixes_ctxt) = param_ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes; - val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm; + val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt; (* lift and instantiate rule *) @@ -238,14 +238,14 @@ (Logic.incr_indexes (fixed, paramTs, inc) t); val inst_tvars' = inst_tvars - |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar); + |> map (apply2 (Thm.ctyp_of inst_ctxt o Logic.incr_tvar inc) o apfst TVar); val inst_vars' = inst_vars - |> map (fn (v, t) => apply2 (Thm.cterm_of fixes_ctxt) (lift_var v, lift_term t)); + |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t)); val thm' = Drule.instantiate_normalize (inst_tvars', inst_vars') (Thm.lift_rule cgoal thm) - |> singleton (Variable.export fixes_ctxt param_ctxt); + |> singleton (Variable.export inst_ctxt param_ctxt); in compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st; diff -r d453c69596cc -r f05ef8c62e4f src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Mar 24 11:53:18 2015 +0100 +++ b/src/Pure/variable.ML Tue Mar 24 15:57:51 2015 +0100 @@ -52,15 +52,16 @@ val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context val auto_fixes: term -> Proof.context -> Proof.context + val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val dest_fixes: Proof.context -> (string * string) list - val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list val exportT: Proof.context -> Proof.context -> thm list -> thm list val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism + val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context val import_inst: bool -> term list -> Proof.context -> (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context @@ -460,11 +461,21 @@ |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])) |> declare_term t; -fun invent_types Ss ctxt = - let - val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; - val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; - in (tfrees, ctxt') end; + +(* dummy patterns *) + +fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = + let val ([x], ctxt') = add_fixes [Name.uu_] ctxt + in (Free (x, T), ctxt') end + | fix_dummy_patterns (Abs (x, T, b)) ctxt = + let val (b', ctxt') = fix_dummy_patterns b ctxt + in (Abs (x, T, b'), ctxt') end + | fix_dummy_patterns (t $ u) ctxt = + let + val (t', ctxt') = fix_dummy_patterns t ctxt; + val (u', ctxt'') = fix_dummy_patterns u ctxt'; + in (t' $ u', ctxt'') end + | fix_dummy_patterns a ctxt = (a, ctxt); @@ -541,6 +552,12 @@ (** import -- fix schematic type/term variables **) +fun invent_types Ss ctxt = + let + val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; + val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; + in (tfrees, ctxt') end; + fun importT_inst ts ctxt = let val tvars = rev (fold Term.add_tvars ts []);