41 HOLogic.mk_binop @{const_name minus} (a, b); |
41 HOLogic.mk_binop @{const_name minus} (a, b); |
42 *} |
42 *} |
43 |
43 |
44 atom_decl name |
44 atom_decl name |
45 |
45 |
46 datatype rlam = |
46 datatype rtrm1 = |
47 rVar "name" |
47 rVr1 "name" |
48 | rApp "rlam" "rlam" |
48 | rAp1 "rtrm1" "rtrm1" |
49 | rLam "name" "rlam" |
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" |
50 |
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 |
51 ML {* |
66 ML {* |
52 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
67 val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1"; |
53 val sorts = []; |
68 val sorts = []; |
54 val binds = [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]]; |
69 val bindsall = [ |
|
70 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [], [(SOME @{term bv1}, 0)]]], |
|
71 [[], [[]], [[], []]] |
|
72 ]; |
55 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
73 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
56 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
74 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
57 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
75 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
58 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
76 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
59 val fv_frees = map Free (fv_names ~~ fv_types); |
77 val fv_frees = map Free (fv_names ~~ fv_types); |
75 HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
93 HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
76 val sub = mk_union (map fv_bind bindxs) |
94 val sub = mk_union (map fv_bind bindxs) |
77 in |
95 in |
78 mk_diff arg sub |
96 mk_diff arg sub |
79 end; |
97 end; |
|
98 val _ = tracing ("d" ^ string_of_int (length dts)); |
|
99 val _ = tracing (string_of_int (length args)); |
|
100 val _ = tracing (string_of_int (length bindcs)); |
80 in |
101 in |
81 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
102 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
82 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
103 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
83 end; |
104 end; |
84 fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds; |
105 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
85 val fv_eqs = maps fv_eq descr |
106 val fv_eqs = flat (map2 fv_eq descr bindsall) |
86 *} |
107 *} |
87 |
108 |
88 |
109 |
89 local_setup {* |
110 local_setup {* |
90 snd o (Primrec.add_primrec |
111 snd o (Primrec.add_primrec |
91 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs) |
112 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs) |
92 *} |
113 *} |
93 print_theorems |
114 print_theorems |
94 |
115 |
95 fun |
|
96 fv_rlam :: "rlam \<Rightarrow> atom set" |
|
97 where |
|
98 "fv_rlam (rVar a) = {atom a}" |
|
99 | "fv_rlam (rApp t1 t2) = (fv_rlam t1) \<union> (fv_rlam t2)" |
|
100 | "fv_rlam (rLam a t) = (fv_rlam t) - {atom a}" |
|
101 |
116 |
102 end |
117 end |