src/HOL/Tools/coinduction.ML
changeset 60642 48dd1cefb4ae
parent 59971 ea06500bb092
child 60784 4f590c08fd5d
equal deleted inserted replaced
60641:f6e8293747fd 60642:48dd1cefb4ae
    59           val vars = raw_vars @ map (Thm.term_of o snd) params;
    59           val vars = raw_vars @ map (Thm.term_of o snd) params;
    60           val names_ctxt = ctxt
    60           val names_ctxt = ctxt
    61             |> fold Variable.declare_names vars
    61             |> fold Variable.declare_names vars
    62             |> fold Variable.declare_thm (raw_thm :: prems);
    62             |> fold Variable.declare_thm (raw_thm :: prems);
    63           val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    63           val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    64           val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    64           val (instT, inst) = Thm.match (thm_concl, concl);
    65             |>> map (apply2 Thm.typ_of)
    65           val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
    66             ||> map (apply2 Thm.term_of);
    66           val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
    67           val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    67           val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    68             |> map (subst_atomic_types rhoTs);
    68             |> map (subst_atomic_types rhoTs);
    69           val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    69           val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    70           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    70           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    71             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
    71             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
   158       "coinduction on types or predicates/sets");
   158       "coinduction on types or predicates/sets");
   159 
   159 
   160 end;
   160 end;
   161 
   161 
   162 end;
   162 end;
   163