author | blanchet |
Thu, 30 Aug 2012 09:47:46 +0200 | |
changeset 49023 | 5afe918dd476 |
parent 49022 | 005ce926a932 |
child 49025 | 7e89b0520e83 |
permissions | -rw-r--r-- |
49017 | 1 |
(* Title: HOL/Codatatype/Tools/bnf_sugar.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2012 |
|
4 |
||
5 |
Sugar on top of a BNF. |
|
6 |
*) |
|
7 |
||
8 |
signature BNF_SUGAR = |
|
9 |
sig |
|
10 |
end; |
|
11 |
||
12 |
structure BNF_Sugar : BNF_SUGAR = |
|
13 |
struct |
|
14 |
||
15 |
open BNF_Util |
|
49019 | 16 |
open BNF_FP_Util |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
17 |
open BNF_Sugar_Tactics |
49017 | 18 |
|
49019 | 19 |
val distinctN = "distinct"; |
20 |
||
49023 | 21 |
fun prepare_sugar prep_term (((raw_ctors, raw_caseof), dtor_names), stor_namess) no_defs_lthy = |
49017 | 22 |
let |
49019 | 23 |
(* TODO: sanity checks on arguments *) |
49017 | 24 |
|
49022 | 25 |
val ctors = map (prep_term no_defs_lthy) raw_ctors; |
49017 | 26 |
val ctor_Tss = map (binder_types o fastype_of) ctors; |
27 |
||
49022 | 28 |
val caseof = prep_term no_defs_lthy raw_caseof; |
29 |
||
30 |
val T as Type (T_name, As) = body_type (fastype_of (hd ctors)); |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
31 |
val b = Binding.qualified_name T_name; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
32 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
33 |
val n = length ctors; |
49022 | 34 |
val ks = 1 upto n; |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
35 |
|
49022 | 36 |
fun mk_caseof T = |
37 |
let |
|
38 |
val (binders, body) = strip_type (fastype_of caseof); |
|
39 |
in |
|
40 |
Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ As)) caseof |
|
41 |
end; |
|
42 |
||
43 |
val ((((xss, yss), (v, v')), p), no_defs_lthy') = no_defs_lthy |> |
|
49019 | 44 |
mk_Freess "x" ctor_Tss |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
45 |
||>> mk_Freess "y" ctor_Tss |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
46 |
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
47 |
||>> yield_singleton (mk_Frees "P") HOLogic.boolT; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
48 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
49 |
val xs_ctors = map2 (curry Term.list_comb) ctors xss; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
50 |
val ys_ctors = map2 (curry Term.list_comb) ctors yss; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
51 |
|
49022 | 52 |
val exist_xs_v_eq_ctors = |
53 |
map2 (fn xs_ctor => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xs_ctor))) xs_ctors xss; |
|
54 |
||
55 |
fun dtor_spec b exist_xs_v_eq_ctor = |
|
56 |
HOLogic.mk_Trueprop |
|
57 |
(HOLogic.mk_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctor)); |
|
58 |
||
59 |
fun stor_spec b x xs xs_ctor k = |
|
60 |
let |
|
61 |
val T' = fastype_of x; |
|
62 |
in |
|
63 |
HOLogic.mk_Trueprop |
|
64 |
(HOLogic.mk_eq (Free (Binding.name_of b, T --> T') $ v, |
|
65 |
Term.list_comb (mk_caseof T', map2 (fn Ts => fn i => |
|
66 |
if i = k then fold_rev lambda xs x else Const (@{const_name undefined}, Ts ---> T')) |
|
67 |
ctor_Tss ks) $ v)) |
|
68 |
end; |
|
69 |
||
70 |
val ((dtor_defs, stor_defss), (lthy', lthy)) = |
|
71 |
no_defs_lthy |
|
72 |
|> fold_map2 (fn b => fn exist_xs_v_eq_ctor => |
|
73 |
Specification.definition (SOME (b, NONE, NoSyn), |
|
74 |
((Thm.def_binding b, []), dtor_spec b exist_xs_v_eq_ctor))) dtor_names exist_xs_v_eq_ctors |
|
75 |
||>> fold_map4 (fn bs => fn xs => fn xs_ctor => fn k => |
|
76 |
fold_map2 (fn b => fn x => |
|
77 |
Specification.definition (SOME (b, NONE, NoSyn), |
|
78 |
((Thm.def_binding b, []), stor_spec b x xs xs_ctor k))) bs xs) stor_namess xss xs_ctors |
|
79 |
ks |
|
80 |
||> `Local_Theory.restore; |
|
81 |
||
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
82 |
val goal_exhaust = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
83 |
let |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
84 |
fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p); |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
85 |
fun mk_prem xs_ctor xs = |
49022 | 86 |
fold_rev Logic.all xs (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xs_ctor))]); |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
87 |
in |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
88 |
mk_imp_p (map2 mk_prem xs_ctors xss) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
89 |
end; |
49019 | 90 |
|
91 |
val goal_injects = |
|
49017 | 92 |
let |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
93 |
fun mk_goal _ _ [] [] = NONE |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
94 |
| mk_goal xs_ctor ys_ctor xs ys = |
49019 | 95 |
SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
96 |
(HOLogic.mk_eq (xs_ctor, ys_ctor), |
49019 | 97 |
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))); |
49017 | 98 |
in |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
99 |
map_filter I (map4 mk_goal xs_ctors ys_ctors xss yss) |
49017 | 100 |
end; |
101 |
||
49019 | 102 |
val goal_half_distincts = |
103 |
let |
|
104 |
fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u))); |
|
105 |
fun mk_goals [] = [] |
|
106 |
| mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts); |
|
107 |
in |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
108 |
mk_goals xs_ctors |
49019 | 109 |
end; |
110 |
||
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
111 |
val goals = [[goal_exhaust], goal_injects, goal_half_distincts]; |
49019 | 112 |
|
113 |
fun after_qed thmss lthy = |
|
114 |
let |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
115 |
val [[exhaust_thm], inject_thms, half_distinct_thms] = thmss; |
49019 | 116 |
|
117 |
val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms; |
|
118 |
||
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
119 |
val nchotomy_thm = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
120 |
let |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
121 |
val goal = |
49022 | 122 |
HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', |
123 |
Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctors)); |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
124 |
in |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
125 |
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
126 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
127 |
|
49019 | 128 |
fun note thmN thms = |
129 |
snd o Local_Theory.note |
|
130 |
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms); |
|
131 |
in |
|
132 |
lthy |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
133 |
|> note distinctN (half_distinct_thms @ other_half_distinct_thms) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
134 |
|> note exhaustN [exhaust_thm] |
49019 | 135 |
|> note injectN inject_thms |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
136 |
|> note nchotomyN [nchotomy_thm] |
49019 | 137 |
end; |
49017 | 138 |
in |
49019 | 139 |
(goals, after_qed, lthy) |
49017 | 140 |
end; |
141 |
||
142 |
val parse_binding_list = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
|
143 |
||
49019 | 144 |
val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => |
145 |
Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
146 |
prepare_sugar Syntax.read_term; |
49017 | 147 |
|
148 |
val _ = |
|
149 |
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" |
|
49023 | 150 |
(((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- |
151 |
parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]")) |
|
152 |
>> bnf_sugar_cmd); |
|
49017 | 153 |
|
154 |
end; |