# HG changeset patch # User wenzelm # Date 1083954794 -7200 # Node ID f52f2cf2d1372d74cac063cd3dca1bf1e4632e03 # Parent 7d8d4c9b36fd7d44d0ea7d4e1ecd61a819c5ee88 tuned; diff -r 7d8d4c9b36fd -r f52f2cf2d137 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri May 07 20:32:50 2004 +0200 +++ b/src/Pure/Isar/attrib.ML Fri May 07 20:33:14 2004 +0200 @@ -195,8 +195,9 @@ val OF_local = syntax (local_thmss >> apply); -(* where: named instantiations *) -(* permits instantiation of type and term variables *) +(* where *) + +(*named instantiations; permits instantiation of type and term variables*) fun read_instantiate _ [] _ thm = thm | read_instantiate context_of insts x thm = @@ -209,7 +210,7 @@ fun has_type_var ((x, _), _) = (case Symbol.explode x of "'"::cs => true | cs => false); val (Tinst, tinsts) = take_prefix has_type_var insts; - val _ = if exists has_type_var tinsts + val _ = if exists has_type_var tinsts then error "Type instantiations must occur before term instantiations." else (); @@ -218,20 +219,20 @@ val tinsts = filter_out has_type_var insts; (* Type instantiations first *) - (* Process type insts: Tinsts_env *) - fun absent xi = error - ("No such type variable in theorem: " ^ + (* Process type insts: Tinsts_env *) + fun absent xi = error + ("No such type variable in theorem: " ^ Syntax.string_of_vname xi); - val (rtypes, rsorts) = types_sorts thm; - fun readT (xi, s) = - let val S = case rsorts xi of Some S => S | None => absent xi; - val T = ProofContext.read_typ ctxt s; - in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T) - else error - ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") - end; - val Tinsts_env = map readT Tinsts; - val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env); + val (rtypes, rsorts) = types_sorts thm; + fun readT (xi, s) = + let val S = case rsorts xi of Some S => S | None => absent xi; + val T = ProofContext.read_typ ctxt s; + in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T) + else error + ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") + end; + val Tinsts_env = map readT Tinsts; + val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env); val thm' = Thm.instantiate (cenvT, []) thm; (* Instantiate, but don't normalise: *) (* this happens after term insts anyway. *) @@ -247,11 +248,13 @@ val Ts = map get_typ xs; val used = add_term_tvarnames (prop_of thm',[]) - (* Names of TVars occuring in thm'. read_termTs ensures + (* Names of TVars occuring in thm'. read_def_termTs ensures that new TVars introduced when reading the instantiation string are distinct from those occuring in the theorem. *) - val (ts, envT) = ProofContext.read_termTs used ctxt (ss ~~ Ts); + val (ts, envT) = + ProofContext.read_termTs ctxt (K false) (K None) (K None) used (ss ~~ Ts); + val cenvT = map (apsnd (Thm.ctyp_of sign)) envT; val cenv = map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) diff -r 7d8d4c9b36fd -r f52f2cf2d137 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri May 07 20:32:50 2004 +0200 +++ b/src/Pure/Isar/method.ML Fri May 07 20:33:14 2004 +0200 @@ -326,8 +326,8 @@ (* res_inst_tac etc. *) -(* Reimplemented to support both static (Isar) and dynamic (proof state) - context. By Clemens Ballarin. *) +(*Reimplemented to support both static (Isar) and dynamic (proof state) + context. By Clemens Ballarin.*) fun bires_inst_tac bires_flag ctxt insts thm = let @@ -347,7 +347,7 @@ val (types, sorts) = types_sorts st; (* Process type insts: Tinsts_env *) fun absent xi = error - ("No such variable in theorem: " ^ Syntax.string_of_vname xi); + ("No such variable in theorem: " ^ Syntax.string_of_vname xi); val (rtypes, rsorts) = types_sorts thm; fun readT (xi, s) = let val S = case rsorts xi of Some S => S | None => absent xi; @@ -364,52 +364,52 @@ | None => absent xi); val (xis, ss) = Library.split_list tinsts; val Ts = map get_typ xis; - val (_, _, Bi, _) = dest_state(st,i) - val params = Logic.strip_params Bi - (* params of subgoal i as string typ pairs *) - val params = rev(Term.rename_wrt_term Bi params) - (* as they are printed: bound variables with *) + val (_, _, Bi, _) = dest_state(st,i) + val params = Logic.strip_params Bi + (* params of subgoal i as string typ pairs *) + val params = rev(Term.rename_wrt_term Bi params) + (* as they are printed: bound variables with *) (* the same name are renamed during printing *) fun types' (a, ~1) = (case assoc (params, a) of None => types (a, ~1) | some => some) | types' xi = types xi; - val used = add_term_tvarnames - (prop_of st $ prop_of thm,[]) - val (ts, envT) = - ProofContext.read_termTs_env (types', sorts, used) ctxt (ss ~~ Ts); - val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env); - val cenv = - map - (fn (xi, t) => - pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) - (gen_distinct - (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) - (xis ~~ ts)); - (* Lift and instantiate rule *) - val {maxidx, ...} = rep_thm st; - val paramTs = map #2 params - and inc = maxidx+1 - fun liftvar (Var ((a,j), T)) = - Var((a, j+inc), paramTs ---> incr_tvar inc T) - | liftvar t = raise TERM("Variable expected", [t]); - fun liftterm t = list_abs_free - (params, Logic.incr_indexes(paramTs,inc) t) - fun liftpair (cv,ct) = - (cterm_fun liftvar cv, cterm_fun liftterm ct) - fun lifttvar((a,i),ctyp) = - let val {T,sign} = rep_ctyp ctyp - in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end - val rule = Drule.instantiate - (map lifttvar cenvT, map liftpair cenv) - (lift_rule (st, i) thm) + fun internal x = is_some (types' (x, ~1)); + val used = Term.add_term_tvarnames (Thm.prop_of st $ Thm.prop_of thm, []); + val (ts, envT) = + ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); + val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env); + val cenv = + map + (fn (xi, t) => + pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) + (gen_distinct + (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) + (xis ~~ ts)); + (* Lift and instantiate rule *) + val {maxidx, ...} = rep_thm st; + val paramTs = map #2 params + and inc = maxidx+1 + fun liftvar (Var ((a,j), T)) = + Var((a, j+inc), paramTs ---> incr_tvar inc T) + | liftvar t = raise TERM("Variable expected", [t]); + fun liftterm t = list_abs_free + (params, Logic.incr_indexes(paramTs,inc) t) + fun liftpair (cv,ct) = + (cterm_fun liftvar cv, cterm_fun liftterm ct) + fun lifttvar((a,i),ctyp) = + let val {T,sign} = rep_ctyp ctyp + in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end + val rule = Drule.instantiate + (map lifttvar cenvT, map liftpair cenv) + (lift_rule (st, i) thm) in - if i > nprems_of st then no_tac st - else st |> - compose_tac (bires_flag, rule, nprems_of thm) i + if i > nprems_of st then no_tac st + else st |> + compose_tac (bires_flag, rule, nprems_of thm) i end - handle TERM (msg,_) => (warning msg; no_tac st) - | THM (msg,_,_) => (warning msg; no_tac st); + handle TERM (msg,_) => (warning msg; no_tac st) + | THM (msg,_,_) => (warning msg; no_tac st); in tac end; @@ -420,7 +420,7 @@ METHOD (fn facts => quant (insert_tac facts THEN' inst_tac ctxt insts thm)) | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; - + val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac; val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac; @@ -471,6 +471,7 @@ fun thin_tac ctxt s = bires_inst_tac true ctxt [(("V", 0), s)] thin_rl; + (* simple Prolog interpreter *) fun prolog_tac rules facts = @@ -685,6 +686,7 @@ fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; + (** method text **) (* datatype text *)