5 Sugar on top of a BNF. |
5 Sugar on top of a BNF. |
6 *) |
6 *) |
7 |
7 |
8 signature BNF_SUGAR = |
8 signature BNF_SUGAR = |
9 sig |
9 sig |
10 val prepare_sugar : (Proof.context -> 'b -> term) -> |
|
11 (((typ * 'b list) * binding list) * binding list list) * 'b -> local_theory -> |
|
12 term list * local_theory |
|
13 end; |
10 end; |
14 |
11 |
15 structure BNF_Sugar : BNF_SUGAR = |
12 structure BNF_Sugar : BNF_SUGAR = |
16 struct |
13 struct |
17 |
14 |
18 open BNF_Util |
15 open BNF_Util |
|
16 open BNF_FP_Util |
19 |
17 |
20 fun prepare_sugar prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) lthy = |
18 val distinctN = "distinct"; |
|
19 |
|
20 fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) |
|
21 lthy = |
21 let |
22 let |
|
23 (* TODO: sanity checks on arguments *) |
|
24 |
|
25 val T as Type (T_name, _) = prep_typ lthy raw_T; |
|
26 val b = Binding.qualified_name T_name; |
|
27 |
22 val ctors = map (prep_term lthy) raw_ctors; |
28 val ctors = map (prep_term lthy) raw_ctors; |
|
29 val ctor_Tss = map (binder_types o fastype_of) ctors; |
23 |
30 |
24 (* TODO: sanity checks on arguments *) |
31 val ((xss, yss), _) = lthy |> |
25 val ctor_Tss = map (binder_types o fastype_of) ctors; |
32 mk_Freess "x" ctor_Tss |
26 val (ctor_argss, _) = lthy |> |
33 ||>> mk_Freess "y" ctor_Tss; |
27 mk_Freess "x" ctor_Tss; |
|
28 |
34 |
29 val goal_distincts = |
35 val goal_injects = |
30 let |
36 let |
31 fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u))) |
37 fun mk_goal _ [] [] = NONE |
32 fun mk_goals [] = [] |
38 | mk_goal ctor xs ys = |
33 | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts) |
39 SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
40 (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)), |
|
41 Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))); |
34 in |
42 in |
35 mk_goals (map2 (curry Term.list_comb) ctors ctor_argss) |
43 map_filter I (map3 mk_goal ctors xss yss) |
36 end; |
44 end; |
37 |
45 |
38 val goals = goal_distincts; |
46 val goal_half_distincts = |
|
47 let |
|
48 fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u))); |
|
49 fun mk_goals [] = [] |
|
50 | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts); |
|
51 in |
|
52 mk_goals (map2 (curry Term.list_comb) ctors xss) |
|
53 end; |
|
54 |
|
55 val goals = [goal_injects, goal_half_distincts]; |
|
56 |
|
57 fun after_qed thmss lthy = |
|
58 let |
|
59 val [inject_thms, half_distinct_thms] = thmss; |
|
60 |
|
61 val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms; |
|
62 |
|
63 fun note thmN thms = |
|
64 snd o Local_Theory.note |
|
65 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms); |
|
66 in |
|
67 lthy |
|
68 |> note injectN inject_thms |
|
69 |> note distinctN (half_distinct_thms @ other_half_distinct_thms) |
|
70 end; |
39 in |
71 in |
40 (goals, lthy) |
72 (goals, after_qed, lthy) |
41 end; |
73 end; |
42 |
74 |
43 val parse_binding_list = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
75 val parse_binding_list = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
44 |
76 |
45 val bnf_sugar_cmd = (fn (goals, lthy) => |
77 val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => |
46 Proof.theorem NONE (K I) (map (single o rpair []) goals) lthy) oo prepare_sugar Syntax.read_term; |
78 Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo |
|
79 prepare_sugar Syntax.read_typ Syntax.read_term; |
47 |
80 |
48 val _ = |
81 val _ = |
49 Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" |
82 Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" |
50 ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- |
83 ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- |
51 parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") -- |
84 parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") -- |