src/HOLCF/IOA/meta_theory/Seq.thy

 
 abbreviation
   sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
   "xs @@ ys == sconc $ xs $ ys"
 
-abbreviation
-  Finite :: "'a seq => bool" where
-  "Finite x == x:sfinite"
+inductive
+  Finite :: "'a seq => bool"
+  where
+    sfinite_0:  "Finite nil"
+  | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
 
 defs
 
 (* f not possible at lhs, as "pattern matching" only for % x arguments,
    f cannot be written at rhs in front, as fix_eq3 does not apply later *)

 
 Infinite_def:
   "Infinite x == ~(seq_finite x)"
 
 
-inductive "sfinite"
-   intros
-    sfinite_0:  "nil:sfinite"
-    sfinite_n:  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
-
-declare sfinite.intros [simp]
+declare Finite.intros [simp]
 declare seq.rews [simp]
 
 
 subsection {* recursive equations of operators *}
 

 (* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
 (* ----------------------------------------------------  *)
 
 lemma Finite_UU_a: "Finite x --> x~=UU"
 apply (rule impI)
-apply (erule sfinite.induct)
+apply (erule Finite.induct)
  apply simp
 apply simp
 done
 
 lemma Finite_UU [simp]: "~(Finite UU)"

 apply fast
 done
 
 lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
 apply (intro strip)
-apply (erule sfinite.elims)
+apply (erule Finite.cases)
 apply fastsimp
 apply (simp add: seq.injects)
 done
 
 lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"