equal
deleted
inserted
replaced
1 theory Equivp |
1 theory Equivp |
2 imports "Fv" |
2 imports "NewFv" "Tacs" "Rsp" "NewFv" |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 fun build_alpha_sym_trans_gl alphas (x, y, z) = |
6 fun build_alpha_sym_trans_gl alphas (x, y, z) = |
7 let |
7 let |
186 val names = Datatype_Prop.make_tnames tys |
186 val names = Datatype_Prop.make_tnames tys |
187 val frees = map Free (names ~~ tys) |
187 val frees = map Free (names ~~ tys) |
188 val rhs = list_comb (cnstr, frees) |
188 val rhs = list_comb (cnstr, frees) |
189 |
189 |
190 fun mk_supp_arg (x, ty) = |
190 fun mk_supp_arg (x, ty) = |
191 if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
191 if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else |
192 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
192 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
193 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
193 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
194 else mk_supp ty x |
194 else mk_supp ty x |
195 val lhss = map mk_supp_arg (frees ~~ tys) |
195 val lhss = map mk_supp_arg (frees ~~ tys) |
196 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
196 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |