src/Pure/Isar/proof_context.ML
changeset 52223 5bb6ae8acb87
parent 52156 576aceb343dc
child 53378 07990ba8c0ea
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   867 
   867 
   868 (** theorems **)
   868 (** theorems **)
   869 
   869 
   870 (* fact_tac *)
   870 (* fact_tac *)
   871 
   871 
       
   872 local
       
   873 
       
   874 fun comp_hhf_tac th i st =
       
   875   PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true}
       
   876     (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
       
   877 
   872 fun comp_incr_tac [] _ = no_tac
   878 fun comp_incr_tac [] _ = no_tac
   873   | comp_incr_tac (th :: ths) i =
   879   | comp_incr_tac (th :: ths) i =
   874       (fn st => Goal.compose_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
   880       (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
       
   881 
       
   882 in
   875 
   883 
   876 fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
   884 fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
   877 
   885 
   878 fun potential_facts ctxt prop =
   886 fun potential_facts ctxt prop =
   879   Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
   887   Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
   880 
   888 
   881 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
   889 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
       
   890 
       
   891 end;
   882 
   892 
   883 
   893 
   884 (* get_thm(s) *)
   894 (* get_thm(s) *)
   885 
   895 
   886 local
   896 local