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 + (* TODO: sanity checks on arguments *)
4.25 +
4.26 + val T as Type (T_name, _) = prep_typ lthy raw_T;
4.27 + val b = Binding.qualified_name T_name;
4.28 +
4.29 val ctors = map (prep_term lthy) raw_ctors;
4.30 + val ctor_Tss = map (binder_types o fastype_of) ctors;
4.31
4.32 - (* TODO: sanity checks on arguments *)
4.33 - val ctor_Tss = map (binder_types o fastype_of) ctors;
4.34 - val (ctor_argss, _) = lthy |>
4.35 - mk_Freess "x" ctor_Tss;
4.36 + val ((xss, yss), _) = lthy |>
4.37 + mk_Freess "x" ctor_Tss
4.38 + ||>> mk_Freess "y" ctor_Tss;
4.39
4.40 - val goal_distincts =
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"