1.1 --- a/src/HOL/Extraction/Higman.thy	Wed Aug 07 16:48:20 2002 +0200
     1.2 +++ b/src/HOL/Extraction/Higman.thy	Wed Aug 07 16:49:25 2002 +0200
     1.3 @@ -292,9 +292,7 @@
     1.4    done
     1.5  
     1.6  
     1.7 -subsection {* Realizers *}
     1.8 -
     1.9 -subsubsection {* Bar induction *}
    1.10 +subsection {* Realizer for Bar induction *}
    1.11  
    1.12  datatype Bar =
    1.13     Good "letter list list"
    1.14 @@ -355,34 +353,6 @@
    1.15      "\<Lambda>x P r (h1: _) f (h2: _) g.
    1.16         Bar_ind_realizer \<cdot> _ \<cdot> _ \<cdot> (\<lambda>r x. realizes r (P x)) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h2"
    1.17  
    1.18 -subsubsection {* Lists *}
    1.19 -
    1.20 -theorem list_ind_realizer:
    1.21 -  assumes f: "P f []"
    1.22 -  and g: "\<And>a as r. P r as \<Longrightarrow> P (g a as r) (a # as)"
    1.23 -  shows "P (list_rec f g xs) xs"
    1.24 -  apply (induct xs)
    1.25 -  apply simp
    1.26 -  apply (rule f)
    1.27 -  apply simp
    1.28 -  apply (rule g)
    1.29 -  apply assumption
    1.30 -  done
    1.31 -
    1.32 -realizers
    1.33 -  list.induct (P): "\<lambda>P xs f g. list_rec f g xs"
    1.34 -    "\<Lambda>P xs f (h: _) g. list_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
    1.35 -
    1.36 -subsubsection {* Letters *}
    1.37 -
    1.38 -theorem letter_exhaust_realizer:
    1.39 -  "(y = A \<Longrightarrow> P r) \<Longrightarrow> (y = B \<Longrightarrow> P s) \<Longrightarrow> P (case y of A \<Rightarrow> r | B \<Rightarrow> s)"
    1.40 -  by (case_tac y, simp+)
    1.41 -
    1.42 -realizers
    1.43 -  letter.exhaust (P): "\<lambda>y P r s. case y of A \<Rightarrow> r | B \<Rightarrow> s"
    1.44 -    "\<Lambda>y P r (h: _) s. letter_exhaust_realizer \<cdot> _ \<cdot> (\<lambda>x. realizes x P) \<cdot> _ \<cdot> _ \<bullet> h"
    1.45 -
    1.46  
    1.47  subsection {* Extracting the program *}
    1.48