src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
changeset 54247 81ee85f56e2d
parent 54229 ca638d713ff8
child 55379 9701dbc35f86
equal deleted inserted replaced
54246:8fdb4dc08ed1 54247:81ee85f56e2d
   278             val names = Term.add_free_names rhs []
   278             val names = Term.add_free_names rhs []
   279           in flatten thy lookup_pred rhs (names, [])
   279           in flatten thy lookup_pred rhs (names, [])
   280             |> map (fn (resultt, (_, prems)) =>
   280             |> map (fn (resultt, (_, prems)) =>
   281               Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
   281               Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
   282           end
   282           end
   283       val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
   283       val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
   284       val (intrs, thy') = thy
   284       val (intrs, thy') = thy
   285         |> Sign.add_consts_i
   285         |> Sign.add_consts_i
   286           (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
   286           (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
   287            dst_preds)
   287            dst_preds)
   288         |> fold_map Specification.axiom
   288         |> fold_map Specification.axiom
   289             (map_index (fn (j, (predname, t)) =>
   289             (map_index (fn (j, (predname, t)) =>
   290                 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
   290                 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
   291               (prednames ~~ intr_ts))
   291               (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
   292       val specs = map (fn predname => (predname,
   292       val specs = map (fn predname => (predname,
   293           map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
   293           map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
   294         dst_prednames
   294         dst_prednames
   295       val thy'' = Fun_Pred.map
   295       val thy'' = Fun_Pred.map
   296         (fold Item_Net.update (map (pairself Logic.varify_global)
   296         (fold Item_Net.update (map (pairself Logic.varify_global)