generate proper attributes for coinduction rules
authorblanchet
Thu Apr 25 17:13:24 2013 +0200 (2013-04-25)
changeset 5177748a0ae342ea0
parent 51776 8ea64fb16bae
child 51778 190f89980f7b
generate proper attributes for coinduction rules
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 13:22:45 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 17:13:24 2013 +0200
     1.3 @@ -31,7 +31,9 @@
     1.4  open BNF_FP
     1.5  open BNF_FP_Def_Sugar_Tactics
     1.6  
     1.7 -(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A") *)
     1.8 +val EqN = "Eq";
     1.9 +
    1.10 +(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.11  fun quasi_unambiguous_case_names names =
    1.12    let
    1.13      val ps = map (`Long_Name.base_name) names;
    1.14 @@ -987,6 +989,21 @@
    1.15              (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
    1.16            end;
    1.17  
    1.18 +        fun mk_coinduct_concls ms discs ctrs =
    1.19 +          let
    1.20 +            fun mk_disc_concl disc = [name_of_disc disc];
    1.21 +            fun mk_ctr_concl 0 _ = []
    1.22 +              | mk_ctr_concl _ ctor = [name_of_ctr ctor];
    1.23 +            val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
    1.24 +            val ctr_concls = map2 mk_ctr_concl ms ctrs;
    1.25 +          in
    1.26 +            flat (map2 append disc_concls ctr_concls)
    1.27 +          end;
    1.28 +
    1.29 +        val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
    1.30 +        val coinduct_conclss =
    1.31 +          map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    1.32 +
    1.33          fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
    1.34  
    1.35          val gunfolds = map (lists_bmoc pgss) unfolds;
    1.36 @@ -1133,18 +1150,26 @@
    1.37            [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
    1.38            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.39  
    1.40 +        val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    1.41 +        val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    1.42 +        val coinduct_case_concl_attrs =
    1.43 +          map2 (fn casex => fn concls =>
    1.44 +              Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    1.45 +            coinduct_cases coinduct_conclss;
    1.46 +        val coinduct_case_attrs =
    1.47 +          coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.48 +
    1.49          val common_notes =
    1.50            (if nn > 1 then
    1.51 -             (* FIXME: attribs *)
    1.52 -             [(coinductN, [coinduct_thm], []),
    1.53 -              (strong_coinductN, [strong_coinduct_thm], [])]
    1.54 +             [(coinductN, [coinduct_thm], coinduct_case_attrs),
    1.55 +              (strong_coinductN, [strong_coinduct_thm], coinduct_case_attrs)]
    1.56             else
    1.57               [])
    1.58            |> map (fn (thmN, thms, attrs) =>
    1.59              ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.60  
    1.61          val notes =
    1.62 -          [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
    1.63 +          [(coinductN, map single coinduct_thms, coinduct_case_attrs),
    1.64             (corecN, corec_thmss, []),
    1.65             (disc_corecN, disc_corec_thmss, simp_attrs),
    1.66             (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
    1.67 @@ -1153,7 +1178,7 @@
    1.68             (sel_corecN, sel_corec_thmss, simp_attrs),
    1.69             (sel_unfoldN, sel_unfold_thmss, simp_attrs),
    1.70             (simpsN, simp_thmss, []),
    1.71 -           (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
    1.72 +           (strong_coinductN, map single strong_coinduct_thms, coinduct_case_attrs),
    1.73             (unfoldN, unfold_thmss, [])]
    1.74            |> maps (fn (thmN, thmss, attrs) =>
    1.75              map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>
     2.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 13:22:45 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 17:13:24 2013 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    val mk_disc_or_sel: typ list -> term -> term
     2.5  
     2.6    val name_of_ctr: term -> string
     2.7 +  val name_of_disc: term -> string
     2.8  
     2.9    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    2.10      (((bool * bool) * term list) * term) *
    2.11 @@ -96,11 +97,27 @@
    2.12      Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
    2.13    end;
    2.14  
    2.15 -fun name_of_ctr c =
    2.16 -  (case head_of c of
    2.17 +fun name_of_const what t =
    2.18 +  (case head_of t of
    2.19      Const (s, _) => s
    2.20    | Free (s, _) => s
    2.21 -  | _ => error "Cannot extract name of constructor");
    2.22 +  | _ => error ("Cannot extract name of " ^ what));
    2.23 +
    2.24 +val name_of_ctr = name_of_const "constructor";
    2.25 +
    2.26 +val notN = "not_";
    2.27 +val eqN = "eq_";
    2.28 +val neqN = "neq_";
    2.29 +
    2.30 +fun name_of_disc t =
    2.31 +  (case head_of t of
    2.32 +    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
    2.33 +    Long_Name.map_base_name (prefix notN) (name_of_disc t')
    2.34 +  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
    2.35 +    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
    2.36 +  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
    2.37 +    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
    2.38 +  | t' => name_of_const "destructor" t');
    2.39  
    2.40  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
    2.41  
    2.42 @@ -200,7 +217,6 @@
    2.43      val xgs = map2 (curry Term.list_comb) gs xss;
    2.44  
    2.45      val fcase = Term.list_comb (casex, fs);
    2.46 -    val gcase = Term.list_comb (casex, gs);
    2.47  
    2.48      val ufcase = fcase $ u;
    2.49      val vfcase = fcase $ v;