equal
deleted
inserted
replaced
5 Definitions and proofs for the alpha-relations. |
5 Definitions and proofs for the alpha-relations. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
|
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
|
11 |
10 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
11 bclause list list list -> term list -> Proof.context -> |
13 bclause list list list -> term list -> Proof.context -> |
12 term list * term list * thm list * thm list * thm * local_theory |
14 term list * term list * thm list * thm list * thm * local_theory |
13 |
15 |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
16 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
69 in |
71 in |
70 Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 |
72 Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 |
71 end |
73 end |
72 |
74 |
73 (* generates the compound binder terms *) |
75 (* generates the compound binder terms *) |
74 fun mk_binders lthy bmode args binders = |
76 fun comb_binders lthy bmode args binders = |
75 let |
77 let |
76 fun bind_set lthy args (NONE, i) = setify lthy (nth args i) |
78 fun bind_set lthy args (NONE, i) = setify lthy (nth args i) |
77 | bind_set _ args (SOME bn, i) = bn $ (nth args i) |
79 | bind_set _ args (SOME bn, i) = bn $ (nth args i) |
78 fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) |
80 fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) |
79 | bind_lst _ args (SOME bn, i) = bn $ (nth args i) |
81 | bind_lst _ args (SOME bn, i) = bn $ (nth args i) |
148 val (alphas, fvs) = split_list (map mk_alpha_fv bodies) |
150 val (alphas, fvs) = split_list (map mk_alpha_fv bodies) |
149 val comp_fv = foldl1 mk_prod_fv fvs |
151 val comp_fv = foldl1 mk_prod_fv fvs |
150 val comp_alpha = foldl1 mk_prod_alpha alphas |
152 val comp_alpha = foldl1 mk_prod_alpha alphas |
151 val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) |
153 val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) |
152 val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) |
154 val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) |
153 val comp_binders = mk_binders lthy bmode args binders |
155 val comp_binders = comb_binders lthy bmode args binders |
154 val comp_binders' = mk_binders lthy bmode args' binders |
156 val comp_binders' = comb_binders lthy bmode args' binders |
155 val alpha_prem = |
157 val alpha_prem = |
156 mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' |
158 mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' |
157 val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) |
159 val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) |
158 in |
160 in |
159 map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) |
161 map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) |