# HG changeset patch
# User traytel
# Date 1473792674 -7200
# Node ID d14e580c3b8fb69a2a7ee3cf4653fee9030ef040
# Parent  ce05cc93e07be03fa5a141827c189e4fd4db0bf6
don't expose internal construction in the coinduction rule for mutual coinductive predicates

diff -r ce05cc93e07b -r d14e580c3b8f src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Sep 13 16:23:12 2016 +0200
+++ b/src/HOL/Inductive.thy	Tue Sep 13 20:51:14 2016 +0200
@@ -369,6 +369,15 @@
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   Collect_mono in_mono vimage_mono
 
+lemma le_rel_bool_arg_iff: "X \<le> Y \<longleftrightarrow> X False \<le> Y False \<and> X True \<le> Y True"
+  unfolding le_fun_def le_bool_def using bool_induct by auto
+
+lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
+  by blast
+
+lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
+  by auto
+
 ML_file "Tools/inductive.ML"
 
 lemmas [mono] =
diff -r ce05cc93e07b -r d14e580c3b8f src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Sep 13 16:23:12 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Sep 13 20:51:14 2016 +0200
@@ -116,7 +116,9 @@
   map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1;
 
 val simp_thms3 =
-  map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
+  @{thms le_rel_bool_arg_iff if_False if_True conj_ac
+    le_fun_def le_bool_def sup_fun_def sup_bool_def simp_thms
+    if_bool_eq_disj all_simps ex_simps imp_conjL};
 
 
 
@@ -775,6 +777,119 @@
 
   in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
 
