equal
deleted
inserted
replaced
182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
186 in |
186 in |
187 (*if length pi_supps > 1 then |
187 if length pi_supps > 1 then |
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen |
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen |
189 (* TODO Add some test that is makes sense *) |
189 (* TODO Add some test that is makes sense *) |
190 end else @{term "True"} |
190 end else @{term "True"} |
191 end |
191 end |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
193 val alpha_lhss = mk_conjl alphas |
193 val alpha_lhss = mk_conjl alphas |