generate 'rel_coinduct' theorem for codatatypes
authordesharna
Tue Jun 24 13:48:14 2014 +0200 (2014-06-24)
changeset 5730258f02fbaa764
parent 57301 7b997028aaac
child 57303 498a62e65f5f
generate 'rel_coinduct' theorem for codatatypes
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     1.5  by auto
     1.6  
     1.7 +lemma predicate2D_conj: "(P \<le> Q) \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
     1.8 +  by auto
     1.9 +
    1.10  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
    1.11  by blast
    1.12  
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     2.3 @@ -597,10 +597,47 @@
     2.4       (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
     2.5    end;
     2.6  
     2.7 -fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs ctr_sugars abs_inverses abs_injects
     2.8 +fun coinduct_attrs fpTs ctr_sugars mss =
     2.9 +  let
    2.10 +    val nn = length fpTs;
    2.11 +    val fp_b_names = map base_name_of_typ fpTs;
    2.12 +    val ctrss = map #ctrs ctr_sugars;
    2.13 +    val discss = map #discs ctr_sugars;
    2.14 +    fun mk_coinduct_concls ms discs ctrs =
    2.15 +      let
    2.16 +        fun mk_disc_concl disc = [name_of_disc disc];
    2.17 +        fun mk_ctr_concl 0 _ = []
    2.18 +          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
    2.19 +        val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
    2.20 +        val ctr_concls = map2 mk_ctr_concl ms ctrs;
    2.21 +      in
    2.22 +        flat (map2 append disc_concls ctr_concls)
    2.23 +      end;
    2.24 +    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
    2.25 +    val coinduct_conclss =
    2.26 +      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    2.27 +
    2.28 +    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    2.29 +    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
    2.30 +
    2.31 +    val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    2.32 +    val coinduct_case_concl_attrs =
    2.33 +      map2 (fn casex => fn concls =>
    2.34 +          Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    2.35 +        coinduct_cases coinduct_conclss;
    2.36 +
    2.37 +    val common_coinduct_attrs =
    2.38 +      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    2.39 +    val coinduct_attrs =
    2.40 +      coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    2.41 +  in
    2.42 +    (coinduct_attrs, common_coinduct_attrs)
    2.43 +  end;
    2.44 +
    2.45 +fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
    2.46    ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
    2.47    let
    2.48 -    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts
    2.49 +    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
    2.50  
    2.51      val (Rs, IRs, fpAs, fpBs, names_lthy) =
    2.52        let
    2.53 @@ -613,7 +650,8 @@
    2.54        in
    2.55          (Rs, IRs,
    2.56            map2 (curry Free) fpAs_names fpA_Ts,
    2.57 -          map2 (curry Free) fpBs_names fpB_Ts, names_lthy)
    2.58 +          map2 (curry Free) fpBs_names fpB_Ts,
    2.59 +          names_lthy)
    2.60        end;
    2.61  
    2.62      val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) =
    2.63 @@ -624,8 +662,8 @@
    2.64          fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts)))
    2.65            selsss);
    2.66        in
    2.67 -        ((mk_discss fpAs As, mk_selsss fpAs As)
    2.68 -        ,(mk_discss fpBs Bs, mk_selsss fpBs Bs))
    2.69 +        ((mk_discss fpAs As, mk_selsss fpAs As),
    2.70 +         (mk_discss fpBs Bs, mk_selsss fpBs Bs))
    2.71        end;
    2.72  
    2.73      fun choose_relator (A, B) = the (find_first (fn t =>
    2.74 @@ -664,23 +702,37 @@
    2.75          map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
    2.76        end;
    2.77  
    2.78 -      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    2.79 -        (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
    2.80 -
    2.81 -      fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
    2.82 +    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    2.83 +      (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
    2.84  
    2.85 -      (*
    2.86 -      val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
    2.87 -      val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
    2.88 -      val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
    2.89 -      *)
    2.90 -  in
    2.91 -    Goal.prove_sorry lthy [] premises goal
    2.92 +    (*
    2.93 +    fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
    2.94 +    val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
    2.95 +    val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
    2.96 +    val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
    2.97 +    *)
    2.98 +
    2.99 +    val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
   2.100        (fn {context = ctxt, prems = prems} =>
   2.101            mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
   2.102              (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss)
   2.103                ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses)
   2.104        |> singleton (Proof_Context.export names_lthy lthy)
   2.105 +      |> Thm.close_derivation;
   2.106 +
   2.107 +    val nn = length fpA_Ts;
   2.108 +    val predicate2D = @{thm predicate2D};
   2.109 +    val predicate2D_conj = @{thm predicate2D_conj};
   2.110 +
   2.111 +    val postproc =
   2.112 +      Drule.zero_var_indexes
   2.113 +      #> `(conj_dests nn)
   2.114 +      #>> map (fn thm => Thm.permute_prems 0 nn (thm RS predicate2D))
   2.115 +      ##> (fn thm => Thm.permute_prems 0 nn
   2.116 +        (if nn = 1 then thm RS predicate2D
   2.117 +         else funpow nn (fn thm => reassoc_conjs (thm RS predicate2D_conj)) thm));
   2.118 +  in
   2.119 +    (postproc rel_coinduct0_thm, coinduct_attrs fpA_Ts ctr_sugars mss)
   2.120    end;
   2.121  
   2.122  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
   2.123 @@ -752,12 +804,10 @@
   2.124              (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
   2.125            handle List.Empty => @{term True};
   2.126  
   2.127 -        (* Probably the good premise *)
   2.128          fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
   2.129            fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
   2.130              HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
   2.131  
   2.132 -        (* Make a new conclusion (e.g. rel_concl) *)
   2.133          val concl =
   2.134            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   2.135              (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   2.136 @@ -792,21 +842,6 @@
   2.137          map2 (postproc oo prove) dtor_coinducts goals
   2.138        end;
   2.139  
   2.140 -    fun mk_coinduct_concls ms discs ctrs =
   2.141 -      let
   2.142 -        fun mk_disc_concl disc = [name_of_disc disc];
   2.143 -        fun mk_ctr_concl 0 _ = []
   2.144 -          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
   2.145 -        val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
   2.146 -        val ctr_concls = map2 mk_ctr_concl ms ctrs;
   2.147 -      in
   2.148 -        flat (map2 append disc_concls ctr_concls)
   2.149 -      end;
   2.150 -
   2.151 -    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   2.152 -    val coinduct_conclss =
   2.153 -      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   2.154 -
   2.155      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   2.156  
   2.157      val gcorecs = map (lists_bmoc pgss) corecs;
   2.158 @@ -898,22 +933,8 @@
   2.159        map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
   2.160  
   2.161      val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
   2.162 -
   2.163 -    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   2.164 -    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   2.165 -
   2.166 -    val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   2.167 -    val coinduct_case_concl_attrs =
   2.168 -      map2 (fn casex => fn concls =>
   2.169 -          Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
   2.170 -        coinduct_cases coinduct_conclss;
   2.171 -
   2.172 -    val common_coinduct_attrs =
   2.173 -      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   2.174 -    val coinduct_attrs =
   2.175 -      coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   2.176    in
   2.177 -    ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
   2.178 +    ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss),
   2.179       (corec_thmss, code_nitpicksimp_attrs),
   2.180       (disc_corec_thmss, []),
   2.181       (disc_corec_iff_thmss, simp_attrs),
   2.182 @@ -1569,13 +1590,15 @@
   2.183              abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   2.184              (Proof_Context.export lthy' no_defs_lthy) lthy;
   2.185  
   2.186 -        val rel_coinduct0_thm = derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs ctr_sugars
   2.187 -           abs_inverses abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss
   2.188 -           rel_xtor_co_induct_thm;
   2.189 +        val ((rel_coinduct_thms, rel_coinduct_thm),
   2.190 +             (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
   2.191 +          derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects
   2.192 +          ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
   2.193  
   2.194          val sel_corec_thmss = map flat sel_corec_thmsss;
   2.195  
   2.196          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
   2.197 +        val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
   2.198  
   2.199          val flat_corec_thms = append oo append;
   2.200  
   2.201 @@ -1585,16 +1608,19 @@
   2.202              mapss rel_injectss rel_distinctss setss;
   2.203  
   2.204          val common_notes =
   2.205 -          (rel_coinductN ^ "0", [rel_coinduct0_thm], []) :: (if nn > 1 then
   2.206 -             [(coinductN, [coinduct_thm], common_coinduct_attrs),
   2.207 -              (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   2.208 -           else
   2.209 -             [])
   2.210 +          (if nn > 1 then
   2.211 +            [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs),
   2.212 +             (coinductN, [coinduct_thm], common_coinduct_attrs),
   2.213 +             (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   2.214 +          else
   2.215 +            [])
   2.216            |> massage_simple_notes fp_common_name;
   2.217  
   2.218          val notes =
   2.219            [(coinductN, map single coinduct_thms,
   2.220              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   2.221 +           (rel_coinductN, map single rel_coinduct_thms,
   2.222 +            K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
   2.223             (corecN, corec_thmss, K corec_attrs),
   2.224             (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
   2.225             (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),