src/Pure/Isar/local_defs.ML
changeset 20049 f48c4a3a34bc
parent 20021 815393c02db9
child 20224 9c40a144ee0e
equal deleted inserted replaced
20048:a7964311f1fb 20049:f48c4a3a34bc
   142 
   142 
   143 (* derived defs -- potentially within the object-logic *)
   143 (* derived defs -- potentially within the object-logic *)
   144 
   144 
   145 fun derived_def ctxt conditional prop =
   145 fun derived_def ctxt conditional prop =
   146   let
   146   let
   147     val thy = ProofContext.theory_of ctxt;
       
   148     val ((c, T), rhs) = prop
   147     val ((c, T), rhs) = prop
   149       |> Thm.cterm_of thy
   148       |> Thm.cterm_of (ProofContext.theory_of ctxt)
   150       |> meta_rewrite (Context.Proof ctxt)
   149       |> meta_rewrite (Context.Proof ctxt)
   151       |> (snd o Logic.dest_equals o Thm.prop_of)
   150       |> (snd o Logic.dest_equals o Thm.prop_of)
   152       |> K conditional ? Logic.strip_imp_concl
   151       |> K conditional ? Logic.strip_imp_concl
   153       |> (abs_def o #2 o cert_def ctxt);
   152       |> (abs_def o #2 o cert_def ctxt);
   154     fun prove ctxt' t def =
   153     fun prove ctxt' t def =
   155       let
   154       let
   156         val thy' = ProofContext.theory_of ctxt';
       
   157         val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
   155         val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
   158         val frees = Term.fold_aterms (fn Free (x, _) =>
   156         val frees = Term.fold_aterms (fn Free (x, _) =>
   159           if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
   157           if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
   160       in
   158       in
   161         Goal.prove thy' frees [] prop' (K (ALLGOALS
   159         Goal.prove ctxt' frees [] prop' (K (ALLGOALS
   162           (meta_rewrite_tac ctxt' THEN'
   160           (meta_rewrite_tac ctxt' THEN'
   163             Tactic.rewrite_goal_tac [def] THEN'
   161             Tactic.rewrite_goal_tac [def] THEN'
   164             Tactic.resolve_tac [Drule.reflexive_thm])))
   162             Tactic.resolve_tac [Drule.reflexive_thm])))
   165         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   163         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   166       end;
   164       end;