Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/BNF_FP_N2M.thy
author blanchet
Fri, 30 Aug 2013 11:27:23 +0200
changeset 53303 ae49b835ca01
child 53304 cfef783090eb
permissions -rw-r--r--
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository

(*  Title:      HOL/BNF/BNF_FP_N2M.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2013

Flattening of nested to mutual (co)recursion.
*)

header {* Flattening of Nested to Mutual (Co)recursion *}

theory BNF_FP_N2M
imports "~~/src/HOL/BNF/BNF_FP_Basic"
begin

lemma eq_le_Grp_id_iff: "(op = \<le> BNF_Util.Grp (Collect R) id) = (All R)"
  unfolding Grp_def id_apply by blast

lemma Grp_id_mono_subst: "(\<And>x y. BNF_Util.Grp P id x y \<Longrightarrow> BNF_Util.Grp Q id (f x) (f y)) \<equiv>
   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
  unfolding Grp_def by rule auto

ML_file "Tools/bnf_fp_n2m_tactics.ML"
ML_file "Tools/bnf_fp_n2m.ML"
ML_file "Tools/bnf_fp_n2m_sugar.ML"

end
isabelle