don't expose internal construction in the coinduction rule for mutual coinductive predicates
authortraytel
Tue Sep 13 20:51:14 2016 +0200 (2016-09-13)
changeset 63863d14e580c3b8f
parent 63862 ce05cc93e07b
child 63864 159882dbb339
child 63865 ccac33e291b1
don't expose internal construction in the coinduction rule for mutual coinductive predicates
src/HOL/Inductive.thy
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 13 16:23:12 2016 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 13 20:51:14 2016 +0200
     1.3 @@ -369,6 +369,15 @@
     1.4    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     1.5    Collect_mono in_mono vimage_mono
     1.6  
     1.7 +lemma le_rel_bool_arg_iff: "X \<le> Y \<longleftrightarrow> X False \<le> Y False \<and> X True \<le> Y True"
     1.8 +  unfolding le_fun_def le_bool_def using bool_induct by auto
     1.9 +
    1.10 +lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
    1.11 +  by blast
    1.12 +
    1.13 +lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
    1.14 +  by auto
    1.15 +
    1.16  ML_file "Tools/inductive.ML"
    1.17  
    1.18  lemmas [mono] =
     2.1 --- a/src/HOL/Tools/inductive.ML	Tue Sep 13 16:23:12 2016 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Tue Sep 13 20:51:14 2016 +0200
     2.3 @@ -116,7 +116,9 @@
     2.4    map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1;
     2.5  
     2.6  val simp_thms3 =
     2.7 -  map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
     2.8 +  @{thms le_rel_bool_arg_iff if_False if_True conj_ac
     2.9 +    le_fun_def le_bool_def sup_fun_def sup_bool_def simp_thms
    2.10 +    if_bool_eq_disj all_simps ex_simps imp_conjL};
    2.11  
    2.12  
    2.13  
    2.14 @@ -775,6 +777,119 @@
    2.15  
    2.16    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
    2.17  
    2.18 +(* prove coinduction rule *)
    2.19 +
    2.20 +fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
    2.21 +fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
    2.22 +
    2.23 +fun prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono
    2.24 +    fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
    2.25 +  let
    2.26 +    val _ = clean_message ctxt quiet_mode "  Proving the coinduction rule ...";
    2.27 +    val n = length cs;
    2.28 +    val (ns, xss) = map_split (fn pred =>
    2.29 +      make_args' argTs xs (arg_types_of (length params) pred) |> `length) preds;
    2.30 +    val xTss = map (map fastype_of) xss;
    2.31 +    val (Rs_names, names_ctxt) = Variable.variant_fixes (mk_names "X" n) ctxt;
    2.32 +    val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> @{typ bool})) Rs_names xTss;
    2.33 +    val Rs_applied = map2 (curry list_comb) Rs xss;
    2.34 +    val preds_applied = map2 (curry list_comb) (map (fn p => list_comb (p, params)) preds) xss;
    2.35 +    val abstract_list = fold_rev (absfree o dest_Free);
    2.36 +    val bss = map (make_bool_args
    2.37 +      (fn b => HOLogic.mk_eq (b, @{term False}))
    2.38 +      (fn b => HOLogic.mk_eq (b, @{term True})) bs) (0 upto n - 1);
    2.39 +    val eq_undefinedss = map (fn ys => map (fn x =>
    2.40 +        HOLogic.mk_eq (x, Const (@{const_name undefined}, fastype_of x)))
    2.41 +      (subtract (op =) ys xs)) xss;
    2.42 +    val R =
    2.43 +      @{fold 3} (fn bs => fn eqs => fn R => fn t => if null bs andalso null eqs then R else
    2.44 +        mk_If (Library.foldr1 HOLogic.mk_conj (bs @ eqs)) R t)
    2.45 +      bss eq_undefinedss Rs_applied @{term False}
    2.46 +      |> abstract_list (bs @ xs);
    2.47 +
    2.48 +    fun subst t =
    2.49 +      (case dest_predicate cs params t of
    2.50 +        SOME (_, i, ts, (_, Us)) =>
    2.51 +          let
    2.52 +            val l = length Us;
    2.53 +            val bs = map Bound (l - 1 downto 0);
    2.54 +            val args = map (incr_boundvars l) ts @ bs
    2.55 +          in
    2.56 +            HOLogic.mk_disj (list_comb (nth Rs i, args),
    2.57 +              list_comb (nth preds i, params @ args))
    2.58 +            |> fold_rev absdummy Us
    2.59 +          end
    2.60 +      | NONE =>
    2.61 +          (case t of
    2.62 +            t1 $ t2 => subst t1 $ subst t2
    2.63 +          | Abs (x, T, u) => Abs (x, T, subst u)
    2.64 +          | _ => t));
    2.65 +
    2.66 +    fun mk_coind_prem r =
    2.67 +      let
    2.68 +        val SOME (_, i, ts, (Ts, _)) =
    2.69 +          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
    2.70 +        val ps =
    2.71 +          map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
    2.72 +          map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r);
    2.73 +      in
    2.74 +        (i, fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
    2.75 +          (Logic.strip_params r)
    2.76 +          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps))
    2.77 +      end;
    2.78 +
    2.79 +    fun mk_prem i Ps = Logic.mk_implies
    2.80 +        ((nth Rs_applied i, Library.foldr1 HOLogic.mk_disj Ps) |> @{apply 2} HOLogic.mk_Trueprop)
    2.81 +      |> fold_rev Logic.all (nth xss i);
    2.82 +
    2.83 +    val prems = map mk_coind_prem intr_ts |> AList.group (op =) |> sort (int_ord o apply2 fst)
    2.84 +      |> map (uncurry mk_prem);
    2.85 +
    2.86 +    val concl = @{map 3} (fn xs =>
    2.87 +        Ctr_Sugar_Util.list_all_free xs oo curry HOLogic.mk_imp) xss Rs_applied preds_applied
    2.88 +      |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
    2.89 +
    2.90 +
    2.91 +    val pred_defs_sym = if null rec_preds_defs then [] else map2 (fn n => fn thm =>
    2.92 +        funpow n (fn thm => thm RS @{thm meta_fun_cong}) thm RS @{thm Pure.symmetric})
    2.93 +      ns rec_preds_defs;
    2.94 +    val simps = simp_thms3 @ pred_defs_sym;
    2.95 +    val simprocs = [Simplifier.the_simproc ctxt "HOL.defined_All"];
    2.96 +    val simplify = asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt addsimprocs simprocs);
    2.97 +    val coind = (mono RS (fp_def RS @{thm def_coinduct}))
    2.98 +      |> infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt R)]
    2.99 +      |> simplify;
   2.100 +    fun idx_of t = find_index (fn R =>
   2.101 +      R = the_single (subtract (op =) (preds @ params) (map Free (Term.add_frees t [])))) Rs;
   2.102 +    val coind_concls = HOLogic.dest_Trueprop (Thm.concl_of coind) |> HOLogic.dest_conj
   2.103 +      |> map (fn t => (idx_of t, t)) |> sort (int_ord o @{apply 2} fst) |> map snd;
   2.104 +    val reorder_bound_goals = map_filter (fn (t, u) => if t aconv u then NONE else
   2.105 +      SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))))
   2.106 +      ((HOLogic.dest_Trueprop concl |> HOLogic.dest_conj) ~~ coind_concls);
   2.107 +    val reorder_bound_thms = map (fn goal => Goal.prove_sorry ctxt [] [] goal
   2.108 +      (fn {context = ctxt, prems = _} =>
   2.109 +        HEADGOAL (EVERY' [resolve_tac ctxt [iffI],
   2.110 +          REPEAT_DETERM o resolve_tac ctxt [allI, impI],
   2.111 +          REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt,
   2.112 +          REPEAT_DETERM o resolve_tac ctxt [allI, impI],
   2.113 +          REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt])))
   2.114 +      reorder_bound_goals;
   2.115 +    val coinduction = Goal.prove_sorry ctxt [] prems concl (fn {context = ctxt, prems = CIH} =>
   2.116 +      HEADGOAL (full_simp_tac
   2.117 +        (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt addsimprocs simprocs) THEN'
   2.118 +        resolve_tac ctxt [coind]) THEN
   2.119 +      ALLGOALS (REPEAT_ALL_NEW (REPEAT_DETERM o resolve_tac ctxt [allI, impI, conjI] THEN'
   2.120 +        REPEAT_DETERM o eresolve_tac ctxt [exE, conjE] THEN'
   2.121 +        dresolve_tac ctxt (map simplify CIH) THEN'
   2.122 +        REPEAT_DETERM o (assume_tac ctxt ORELSE'
   2.123 +          eresolve_tac ctxt [conjE] ORELSE' dresolve_tac ctxt [spec, mp]))))
   2.124 +  in
   2.125 +    coinduction
   2.126 +    |> length cs = 1 ? (Object_Logic.rulify ctxt #> rotate_prems ~1)
   2.127 +    |> singleton (Proof_Context.export names_ctxt ctxt''')
   2.128 +  end
   2.129 +
   2.130 +
   2.131  
   2.132  
   2.133  (** specification of (co)inductive predicates **)
   2.134 @@ -990,14 +1105,12 @@
   2.135      val raw_induct = zero_var_indexes
   2.136        (if no_ind then Drule.asm_rl
   2.137         else if coind then
   2.138 -         singleton (Proof_Context.export lthy2 lthy1)
   2.139 -           (rotate_prems ~1 (Object_Logic.rulify lthy2
   2.140 -             (fold_rule lthy2 rec_preds_defs
   2.141 -               (rewrite_rule lthy2 simp_thms3
   2.142 -                (mono RS (fp_def RS @{thm def_coinduct}))))))
   2.143 +         prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono fp_def
   2.144 +           rec_preds_defs lthy2 lthy1
   2.145         else
   2.146           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   2.147             rec_preds_defs lthy2 lthy1);
   2.148 +
   2.149      val eqs =
   2.150        if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1;
   2.151