src/HOL/Lambda/Lambda.thy

--- a/src/HOL/Lambda/Lambda.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -53,29 +53,21 @@
 
 subsection {* Beta-reduction *}
 
-consts
-  beta :: "(dB \<times> dB) set"
-
-abbreviation
-  beta_red :: "[dB, dB] => bool"  (infixl "->" 50) where
-  "s -> t == (s, t) \<in> beta"
+inductive2 beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  where
+    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
 
 abbreviation
   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
-  "s ->> t == (s, t) \<in> beta^*"
+  "s ->> t == beta^** s t"
 
 notation (latex)
-  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50) and
   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
-inductive beta
-  intros
-    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
-    appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
-    appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
-    abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
-
-inductive_cases beta_cases [elim!]:
+inductive_cases2 beta_cases [elim!]:
   "Var i \<rightarrow>\<^sub>\<beta> t"
   "Abs r \<rightarrow>\<^sub>\<beta> s"
   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
@@ -88,19 +80,19 @@
 
 lemma rtrancl_beta_Abs [intro!]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppL:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppR:
     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
-  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
-  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
+  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
 
 
 subsection {* Substitution-lemmas *}
@@ -164,8 +156,8 @@
 
 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_into_rtrancl)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl.rtrancl_into_rtrancl)
   apply (erule subst_preserves_beta)
   done
 
@@ -175,22 +167,22 @@
 
 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_into_rtrancl)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl.rtrancl_into_rtrancl)
   apply (erule lift_preserves_beta)
   done
 
 theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   apply (induct t arbitrary: r s i)
-    apply (simp add: subst_Var r_into_rtrancl)
+    apply (simp add: subst_Var r_into_rtrancl')
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)
   done
 
 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   apply (induct set: rtrancl)
-   apply (rule rtrancl_refl)
-  apply (erule rtrancl_trans)
+   apply (rule rtrancl.rtrancl_refl)
+  apply (erule rtrancl_trans')
   apply (erule subst_preserves_beta2)
   done