# HG changeset patch
# User berghofe
# Date 1028731765 -7200
# Node ID d2cbbad84ad334e3e6cc4736bc3e3b01aa1b3cbc
# Parent  70d8dfef587d6f0b632aeafe2b118412e2691ee5
Removed (now unneeded) declarations of realizers for induction on lists and letters.

diff -r 70d8dfef587d -r d2cbbad84ad3 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Wed Aug 07 16:48:20 2002 +0200
+++ b/src/HOL/Extraction/Higman.thy	Wed Aug 07 16:49:25 2002 +0200
@@ -292,9 +292,7 @@
   done
 
 
-subsection {* Realizers *}
-
-subsubsection {* Bar induction *}
+subsection {* Realizer for Bar induction *}
 
 datatype Bar =
    Good "letter list list"
@@ -355,34 +353,6 @@
     "\<Lambda>x P r (h1: _) f (h2: _) g.
        Bar_ind_realizer \<cdot> _ \<cdot> _ \<cdot> (\<lambda>r x. realizes r (P x)) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h2"
 
-subsubsection {* Lists *}
-
-theorem list_ind_realizer:
-  assumes f: "P f []"
-  and g: "\<And>a as r. P r as \<Longrightarrow> P (g a as r) (a # as)"
-  shows "P (list_rec f g xs) xs"
-  apply (induct xs)
-  apply simp
-  apply (rule f)
-  apply simp
-  apply (rule g)
-  apply assumption
-  done
-
-realizers
-  list.induct (P): "\<lambda>P xs f g. list_rec f g xs"
-    "\<Lambda>P xs f (h: _) g. list_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
-
-subsubsection {* Letters *}
-
-theorem letter_exhaust_realizer:
-  "(y = A \<Longrightarrow> P r) \<Longrightarrow> (y = B \<Longrightarrow> P s) \<Longrightarrow> P (case y of A \<Rightarrow> r | B \<Rightarrow> s)"
-  by (case_tac y, simp+)
-
-realizers
-  letter.exhaust (P): "\<lambda>y P r s. case y of A \<Rightarrow> r | B \<Rightarrow> s"
-    "\<Lambda>y P r (h: _) s. letter_exhaust_realizer \<cdot> _ \<cdot> (\<lambda>x. realizes x P) \<cdot> _ \<cdot> _ \<bullet> h"
-
 
 subsection {* Extracting the program *}