countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
authorhuffman
Thu Sep 06 08:59:50 2012 -0700 (2012-09-06)
changeset 491876096da55d2d6
parent 49186 4b5fa9d5e330
child 49188 22f7e7b68f50
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
src/HOL/Library/Countable.thy
     1.1 --- a/src/HOL/Library/Countable.thy	Thu Sep 06 17:12:24 2012 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Sep 06 08:59:50 2012 -0700
     1.3 @@ -288,12 +288,17 @@
     1.4          val induct_thms = #inducts (snd induct_info)
     1.5          val alist = pred_names ~~ induct_thms
     1.6          val induct_thm = the (AList.lookup (op =) alist pred_name)
     1.7 +        val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
     1.8 +        val thy = Proof_Context.theory_of ctxt
     1.9 +        val insts = vars |> map (fn (_, T) => try (Thm.cterm_of thy)
    1.10 +          (Const (@{const_name Countable.finite_item}, T)))
    1.11 +        val induct_thm' = Drule.instantiate' [] insts induct_thm
    1.12          val rules = @{thms finite_item.intros}
    1.13        in
    1.14          SOLVED' (fn i => EVERY
    1.15            [rtac @{thm countable_datatype} i,
    1.16             rtac typedef_thm i,
    1.17 -           etac induct_thm i,
    1.18 +           etac induct_thm' i,
    1.19             REPEAT (resolve_tac rules i ORELSE atac i)]) 1
    1.20        end)
    1.21  *}