# HG changeset patch
# User berghofe
# Date 1051518822 -7200
# Node ID 562fd03b266de9666dfebcfb670cba209651a056
# Parent  21615e44ba886cfb1ecca7f9a2c92b45f75346b9
Converted main proofs to Isar.

diff -r 21615e44ba88 -r 562fd03b266d src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Mon Apr 28 09:58:12 2003 +0200
+++ b/src/HOL/Extraction/Higman.thy	Mon Apr 28 10:33:42 2003 +0200
@@ -63,7 +63,7 @@
 inductive bar
 intros
   bar1 [CPure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
-  bar2 [CPure.intro]: "(\<forall>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
+  bar2 [CPure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
 
 theorem prop1: "([] # ws) \<in> bar" by rules
 
@@ -127,67 +127,6 @@
   apply rules+
   done
 
-theorem letter_cases:
-  "(a::letter) \<noteq> b \<Longrightarrow> (x = a \<Longrightarrow> P) \<Longrightarrow> (x = b \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (case_tac a)
-  apply (case_tac b)
-  apply (case_tac x, simp, simp)
-  apply (case_tac x, simp, simp)
-  apply (case_tac b)
-  apply (case_tac x, simp, simp)
-  apply (case_tac x, simp, simp)
-  done
-  
-theorem prop2:
-  "xs \<in> bar \<Longrightarrow> \<forall>ys. ys \<in> bar \<longrightarrow>
-     (\<forall>a b zs. a \<noteq> b \<longrightarrow> (xs, zs) \<in> T a \<longrightarrow> (ys, zs) \<in> T b \<longrightarrow> zs \<in> bar)"
-  apply (erule bar.induct)
-  apply (rule allI impI)+
-  apply (rule bar1)
-  apply (rule lemma3)
-  apply assumption+
-  apply (rule allI, rule impI)
-  apply (erule bar.induct)
-  apply (rule allI impI)+
-  apply (rule bar1)
-  apply (rule lemma3, assumption, assumption)
-  apply (rule allI impI)+
-  apply (rule bar2)
-  apply (rule allI)
-  apply (induct_tac w)
-  apply (rule prop1)
-  apply (rule_tac x=aa in letter_cases, assumption)
-  apply hypsubst
-  apply (erule_tac x=list in allE)
-  apply (erule conjE)
-  apply (erule_tac x=wsa in allE, erule impE)
-  apply (rule bar2)
-  apply rules
-  apply (erule allE, erule allE, erule_tac x="(a # list) # zs" in allE,
-    erule impE, assumption)
-  apply (erule impE)
-  apply (rule T1)
-  apply assumption
-  apply (erule mp)
-  apply (rule T2)
-  apply (erule not_sym)
-  apply assumption
-  apply hypsubst
-  apply (rotate_tac 1)
-  apply (erule_tac x=list in allE)
-  apply (erule conjE)
-  apply (erule allE, erule allE, erule_tac x="(b # list) # zs" in allE,
-    erule impE)
-  apply assumption
-  apply (erule impE)
-  apply (rule T2)
-  apply assumption
-  apply assumption
-  apply (erule mp)
-  apply (rule T1)
-  apply assumption
-  done
-
 theorem lemma4 [rule_format]: "(ws, zs) \<in> R a \<Longrightarrow> ws \<noteq> [] \<longrightarrow> (ws, zs) \<in> T a"
   apply (erule R.induct)
   apply rules
@@ -208,10 +147,17 @@
   apply simp
   done
 
-theorem R_nil: "([], zs) \<in> R a \<Longrightarrow> zs = []"
-  by (erule R.elims, simp+)
+lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"
+  apply (case_tac a)
+  apply (case_tac b)
+  apply (case_tac c, simp, simp)
+  apply (case_tac c, simp, simp)
+  apply (case_tac b)
+  apply (case_tac c, simp, simp)
+  apply (case_tac c, simp, simp)
+  done
 
-theorem letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"
+lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"
   apply (case_tac a)
   apply (case_tac b)
   apply simp
@@ -221,50 +167,92 @@
   apply simp
   done
 
-theorem prop3: "xs \<in> bar \<Longrightarrow> \<forall>zs. (xs, zs) \<in> R a \<longrightarrow> zs \<in> bar"
-  apply (erule bar.induct)
-  apply (rule allI impI)+
-  apply (rule bar1)
-  apply (rule lemma2)
-  apply assumption+
-  apply (rule allI impI)+
-  apply (case_tac ws)
-  apply simp
-  apply (drule R_nil)
-  apply simp_all
-  apply rules
-  apply (rule bar2)
-  apply (rule allI)
-  apply (induct_tac w)
-  apply (rule prop1)
-  apply (rule_tac a1=aaa and b1=a in disjE [OF letter_eq_dec])
-  apply rules
-  apply (rule_tac xs="aa # list" and ys="lista # zs" and zs="(aaa # lista) # zs"
-    and b=aaa in prop2 [rule_format])
-  apply (rule bar2)
-  apply rules
-  apply assumption
-  apply (erule not_sym)
-  apply (rule T2)
-  apply (erule not_sym)
-  apply (erule lemma4)
-  apply simp
-  apply (rule T0)
-  apply assumption+
-  done
+theorem prop2:
+  assumes ab: "a \<noteq> b" and bar: "xs \<in> bar"
+  shows "\<And>ys zs. ys \<in> bar \<Longrightarrow> (xs, zs) \<in> T a \<Longrightarrow> (ys, zs) \<in> T b \<Longrightarrow> zs \<in> bar" using bar
+proof induct
+  fix xs zs assume "xs \<in> good" and "(xs, zs) \<in> T a"
+  show "zs \<in> bar" by (rule bar1) (rule lemma3)
+next
+  fix xs ys
+  assume I: "\<And>w ys zs. ys \<in> bar \<Longrightarrow> (w # xs, zs) \<in> T a \<Longrightarrow> (ys, zs) \<in> T b \<Longrightarrow> zs \<in> bar"
+  assume "ys \<in> bar"
+  thus "\<And>zs. (xs, zs) \<in> T a \<Longrightarrow> (ys, zs) \<in> T b \<Longrightarrow> zs \<in> bar"
+  proof induct
+    fix ys zs assume "ys \<in> good" and "(ys, zs) \<in> T b"
+    show "zs \<in> bar" by (rule bar1) (rule lemma3)
+  next
+    fix ys zs assume I': "\<And>w zs. (xs, zs) \<in> T a \<Longrightarrow> (w # ys, zs) \<in> T b \<Longrightarrow> zs \<in> bar"
+    and ys: "\<And>w. w # ys \<in> bar" and Ta: "(xs, zs) \<in> T a" and Tb: "(ys, zs) \<in> T b"
+    show "zs \<in> bar"
+    proof (rule bar2)
+      fix w
+      show "w # zs \<in> bar"
+      proof (cases w)
+	case Nil
+	thus ?thesis by simp (rule prop1)
+      next
+	case (Cons c cs)
+	from letter_eq_dec show ?thesis
+	proof
+	  assume ca: "c = a"
+	  from ab have "(a # cs) # zs \<in> bar" by (rules intro: I ys Ta Tb)+
+	  thus ?thesis by (simp add: Cons ca)
+	next
+	  assume "c \<noteq> a"
+	  with ab have cb: "c = b" by (rule letter_neq)
+	  from ab have "(b # cs) # zs \<in> bar" by (rules intro: I' Ta Tb)+
+	  thus ?thesis by (simp add: Cons cb)
+	qed
+      qed
+    qed
+  qed
+qed
 
-theorem prop5: "[w] \<in> bar"
-  apply (induct_tac w)
-  apply (rule prop1)
-  apply (rule prop3 [rule_format])
-  apply rules+
-  done
+theorem prop3:
+  assumes bar: "xs \<in> bar"
+  shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> (xs, zs) \<in> R a \<Longrightarrow> zs \<in> bar" using bar
+proof induct
+  fix xs zs
+  assume "xs \<in> good" and "(xs, zs) \<in> R a"
+  show "zs \<in> bar" by (rule bar1) (rule lemma2)
+next
+  fix xs zs
+  assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> (w # xs, zs) \<in> R a \<Longrightarrow> zs \<in> bar"
+  and xsb: "\<And>w. w # xs \<in> bar" and xsn: "xs \<noteq> []" and R: "(xs, zs) \<in> R a"
+  show "zs \<in> bar"
+  proof (rule bar2)
+    fix w
+    show "w # zs \<in> bar"
+    proof (induct w)
+      case Nil
+      show ?case by (rule prop1)
+    next
+      case (Cons c cs)
+      from letter_eq_dec show ?case
+      proof
+	assume "c = a"
+	thus ?thesis by (rules intro: I [simplified] R)
+      next
+	from R xsn have T: "(xs, zs) \<in> T a" by (rule lemma4)
+	assume "c \<noteq> a"
+	thus ?thesis by (rules intro: prop2 Cons xsb xsn R T)
+      qed
+    qed
+  qed
+qed
 
 theorem higman: "[] \<in> bar"
-  apply (rule bar2)
-  apply (rule allI)
-  apply (rule prop5)
-  done
+proof (rule bar2)
+  fix w
+  show "[w] \<in> bar"
+  proof (induct w)
+    show "[[]] \<in> bar" by (rule prop1)
+  next
+    fix c cs assume "[cs] \<in> bar"
+    thus "[c # cs] \<in> bar" by (rule prop3) (simp, rules)
+  qed
+qed
 
 consts
   is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
@@ -274,22 +262,20 @@
   "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
 
 theorem good_prefix_lemma:
-  "ws \<in> bar \<Longrightarrow> is_prefix ws f \<longrightarrow> (\<exists>vs. is_prefix vs f \<and> vs \<in> good)"
-  apply (erule bar.induct)
-  apply rules
-  apply (rule impI)
-  apply (erule_tac x="f (length ws)" in allE)
-  apply (erule conjE)
-  apply (erule impE)
-  apply simp
-  apply assumption
-  done
+  assumes bar: "ws \<in> bar"
+  shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> vs \<in> good" using bar
+proof induct
+  case bar1
+  thus ?case by rules
+next
+  case (bar2 ws)
+  have "is_prefix (f (length ws) # ws) f" by simp
+  thus ?case by (rules intro: bar2)
+qed
 
 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> vs \<in> good"
-  apply (insert higman)
-  apply (drule good_prefix_lemma)
-  apply simp
-  done
+  using higman
+  by (rule good_prefix_lemma) simp+
 
 subsection {* Extracting the program *}
 
@@ -306,8 +292,6 @@
   @{thm [display] good_prefix_lemma_def [no_vars]}
   Program extracted from the proof of @{text higman}:
   @{thm [display] higman_def [no_vars]}
-  Program extracted from the proof of @{text prop5}:
-  @{thm [display] prop5_def [no_vars]}
   Program extracted from the proof of @{text prop1}:
   @{thm [display] prop1_def [no_vars]}
   Program extracted from the proof of @{text prop2}: