src/Provers/hypsubst.ML
changeset 26992 4508f20818af
parent 26833 7c3757fccf0e
child 27572 67cd6ed76446
equal deleted inserted replaced
26991:2aa686443859 26992:4508f20818af
   141 
   141 
   142 end;
   142 end;
   143 
   143 
   144 val ssubst = standard (Data.sym RS Data.subst);
   144 val ssubst = standard (Data.sym RS Data.subst);
   145 
   145 
   146 fun inst_subst_tac b rl = SUBGOAL (fn (Bi, i) => fn st =>
   146 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   147   case try (Logic.strip_assums_hyp #> hd #>
   147   case try (Logic.strip_assums_hyp #> hd #>
   148       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) Bi of
   148       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   149     SOME (t, t') =>
   149     SOME (t, t') =>
   150       let
   150       let
       
   151         val Bi = Thm.term_of cBi;
   151         val ps = Logic.strip_params Bi;
   152         val ps = Logic.strip_params Bi;
   152         val U = fastype_of1 (rev (map snd ps), t);
   153         val U = Term.fastype_of1 (rev (map snd ps), t);
   153         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   154         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   154         val rl' = Thm.lift_rule (nth (cprems_of st) (i - 1)) rl;
   155         val rl' = Thm.lift_rule cBi rl;
   155         val Var (ixn, T) = head_of (Data.dest_Trueprop
   156         val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
   156           (Logic.strip_assums_concl (prop_of rl')));
   157           (Logic.strip_assums_concl (Thm.prop_of rl')));
   157         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   158         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   158           (Logic.strip_assums_concl (hd (prems_of rl'))));
   159           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
   159         val (Ts, V) = split_last (binder_types T);
   160         val (Ts, V) = split_last (Term.binder_types T);
   160         val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
   161         val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
   161             Bound j => subst_bounds (map Bound
   162             Bound j => subst_bounds (map Bound
   162               ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   163               ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   163           | t => abstract_over (t, incr_boundvars 1 Q));
   164           | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   164         val thy = theory_of_thm rl'
   165         val thy = Thm.theory_of_thm rl';
   165       in compose_tac (true, instantiate ([(ctyp_of thy V, ctyp_of thy U)],
   166         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
       
   167       in compose_tac (true, Drule.instantiate (instT,
   166         map (pairself (cterm_of thy))
   168         map (pairself (cterm_of thy))
   167           [(Var (ixn, Ts ---> U --> body_type T), u),
   169           [(Var (ixn, Ts ---> U --> body_type T), u),
   168            (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
   170            (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
   169            (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
   171            (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
   170         nprems_of rl) i st
   172         nprems_of rl) i
   171       end
   173       end
   172   | NONE => Seq.empty);
   174   | NONE => no_tac);
   173 
   175 
   174 val imp_intr_tac = rtac Data.imp_intr;
   176 val imp_intr_tac = rtac Data.imp_intr;
   175 
   177 
   176 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
   178 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
   177 (* premises containing meta-implications or quantifiers                *)
   179 (* premises containing meta-implications or quantifiers                *)