src/HOL/Wellfounded.thy
changeset 37767 a2b7a20d6ea3
parent 37407 61dd8c145da7
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -682,9 +682,8 @@
     1.4  
     1.5  text{* Lexicographic combinations *}
     1.6  
     1.7 -definition
     1.8 -  lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
     1.9 -  [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
    1.10 +definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
    1.11 +  "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
    1.12  
    1.13  lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
    1.14  apply (unfold wf_def lex_prod_def) 
    1.15 @@ -819,10 +818,8 @@
    1.16  by (force elim!: max_ext.cases)
    1.17  
    1.18  
    1.19 -definition
    1.20 -  min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
    1.21 -where
    1.22 -  [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
    1.23 +definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"  where
    1.24 +  "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
    1.25  
    1.26  lemma min_ext_wf:
    1.27    assumes "wf r"