src/HOL/Tools/coinduction.ML
changeset 59582 0fbed69ff081
parent 59580 cbc38731d42f
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/coinduction.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -24,15 +24,15 @@
     1.4  
     1.5  fun ALLGOALS_SKIP skip tac st =
     1.6    let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
     1.7 -  in doall (nprems_of st) st  end;
     1.8 +  in doall (Thm.nprems_of st) st  end;
     1.9  
    1.10  fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
    1.11    st |> (tac1 i THEN (fn st' =>
    1.12 -    Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
    1.13 +    Seq.INTERVAL tac2 (i + skip) (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
    1.14  
    1.15  fun DELETE_PREMS_AFTER skip tac i st =
    1.16    let
    1.17 -    val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    1.18 +    val n = nth (Thm.prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
    1.19    in
    1.20      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
    1.21    end;
    1.22 @@ -56,14 +56,14 @@
    1.23        Object_Logic.atomize_prems_tac ctxt THEN'
    1.24        DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
    1.25          let
    1.26 -          val vars = raw_vars @ map (term_of o snd) params;
    1.27 +          val vars = raw_vars @ map (Thm.term_of o snd) params;
    1.28            val names_ctxt = ctxt
    1.29              |> fold Variable.declare_names vars
    1.30              |> fold Variable.declare_thm (raw_thm :: prems);
    1.31            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    1.32            val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    1.33 -            |>> map (apply2 typ_of)
    1.34 -            ||> map (apply2 term_of);
    1.35 +            |>> map (apply2 Thm.typ_of)
    1.36 +            ||> map (apply2 Thm.term_of);
    1.37            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
    1.38              |> map (subst_atomic_types rhoTs);
    1.39            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
    1.40 @@ -73,7 +73,7 @@
    1.41              @{map 3} (fn name => fn T => fn (_, rhs) =>
    1.42                HOLogic.mk_eq (Free (name, T), rhs))
    1.43              names Ts raw_eqs;
    1.44 -          val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
    1.45 +          val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.46              |> try (Library.foldr1 HOLogic.mk_conj)
    1.47              |> the_default @{term True}
    1.48              |> Ctr_Sugar_Util.list_exists_free vars
    1.49 @@ -104,8 +104,9 @@
    1.50                         val inv_thms = init @ [last];
    1.51                         val eqs = take e inv_thms;
    1.52                         fun is_local_var t =
    1.53 -                         member (fn (t, (_, t')) => t aconv (term_of t')) params t;
    1.54 -                        val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
    1.55 +                         member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
    1.56 +                        val (eqs, assms') =
    1.57 +                          filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
    1.58                          val assms = assms' @ drop e inv_thms
    1.59                        in
    1.60                          HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
    1.61 @@ -114,7 +115,7 @@
    1.62          end) ctxt) THEN'
    1.63        K (prune_params_tac ctxt))
    1.64      #> Seq.maps (fn st =>
    1.65 -      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
    1.66 +      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
    1.67    end));
    1.68  
    1.69  local