+(* prove coinduction rule *)
+
+fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
+fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
+
+fun prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono
+    fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
+  let
+    val _ = clean_message ctxt quiet_mode "  Proving the coinduction rule ...";
+    val n = length cs;
+    val (ns, xss) = map_split (fn pred =>
+      make_args' argTs xs (arg_types_of (length params) pred) |> `length) preds;
+    val xTss = map (map fastype_of) xss;
+    val (Rs_names, names_ctxt) = Variable.variant_fixes (mk_names "X" n) ctxt;
+    val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> @{typ bool})) Rs_names xTss;
+    val Rs_applied = map2 (curry list_comb) Rs xss;
+    val preds_applied = map2 (curry list_comb) (map (fn p => list_comb (p, params)) preds) xss;
+    val abstract_list = fold_rev (absfree o dest_Free);
+    val bss = map (make_bool_args
+      (fn b => HOLogic.mk_eq (b, @{term False}))
+      (fn b => HOLogic.mk_eq (b, @{term True})) bs) (0 upto n - 1);
+    val eq_undefinedss = map (fn ys => map (fn x =>
+        HOLogic.mk_eq (x, Const (@{const_name undefined}, fastype_of x)))
+      (subtract (op =) ys xs)) xss;
+    val R =
+      @{fold 3} (fn bs => fn eqs => fn R => fn t => if null bs andalso null eqs then R else
+        mk_If (Library.foldr1 HOLogic.mk_conj (bs @ eqs)) R t)
+      bss eq_undefinedss Rs_applied @{term False}
+      |> abstract_list (bs @ xs);
+
+    fun subst t =
+      (case dest_predicate cs params t of
+        SOME (_, i, ts, (_, Us)) =>
+          let
+            val l = length Us;
+            val bs = map Bound (l - 1 downto 0);
+            val args = map (incr_boundvars l) ts @ bs
+          in
+            HOLogic.mk_disj (list_comb (nth Rs i, args),
+              list_comb (nth preds i, params @ args))
+            |> fold_rev absdummy Us
+          end
+      | NONE =>
+          (case t of
+            t1 $ t2 => subst t1 $ subst t2
+          | Abs (x, T, u) => Abs (x, T, subst u)
+          | _ => t));
+
+    fun mk_coind_prem r =
+      let
+        val SOME (_, i, ts, (Ts, _)) =
+          dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
+        val ps =
+          map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
+          map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r);
+      in
+        (i, fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
+          (Logic.strip_params r)
+          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps))
+      end;
+
+    fun mk_prem i Ps = Logic.mk_implies
+        ((nth Rs_applied i, Library.foldr1 HOLogic.mk_disj Ps) |> @{apply 2} HOLogic.mk_Trueprop)
+      |> fold_rev Logic.all (nth xss i);
+
+    val prems = map mk_coind_prem intr_ts |> AList.group (op =) |> sort (int_ord o apply2 fst)
+      |> map (uncurry mk_prem);
+
+    val concl = @{map 3} (fn xs =>
+        Ctr_Sugar_Util.list_all_free xs oo curry HOLogic.mk_imp) xss Rs_applied preds_applied
+      |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
+
+
+    val pred_defs_sym = if null rec_preds_defs then [] else map2 (fn n => fn thm =>
+        funpow n (fn thm => thm RS @{thm meta_fun_cong}) thm RS @{thm Pure.symmetric})
+      ns rec_preds_defs;
+    val simps = simp_thms3 @ pred_defs_sym;
+    val simprocs = [Simplifier.the_simproc ctxt "HOL.defined_All"];
+    val simplify = asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt addsimprocs simprocs);
+    val coind = (mono RS (fp_def RS @{thm def_coinduct}))
+      |> infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt R)]
+      |> simplify;
+    fun idx_of t = find_index (fn R =>
+      R = the_single (subtract (op =) (preds @ params) (map Free (Term.add_frees t [])))) Rs;
+    val coind_concls = HOLogic.dest_Trueprop (Thm.concl_of coind) |> HOLogic.dest_conj
+      |> map (fn t => (idx_of t, t)) |> sort (int_ord o @{apply 2} fst) |> map snd;
+    val reorder_bound_goals = map_filter (fn (t, u) => if t aconv u then NONE else
+      SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))))
+      ((HOLogic.dest_Trueprop concl |> HOLogic.dest_conj) ~~ coind_concls);
+    val reorder_bound_thms = map (fn goal => Goal.prove_sorry ctxt [] [] goal
+      (fn {context = ctxt, prems = _} =>
+        HEADGOAL (EVERY' [resolve_tac ctxt [iffI],
+          REPEAT_DETERM o resolve_tac ctxt [allI, impI],
+          REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt,
+          REPEAT_DETERM o resolve_tac ctxt [allI, impI],
+          REPEAT_DETERM o dresolve_tac ctxt [spec], eresolve_tac ctxt [mp], assume_tac ctxt])))
+      reorder_bound_goals;
+    val coinduction = Goal.prove_sorry ctxt [] prems concl (fn {context = ctxt, prems = CIH} =>
+      HEADGOAL (full_simp_tac
+        (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt addsimprocs simprocs) THEN'
+        resolve_tac ctxt [coind]) THEN
+      ALLGOALS (REPEAT_ALL_NEW (REPEAT_DETERM o resolve_tac ctxt [allI, impI, conjI] THEN'
+        REPEAT_DETERM o eresolve_tac ctxt [exE, conjE] THEN'
+        dresolve_tac ctxt (map simplify CIH) THEN'
+        REPEAT_DETERM o (assume_tac ctxt ORELSE'
+          eresolve_tac ctxt [conjE] ORELSE' dresolve_tac ctxt [spec, mp]))))
+  in
+    coinduction
+    |> length cs = 1 ? (Object_Logic.rulify ctxt #> rotate_prems ~1)
+    |> singleton (Proof_Context.export names_ctxt ctxt''')
+  end
+
+
 
 
 (** specification of (co)inductive predicates **)
@@ -990,14 +1105,12 @@
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl
        else if coind then
-         singleton (Proof_Context.export lthy2 lthy1)
-           (rotate_prems ~1 (Object_Logic.rulify lthy2
-             (fold_rule lthy2 rec_preds_defs
-               (rewrite_rule lthy2 simp_thms3
-                (mono RS (fp_def RS @{thm def_coinduct}))))))
+         prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono fp_def
+           rec_preds_defs lthy2 lthy1
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs lthy2 lthy1);
+
     val eqs =
       if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1;