1 theory Closures2

     1 theory Closures2

     2 imports 

     2 imports 

     3   Closures

     3   Closures

     4   Higman

     4   Higman

     6 begin

     5 begin

     7 

     6 

     8 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}

     7 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}

     9 

     8 

    10 (* compatibility with Higman theory by Stefan *)

     9 (* compatibility with Higman theory by Stefan *)

   118   have "{(x, y). x \<preceq> y \<and> x \<noteq> y} \<subseteq> measure length"

   117   have "{(x, y). x \<preceq> y \<and> x \<noteq> y} \<subseteq> measure length"

   119     unfolding measure_def by (auto simp add: emb_strict_length)

   118     unfolding measure_def by (auto simp add: emb_strict_length)

   120   ultimately 

   119   ultimately 

   121   show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset)

   120   show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset)

   122 qed

   121 qed

   123 

   123 

   124 subsection {* Sub- and Supsequences *}

   124 subsection {* Sub- and Supsequences *}

   125 

   125 

   126 definition

   126 definition

   127  "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"

   127  "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"