25 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
25 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
26 *) |
26 *) |
27 |
27 |
28 ML {* |
28 ML {* |
29 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
29 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
|
30 (* TODO: It is the same as one in 'nominal_atoms' *) |
30 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
31 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
31 val noatoms = @{term "{} :: atom set"}; |
32 val noatoms = @{term "{} :: atom set"}; |
32 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; |
33 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; |
33 fun mk_union sets = |
34 fun mk_union sets = |
34 fold (fn a => fn b => |
35 fold (fn a => fn b => |
39 if b = noatoms then a else |
40 if b = noatoms then a else |
40 if b = a then noatoms else |
41 if b = a then noatoms else |
41 HOLogic.mk_binop @{const_name minus} (a, b); |
42 HOLogic.mk_binop @{const_name minus} (a, b); |
42 *} |
43 *} |
43 |
44 |
44 atom_decl name |
|
45 |
|
46 datatype rtrm1 = |
|
47 rVr1 "name" |
|
48 | rAp1 "rtrm1" "rtrm1" |
|
49 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
50 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
51 and bp = |
|
52 BUnit |
|
53 | BVr "name" |
|
54 | BPr "bp" "bp" |
|
55 |
|
56 (* to be given by the user *) |
|
57 |
|
58 primrec |
|
59 bv1 |
|
60 where |
|
61 "bv1 (BUnit) = {}" |
|
62 | "bv1 (BVr x) = {atom x}" |
|
63 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
64 |
|
65 ML maps |
|
66 ML {* |
45 ML {* |
67 val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1"; |
46 (* Currently needs just one full_tname to access Datatype *) |
68 val sorts = []; |
47 fun define_raw_fv full_tname bindsall lthy = |
69 val bindsall = [ |
48 let |
70 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
49 val thy = ProofContext.theory_of lthy |
71 [[], [[]], [[], []]] |
50 val {descr, ...} = Datatype.the_info thy full_tname; |
72 ]; |
51 val sorts = []; (* TODO *) |
73 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
52 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
74 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
53 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
75 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
54 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
76 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
55 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
77 val fv_frees = map Free (fv_names ~~ fv_types); |
56 val fv_frees = map Free (fv_names ~~ fv_types); |
104 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
83 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
105 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
84 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
106 end; |
85 end; |
107 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
86 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
108 val fv_eqs = flat (map2 fv_eq descr bindsall) |
87 val fv_eqs = flat (map2 fv_eq descr bindsall) |
|
88 in |
|
89 snd (Primrec.add_primrec |
|
90 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
|
91 end |
109 *} |
92 *} |
110 |
93 |
111 |
94 |
112 local_setup {* |
95 atom_decl name |
113 snd o (Primrec.add_primrec |
96 |
114 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs) |
97 datatype rtrm1 = |
115 *} |
98 rVr1 "name" |
|
99 | rAp1 "rtrm1" "rtrm1" |
|
100 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
101 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
102 and bp = |
|
103 BUnit |
|
104 | BVr "name" |
|
105 | BPr "bp" "bp" |
|
106 |
|
107 (* to be given by the user *) |
|
108 |
|
109 primrec |
|
110 bv1 |
|
111 where |
|
112 "bv1 (BUnit) = {}" |
|
113 | "bv1 (BVr x) = {atom x}" |
|
114 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
115 |
|
116 local_setup {* define_raw_fv "Fv.rtrm1" |
|
117 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
118 [[], [[]], [[], []]]] *} |
116 print_theorems |
119 print_theorems |
117 |
120 |
118 |
|
119 end |
121 end |