src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 57302 58f02fbaa764
parent 57301 7b997028aaac
child 57303 498a62e65f5f
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -597,10 +597,47 @@
     1.4       (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
     1.5    end;
     1.6  
     1.7 -fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs ctr_sugars abs_inverses abs_injects
     1.8 +fun coinduct_attrs fpTs ctr_sugars mss =
     1.9 +  let
    1.10 +    val nn = length fpTs;
    1.11 +    val fp_b_names = map base_name_of_typ fpTs;
    1.12 +    val ctrss = map #ctrs ctr_sugars;
    1.13 +    val discss = map #discs ctr_sugars;
    1.14 +    fun mk_coinduct_concls ms discs ctrs =
    1.15 +      let
    1.16 +        fun mk_disc_concl disc = [name_of_disc disc];
    1.17 +        fun mk_ctr_concl 0 _ = []
    1.18 +          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
    1.19 +        val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
    1.20 +        val ctr_concls = map2 mk_ctr_concl ms ctrs;
    1.21 +      in
    1.22 +        flat (map2 append disc_concls ctr_concls)
    1.23 +      end;
    1.24 +    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
    1.25 +    val coinduct_conclss =
    1.26 +      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    1.27 +
    1.28 +    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    1.29 +    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
    1.30 +
    1.31 +    val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    1.32 +    val coinduct_case_concl_attrs =
    1.33 +      map2 (fn casex => fn concls =>
    1.34 +          Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    1.35 +        coinduct_cases coinduct_conclss;
    1.36 +
    1.37 +    val common_coinduct_attrs =
    1.38 +      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.39 +    val coinduct_attrs =
    1.40 +      coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.41 +  in
    1.42 +    (coinduct_attrs, common_coinduct_attrs)
    1.43 +  end;
    1.44 +
    1.45 +fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
    1.46    ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
    1.47    let
    1.48 -    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts
    1.49 +    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
    1.50  
    1.51      val (Rs, IRs, fpAs, fpBs, names_lthy) =
    1.52        let
    1.53 @@ -613,7 +650,8 @@
    1.54        in
    1.55          (Rs, IRs,
    1.56            map2 (curry Free) fpAs_names fpA_Ts,
    1.57 -          map2 (curry Free) fpBs_names fpB_Ts, names_lthy)
    1.58 +          map2 (curry Free) fpBs_names fpB_Ts,
    1.59 +          names_lthy)
    1.60        end;
    1.61  
    1.62      val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) =
    1.63 @@ -624,8 +662,8 @@
    1.64          fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts)))
    1.65            selsss);
    1.66        in
    1.67 -        ((mk_discss fpAs As, mk_selsss fpAs As)
    1.68 -        ,(mk_discss fpBs Bs, mk_selsss fpBs Bs))
    1.69 +        ((mk_discss fpAs As, mk_selsss fpAs As),
    1.70 +         (mk_discss fpBs Bs, mk_selsss fpBs Bs))
    1.71        end;
    1.72  
    1.73      fun choose_relator (A, B) = the (find_first (fn t =>
    1.74 @@ -664,23 +702,37 @@
    1.75          map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
    1.76        end;
    1.77  
    1.78 -      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.79 -        (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
    1.80 -
    1.81 -      fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
    1.82 +    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    1.83 +      (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
    1.84  
    1.85 -      (*
    1.86 -      val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
    1.87 -      val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
    1.88 -      val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
    1.89 -      *)
    1.90 -  in
    1.91 -    Goal.prove_sorry lthy [] premises goal
    1.92 +    (*
    1.93 +    fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
    1.94 +    val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
    1.95 +    val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
    1.96 +    val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
    1.97 +    *)
    1.98 +
    1.99 +    val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
   1.100        (fn {context = ctxt, prems = prems} =>
   1.101            mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
   1.102              (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss)
   1.103                ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses)
   1.104        |> singleton (Proof_Context.export names_lthy lthy)
   1.105 +      |> Thm.close_derivation;
   1.106 +
   1.107 +    val nn = length fpA_Ts;
   1.108 +    val predicate2D = @{thm predicate2D};
   1.109 +    val predicate2D_conj = @{thm predicate2D_conj};
   1.110 +
   1.111 +    val postproc =
   1.112 +      Drule.zero_var_indexes
   1.113 +      #> `(conj_dests nn)
   1.114 +      #>> map (fn thm => Thm.permute_prems 0 nn (thm RS predicate2D))
   1.115 +      ##> (fn thm => Thm.permute_prems 0 nn
   1.116 +        (if nn = 1 then thm RS predicate2D
   1.117 +         else funpow nn (fn thm => reassoc_conjs (thm RS predicate2D_conj)) thm));
   1.118 +  in
   1.119 +    (postproc rel_coinduct0_thm, coinduct_attrs fpA_Ts ctr_sugars mss)
   1.120    end;
   1.121  
   1.122  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
   1.123 @@ -752,12 +804,10 @@
   1.124              (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
   1.125            handle List.Empty => @{term True};
   1.126  
   1.127 -        (* Probably the good premise *)
   1.128          fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
   1.129            fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
   1.130              HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
   1.131  
   1.132 -        (* Make a new conclusion (e.g. rel_concl) *)
   1.133          val concl =
   1.134            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.135              (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   1.136 @@ -792,21 +842,6 @@
   1.137          map2 (postproc oo prove) dtor_coinducts goals
   1.138        end;
   1.139  
   1.140 -    fun mk_coinduct_concls ms discs ctrs =
   1.141 -      let
   1.142 -        fun mk_disc_concl disc = [name_of_disc disc];
   1.143 -        fun mk_ctr_concl 0 _ = []
   1.144 -          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
   1.145 -        val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
   1.146 -        val ctr_concls = map2 mk_ctr_concl ms ctrs;
   1.147 -      in
   1.148 -        flat (map2 append disc_concls ctr_concls)
   1.149 -      end;
   1.150 -
   1.151 -    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   1.152 -    val coinduct_conclss =
   1.153 -      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   1.154 -
   1.155      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   1.156  
   1.157      val gcorecs = map (lists_bmoc pgss) corecs;
   1.158 @@ -898,22 +933,8 @@
   1.159        map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
   1.160  
   1.161      val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
   1.162 -
   1.163 -    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   1.164 -    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   1.165 -
   1.166 -    val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   1.167 -    val coinduct_case_concl_attrs =
   1.168 -      map2 (fn casex => fn concls =>
   1.169 -          Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
   1.170 -        coinduct_cases coinduct_conclss;
   1.171 -
   1.172 -    val common_coinduct_attrs =
   1.173 -      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   1.174 -    val coinduct_attrs =
   1.175 -      coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   1.176    in
   1.177 -    ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
   1.178 +    ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss),
   1.179       (corec_thmss, code_nitpicksimp_attrs),
   1.180       (disc_corec_thmss, []),
   1.181       (disc_corec_iff_thmss, simp_attrs),
   1.182 @@ -1569,13 +1590,15 @@
   1.183              abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   1.184              (Proof_Context.export lthy' no_defs_lthy) lthy;
   1.185  
   1.186 -        val rel_coinduct0_thm = derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs ctr_sugars
   1.187 -           abs_inverses abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss
   1.188 -           rel_xtor_co_induct_thm;
   1.189 +        val ((rel_coinduct_thms, rel_coinduct_thm),
   1.190 +             (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
   1.191 +          derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects
   1.192 +          ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
   1.193  
   1.194          val sel_corec_thmss = map flat sel_corec_thmsss;
   1.195  
   1.196          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
   1.197 +        val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
   1.198  
   1.199          val flat_corec_thms = append oo append;
   1.200  
   1.201 @@ -1585,16 +1608,19 @@
   1.202              mapss rel_injectss rel_distinctss setss;
   1.203  
   1.204          val common_notes =
   1.205 -          (rel_coinductN ^ "0", [rel_coinduct0_thm], []) :: (if nn > 1 then
   1.206 -             [(coinductN, [coinduct_thm], common_coinduct_attrs),
   1.207 -              (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   1.208 -           else
   1.209 -             [])
   1.210 +          (if nn > 1 then
   1.211 +            [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs),
   1.212 +             (coinductN, [coinduct_thm], common_coinduct_attrs),
   1.213 +             (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   1.214 +          else
   1.215 +            [])
   1.216            |> massage_simple_notes fp_common_name;
   1.217  
   1.218          val notes =
   1.219            [(coinductN, map single coinduct_thms,
   1.220              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   1.221 +           (rel_coinductN, map single rel_coinduct_thms,
   1.222 +            K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
   1.223             (corecN, corec_thmss, K corec_attrs),
   1.224             (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
   1.225             (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),