more work on BNF sugar
authorblanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30)
changeset 49019fc4decdba5ce
parent 49018 b2884253b421
child 49020 f379cf5d71bd
more work on BNF sugar
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_sugar.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -68,7 +68,6 @@
     1.4  
     1.5  val bdTN = "bdT";
     1.6  
     1.7 -val compN = "comp_"
     1.8  fun mk_killN n = "kill" ^ string_of_int n ^ "_";
     1.9  fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
    1.10  fun mk_permuteN src dest =
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
     2.3 @@ -528,7 +528,7 @@
     2.4  
     2.5  (* Define new BNFs *)
     2.6  
     2.7 -fun prepare_bnf const_policy mk_fact_policy qualify prep_term Ds_opt
     2.8 +fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
     2.9    ((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits) no_defs_lthy =
    2.10    let
    2.11      val fact_policy = mk_fact_policy no_defs_lthy;
    2.12 @@ -1167,14 +1167,14 @@
    2.13    in
    2.14      (map2 (Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs))
    2.15      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    2.16 -  end) oo prepare_bnf const_policy fact_policy qualify
    2.17 +  end) oo prepare_def const_policy fact_policy qualify
    2.18    (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
    2.19  
    2.20  val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    2.21    Proof.unfolding ([[(defs, [])]])
    2.22      (Proof.theorem NONE (snd oo after_qed)
    2.23        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    2.24 -  prepare_bnf Do_Inline user_policy I Syntax.read_term NONE;
    2.25 +  prepare_def Do_Inline user_policy I Syntax.read_term NONE;
    2.26  
    2.27  fun print_bnfs ctxt =
    2.28    let
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Aug 30 09:47:46 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Aug 30 09:47:46 2012 +0200
     3.3 @@ -30,6 +30,7 @@
     3.4    val hsetN: string
     3.5    val hset_recN: string
     3.6    val inductN: string
     3.7 +  val injectN: string
     3.8    val isNodeN: string
     3.9    val iterN: string
    3.10    val iter_uniqueN: string
    3.11 @@ -154,7 +155,8 @@
    3.12  val fld_unfN = fldN ^ "_" ^ unfN
    3.13  val unf_fldN = unfN ^ "_" ^ fldN
    3.14  fun mk_nchotomyN s = s ^ "_nchotomy"
    3.15 -fun mk_injectN s = s ^ "_inject"
    3.16 +val injectN = "inject"
    3.17 +fun mk_injectN s = s ^ "_" ^ injectN
    3.18  fun mk_exhaustN s = s ^ "_exhaust"
    3.19  val fld_injectN = mk_injectN fldN
    3.20  val fld_exhaustN = mk_exhaustN fldN
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 09:47:46 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 09:47:46 2012 +0200
     4.3 @@ -7,43 +7,76 @@
     4.4  
     4.5  signature BNF_SUGAR =
     4.6  sig
     4.7 -  val prepare_sugar : (Proof.context -> 'b -> term) ->
     4.8 -    (((typ * 'b list) * binding list) * binding list list) * 'b -> local_theory ->
     4.9 -    term list * local_theory
    4.10  end;
    4.11  
    4.12  structure BNF_Sugar : BNF_SUGAR =
    4.13  struct
    4.14  
    4.15  open BNF_Util
    4.16 +open BNF_FP_Util
    4.17  
    4.18 -fun prepare_sugar prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) lthy =
    4.19 +val distinctN = "distinct";
    4.20 +
    4.21 +fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur)
    4.22 +  lthy =
    4.23    let
    4.24 -    val ctors = map (prep_term lthy) raw_ctors;
    4.25 +    (* TODO: sanity checks on arguments *)
    4.26  
    4.27 -    (* TODO: sanity checks on arguments *)
    4.28 +    val T as Type (T_name, _) = prep_typ lthy raw_T;
    4.29 +    val b = Binding.qualified_name T_name;
    4.30 +
    4.31 +    val ctors = map (prep_term lthy) raw_ctors;
    4.32      val ctor_Tss = map (binder_types o fastype_of) ctors;
    4.33 -    val (ctor_argss, _) = lthy |>
    4.34 -      mk_Freess "x" ctor_Tss;
    4.35  
    4.36 -    val goal_distincts =
    4.37 +    val ((xss, yss), _) = lthy |>
    4.38 +      mk_Freess "x" ctor_Tss
    4.39 +      ||>> mk_Freess "y" ctor_Tss;
    4.40 +
    4.41 +    val goal_injects =
    4.42        let
    4.43 -        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)))
    4.44 -        fun mk_goals [] = []
    4.45 -          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts)
    4.46 +        fun mk_goal _ [] [] = NONE
    4.47 +          | mk_goal ctor xs ys =
    4.48 +            SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq
    4.49 +              (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)),
    4.50 +               Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))));
    4.51        in
    4.52 -        mk_goals (map2 (curry Term.list_comb) ctors ctor_argss)
    4.53 +        map_filter I (map3 mk_goal ctors xss yss)
    4.54        end;
    4.55  
    4.56 -    val goals = goal_distincts;
    4.57 +    val goal_half_distincts =
    4.58 +      let
    4.59 +        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)));
    4.60 +        fun mk_goals [] = []
    4.61 +          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts);
    4.62 +      in
    4.63 +        mk_goals (map2 (curry Term.list_comb) ctors xss)
    4.64 +      end;
    4.65 +
    4.66 +    val goals = [goal_injects, goal_half_distincts];
    4.67 +
    4.68 +    fun after_qed thmss lthy =
    4.69 +      let
    4.70 +        val [inject_thms, half_distinct_thms] = thmss;
    4.71 +
    4.72 +        val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
    4.73 +
    4.74 +        fun note thmN thms =
    4.75 +          snd o Local_Theory.note
    4.76 +            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
    4.77 +      in
    4.78 +        lthy
    4.79 +        |> note injectN inject_thms
    4.80 +        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
    4.81 +      end;
    4.82    in
    4.83 -    (goals, lthy)
    4.84 +    (goals, after_qed, lthy)
    4.85    end;
    4.86  
    4.87  val parse_binding_list = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
    4.88  
    4.89 -val bnf_sugar_cmd = (fn (goals, lthy) =>
    4.90 -  Proof.theorem NONE (K I) (map (single o rpair []) goals) lthy) oo prepare_sugar Syntax.read_term;
    4.91 +val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
    4.92 +  Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
    4.93 +  prepare_sugar Syntax.read_typ Syntax.read_term;
    4.94  
    4.95  val _ =
    4.96    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"