diff --git a/src/CCL/CCL.thy b/src/CCL/CCL.thy
--- a/src/CCL/CCL.thy
+++ b/src/CCL/CCL.thy
@@ -1,497 +1,497 @@
 (*  Title:      CCL/CCL.thy
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Classical Computational Logic for Untyped Lambda Calculus
   with reduction to weak head-normal form\<close>
 
 theory CCL
 imports Gfp
 begin
 
 text \<open>
   Based on FOL extended with set collection, a primitive higher-order
   logic.  HOL is too strong - descriptions prevent a type of programs
   being defined which contains only executable terms.
 \<close>
 
 class prog = "term"
 default_sort prog
 
 instance "fun" :: (prog, prog) prog ..
 
 typedecl i
 instance i :: prog ..
 
 
 consts
   (*** Evaluation Judgement ***)
   Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl "\<longlongrightarrow>" 20)
 
   (*** Bisimulations for pre-order and equality ***)
   po          ::       "['a,'a]\<Rightarrow>o"           (infixl "[=" 50)
 
   (*** Term Formers ***)
   true        ::       "i"
   false       ::       "i"
   pair        ::       "[i,i]\<Rightarrow>i"             ("(1<_,/_>)")
   lambda      ::       "(i\<Rightarrow>i)\<Rightarrow>i"            (binder "lam " 55)
   "case"      ::       "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   "apply"     ::       "[i,i]\<Rightarrow>i"             (infixl "`" 56)
   bot         ::       "i"
 
   (******* EVALUATION SEMANTICS *******)
 
   (**  This is the evaluation semantics from which the axioms below were derived.  **)
   (**  It is included here just as an evaluator for FUN and has no influence on    **)
   (**  inference in the theory CCL.                                                **)
 
 axiomatization where
   trueV:       "true \<longlongrightarrow> true" and
   falseV:      "false \<longlongrightarrow> false" and
   pairV:       "<a,b> \<longlongrightarrow> <a,b>" and
   lamV:        "\<And>b. lam x. b(x) \<longlongrightarrow> lam x. b(x)" and
 
   caseVtrue:   "\<lbrakk>t \<longlongrightarrow> true; d \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVfalse:  "\<lbrakk>t \<longlongrightarrow> false; e \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVpair:   "\<lbrakk>t \<longlongrightarrow> <a,b>; f(a,b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVlam:    "\<And>b. \<lbrakk>t \<longlongrightarrow> lam x. b(x); g(b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c"
 
   (*** Properties of evaluation: note that "t \<longlongrightarrow> c" impies that c is canonical ***)
 
 axiomatization where
   canonical:  "\<lbrakk>t \<longlongrightarrow> c; c==true \<Longrightarrow> u\<longlongrightarrow>v;
                           c==false \<Longrightarrow> u\<longlongrightarrow>v;
                     \<And>a b. c==<a,b> \<Longrightarrow> u\<longlongrightarrow>v;
                       \<And>f. c==lam x. f(x) \<Longrightarrow> u\<longlongrightarrow>v\<rbrakk> \<Longrightarrow>
              u\<longlongrightarrow>v"
 
   (* Should be derivable - but probably a bitch! *)
 axiomatization where
   substitute: "\<lbrakk>a==a'; t(a)\<longlongrightarrow>c(a)\<rbrakk> \<Longrightarrow> t(a')\<longlongrightarrow>c(a')"
 
   (************** LOGIC ***************)
 
   (*** Definitions used in the following rules ***)
 
 axiomatization where
   bot_def:         "bot == (lam x. x`x)`(lam x. x`x)" and
   apply_def:     "f ` t == case(f, bot, bot, \<lambda>x y. bot, \<lambda>u. u(t))"
 
 definition "fix" :: "(i\<Rightarrow>i)\<Rightarrow>i"
   where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
 
   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
   (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
   (*  behavioural equivalence (ie the relations PO and EQ defined below).            *)
 
 definition SIM :: "[i,i,i set]\<Rightarrow>o"
   where
   "SIM(t,t',R) ==  (t=true \<and> t'=true) | (t=false \<and> t'=false) |
                   (\<exists>a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
                   (\<exists>f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
 
 definition POgen :: "i set \<Rightarrow> i set"
   where "POgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot | SIM(t,t',R))}"
 
 definition EQgen :: "i set \<Rightarrow> i set"
   where "EQgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot \<and> t' = bot | SIM(t,t',R))}"
 
 definition PO :: "i set"
   where "PO == gfp(POgen)"
 
 definition EQ :: "i set"
   where "EQ == gfp(EQgen)"
 
 
   (*** Rules ***)
 
   (** Partial Order **)
 
 axiomatization where
   po_refl:        "a [= a" and
   po_trans:       "\<lbrakk>a [= b;  b [= c\<rbrakk> \<Longrightarrow> a [= c" and
   po_cong:        "a [= b \<Longrightarrow> f(a) [= f(b)" and
 
   (* Extend definition of [= to program fragments of higher type *)
   po_abstractn:   "(\<And>x. f(x) [= g(x)) \<Longrightarrow> (\<lambda>x. f(x)) [= (\<lambda>x. g(x))"
 
   (** Equality - equivalence axioms inherited from FOL.thy   **)
   (**          - congruence of "=" is axiomatised implicitly **)
 
 axiomatization where
   eq_iff:         "t = t' \<longleftrightarrow> t [= t' \<and> t' [= t"
 
   (** Properties of canonical values given by greatest fixed point definitions **)
 
 axiomatization where
   PO_iff:         "t [= t' \<longleftrightarrow> <t,t'> : PO" and
   EQ_iff:         "t =  t' \<longleftrightarrow> <t,t'> : EQ"
 
   (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **)
 
 axiomatization where
   caseBtrue:            "case(true,d,e,f,g) = d" and
   caseBfalse:          "case(false,d,e,f,g) = e" and
   caseBpair:           "case(<a,b>,d,e,f,g) = f(a,b)" and
   caseBlam:       "\<And>b. case(lam x. b(x),d,e,f,g) = g(b)" and
   caseBbot:              "case(bot,d,e,f,g) = bot"           (* strictness *)
 
   (** The theory is non-trivial **)
 axiomatization where
   distinctness:   "\<not> lam x. b(x) = bot"
 
   (*** Definitions of Termination and Divergence ***)
 
 definition Dvg :: "i \<Rightarrow> o"
   where "Dvg(t) == t = bot"
 
 definition Trm :: "i \<Rightarrow> o"
   where "Trm(t) == \<not> Dvg(t)"
 
 text \<open>
 Would be interesting to build a similar theory for a typed programming language:
     ie.     true :: bool,      fix :: ('a\<Rightarrow>'a)\<Rightarrow>'a  etc......
 
 This is starting to look like LCF.
 What are the advantages of this approach?
         - less axiomatic
         - wfd induction / coinduction and fixed point induction available
 \<close>
 
 
 lemmas ccl_data_defs = apply_def fix_def
 
 declare po_refl [simp]
 
 
 subsection \<open>Congruence Rules\<close>
 
 (*similar to AP_THM in Gordon's HOL*)
 lemma fun_cong: "(f::'a\<Rightarrow>'b) = g \<Longrightarrow> f(x)=g(x)"
   by simp
 
 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
 lemma arg_cong: "x=y \<Longrightarrow> f(x)=f(y)"
   by simp
 
 lemma abstractn: "(\<And>x. f(x) = g(x)) \<Longrightarrow> f = g"
   apply (simp add: eq_iff)
   apply (blast intro: po_abstractn)
   done
 
 lemmas caseBs = caseBtrue caseBfalse caseBpair caseBlam caseBbot
 
 
 subsection \<open>Termination and Divergence\<close>
 
 lemma Trm_iff: "Trm(t) \<longleftrightarrow> \<not> t = bot"
   by (simp add: Trm_def Dvg_def)
 
 lemma Dvg_iff: "Dvg(t) \<longleftrightarrow> t = bot"
   by (simp add: Trm_def Dvg_def)
 
 
 subsection \<open>Constructors are injective\<close>
 
 lemma eq_lemma: "\<lbrakk>x=a; y=b; x=y\<rbrakk> \<Longrightarrow> a=b"
   by simp
 
 ML \<open>
   fun inj_rl_tac ctxt rews i =
     let
       fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
       val inj_lemmas = maps mk_inj_lemmas rews
     in
       CHANGED (REPEAT (assume_tac ctxt i ORELSE
         resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
         eresolve_tac ctxt inj_lemmas i ORELSE
         asm_simp_tac (ctxt addsimps rews) i))
     end;
 \<close>
 
 method_setup inj_rl = \<open>
   Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
 \<close>
 
 lemma ccl_injs:
   "<a,b> = <a',b'> \<longleftrightarrow> (a=a' \<and> b=b')"
   "\<And>b b'. (lam x. b(x) = lam x. b'(x)) \<longleftrightarrow> ((ALL z. b(z)=b'(z)))"
   by (inj_rl caseBs)
 
 
 lemma pair_inject: "<a,b> = <a',b'> \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R"
   by (simp add: ccl_injs)
 
 
 subsection \<open>Constructors are distinct\<close>
 
 lemma lem: "t=t' \<Longrightarrow> case(t,b,c,d,e) = case(t',b,c,d,e)"
   by simp
 
 ML \<open>
 local
-  fun pairs_of f x [] = []
+  fun pairs_of _ _ [] = []
     | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)
 
-  fun mk_combs ff [] = []
+  fun mk_combs _ [] = []
     | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs
 
   (* Doesn't handle binder types correctly *)
   fun saturate thy sy name =
-       let fun arg_str 0 a s = s
+       let fun arg_str 0 _ s = s
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
            val T = Sign.the_const_type thy (Sign.intern_const thy sy);
            val arity = length (binder_types T)
        in sy ^ (arg_str arity name "") end
 
   fun mk_thm_str thy a b = "\<not> " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
 
   val lemma = @{thm lem};
   val eq_lemma = @{thm eq_lemma};
   val distinctness = @{thm distinctness};
   fun mk_lemma (ra,rb) =
     [lemma] RL [ra RS (rb RS eq_lemma)] RL
     [distinctness RS @{thm notE}, @{thm sym} RS (distinctness RS @{thm notE})]
 in
   fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
   fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
 end
 \<close>
 
 ML \<open>
 val caseB_lemmas = mk_lemmas @{thms caseBs}
 
 val ccl_dstncts =
   let
     fun mk_raw_dstnct_thm rls s =
       Goal.prove_global \<^theory> [] [] (Syntax.read_prop_global \<^theory> s)
         (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1)
   in map (mk_raw_dstnct_thm caseB_lemmas)
     (mk_dstnct_rls \<^theory> ["bot","true","false","pair","lambda"]) end
 
 fun mk_dstnct_thms ctxt defs inj_rls xs =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun mk_dstnct_thm rls s =
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn _ =>
           rewrite_goals_tac ctxt defs THEN
           simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
 fun mkall_dstnct_thms ctxt defs i_rls xss = maps (mk_dstnct_thms ctxt defs i_rls) xss
 
 (*** Rewriting and Proving ***)
 
 fun XH_to_I rl = rl RS @{thm iffD2}
 fun XH_to_D rl = rl RS @{thm iffD1}
 val XH_to_E = make_elim o XH_to_D
 val XH_to_Is = map XH_to_I
 val XH_to_Ds = map XH_to_D
 val XH_to_Es = map XH_to_E;
 
 ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
 ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
 ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
 \<close>
 
 lemmas [simp] = ccl_rews
   and [elim!] = pair_inject ccl_dstnctsEs
   and [dest!] = ccl_injDs
 
 
 subsection \<open>Facts from gfp Definition of \<open>[=\<close> and \<open>=\<close>\<close>
 
 lemma XHlemma1: "\<lbrakk>A=B; a:B \<longleftrightarrow> P\<rbrakk> \<Longrightarrow> a:A \<longleftrightarrow> P"
   by simp
 
 lemma XHlemma2: "(P(t,t') \<longleftrightarrow> Q) \<Longrightarrow> (<t,t'> : {p. \<exists>t t'. p=<t,t'> \<and>  P(t,t')} \<longleftrightarrow> Q)"
   by blast
 
 
 subsection \<open>Pre-Order\<close>
 
 lemma POgen_mono: "mono(\<lambda>X. POgen(X))"
   apply (unfold POgen_def SIM_def)
   apply (rule monoI)
   apply blast
   done
 
 lemma POgenXH:
   "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
            (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
            (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
   apply (unfold POgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma poXH:
   "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
                  (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
   apply (simp add: PO_iff del: ex_simps)
   apply (rule POgen_mono
     [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def])
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma po_bot: "bot [= b"
   apply (rule poXH [THEN iffD2])
   apply simp
   done
 
 lemma bot_poleast: "a [= bot \<Longrightarrow> a=bot"
   apply (drule poXH [THEN iffD1])
   apply simp
   done
 
 lemma po_pair: "<a,b> [= <a',b'> \<longleftrightarrow>  a [= a' \<and> b [= b'"
   apply (rule poXH [THEN iff_trans])
   apply simp
   done
 
 lemma po_lam: "lam x. f(x) [= lam x. f'(x) \<longleftrightarrow> (ALL x. f(x) [= f'(x))"
   apply (rule poXH [THEN iff_trans])
   apply fastforce
   done
 
 lemmas ccl_porews = po_bot po_pair po_lam
 
 lemma case_pocong:
   assumes 1: "t [= t'"
     and 2: "a [= a'"
     and 3: "b [= b'"
     and 4: "\<And>x y. c(x,y) [= c'(x,y)"
     and 5: "\<And>u. d(u) [= d'(u)"
   shows "case(t,a,b,c,d) [= case(t',a',b',c',d')"
   apply (rule 1 [THEN po_cong, THEN po_trans])
   apply (rule 2 [THEN po_cong, THEN po_trans])
   apply (rule 3 [THEN po_cong, THEN po_trans])
   apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans])
   apply (rule_tac f1 = "\<lambda>d. case (t',a',b',c',d)" in
     5 [THEN po_abstractn, THEN po_cong, THEN po_trans])
   apply (rule po_refl)
   done
 
 lemma apply_pocong: "\<lbrakk>f [= f'; a [= a'\<rbrakk> \<Longrightarrow> f ` a [= f' ` a'"
   unfolding ccl_data_defs
   apply (rule case_pocong, (rule po_refl | assumption)+)
   apply (erule po_cong)
   done
 
 lemma npo_lam_bot: "\<not> lam x. b(x) [= bot"
   apply (rule notI)
   apply (drule bot_poleast)
   apply (erule distinctness [THEN notE])
   done
 
 lemma po_lemma: "\<lbrakk>x=a; y=b; x[=y\<rbrakk> \<Longrightarrow> a[=b"
   by simp
 
 lemma npo_pair_lam: "\<not> <a,b> [= lam x. f(x)"
   apply (rule notI)
   apply (rule npo_lam_bot [THEN notE])
   apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]])
   apply (rule po_refl npo_lam_bot)+
   done
 
 lemma npo_lam_pair: "\<not> lam x. f(x) [= <a,b>"
   apply (rule notI)
   apply (rule npo_lam_bot [THEN notE])
   apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]])
   apply (rule po_refl npo_lam_bot)+
   done
 
 lemma npo_rls1:
   "\<not> true [= false"
   "\<not> false [= true"
   "\<not> true [= <a,b>"
   "\<not> <a,b> [= true"
   "\<not> true [= lam x. f(x)"
   "\<not> lam x. f(x) [= true"
   "\<not> false [= <a,b>"
   "\<not> <a,b> [= false"
   "\<not> false [= lam x. f(x)"
   "\<not> lam x. f(x) [= false"
   by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all,
     (rule po_refl npo_lam_bot)+)+
 
 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
 
 
 subsection \<open>Coinduction for \<open>[=\<close>\<close>
 
 lemma po_coinduct: "\<lbrakk><t,u> : R; R <= POgen(R)\<rbrakk> \<Longrightarrow> t [= u"
   apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]])
    apply assumption+
   done
 
 
 subsection \<open>Equality\<close>
 
 lemma EQgen_mono: "mono(\<lambda>X. EQgen(X))"
   apply (unfold EQgen_def SIM_def)
   apply (rule monoI)
   apply blast
   done
 
 lemma EQgenXH:
   "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |
                                              (t=false \<and> t'=false) |
                  (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
   apply (unfold EQgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma eqXH:
   "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
                      (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                      (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
   apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
     (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : EQ \<and> <b,b'> : EQ) |
     (EX f f'. t=lam x. f (x) \<and> t'=lam x. f' (x) \<and> (ALL x. <f (x) ,f' (x) > : EQ))")
   apply (erule rev_mp)
   apply (simp add: EQ_iff [THEN iff_sym])
   apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1,
     unfolded EQgen_def SIM_def])
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma eq_coinduct: "\<lbrakk><t,u> : R; R <= EQgen(R)\<rbrakk> \<Longrightarrow> t = u"
   apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]])
    apply assumption+
   done
 
 lemma eq_coinduct3:
   "\<lbrakk><t,u> : R;  R <= EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))\<rbrakk> \<Longrightarrow> t = u"
   apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]])
   apply (rule EQgen_mono | assumption)+
   done
 
 method_setup eq_coinduct3 = \<open>
   Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
     SIMPLE_METHOD'
       (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
 \<close>
 
 
 subsection \<open>Untyped Case Analysis and Other Facts\<close>
 
 lemma cond_eta: "(EX f. t=lam x. f(x)) \<Longrightarrow> t = lam x.(t ` x)"
   by (auto simp: apply_def)
 
 lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))"
   apply (cut_tac refl [THEN eqXH [THEN iffD1]])
   apply blast
   done
 
 lemma term_case:
   "\<lbrakk>P(bot); P(true); P(false); \<And>x y. P(<x,y>); \<And>b. P(lam x. b(x))\<rbrakk> \<Longrightarrow> P(t)"
   using exhaustion [of t] by blast
 
 end
diff --git a/src/CCL/Term.thy b/src/CCL/Term.thy
--- a/src/CCL/Term.thy
+++ b/src/CCL/Term.thy
@@ -1,313 +1,308 @@
 (*  Title:      CCL/Term.thy
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Definitions of usual program constructs in CCL\<close>
 
 theory Term
 imports CCL
 begin
 
 definition one :: "i"
   where "one == true"
 
 definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
   where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
 definition inl :: "i\<Rightarrow>i"
   where "inl(a) == <true,a>"
 
 definition inr :: "i\<Rightarrow>i"
   where "inr(b) == <false,b>"
 
 definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
 
 definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
   where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
 
 definition fst :: "i\<Rightarrow>i"
   where "fst(t) == split(t, \<lambda>x y. x)"
 
 definition snd :: "i\<Rightarrow>i"
   where "snd(t) == split(t, \<lambda>x y. y)"
 
 definition thd :: "i\<Rightarrow>i"
   where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
 
 definition zero :: "i"
   where "zero == inl(one)"
 
 definition succ :: "i\<Rightarrow>i"
   where "succ(n) == inr(n)"
 
 definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
   where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
   where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
 
 definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec2 (h, f) ==
     letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
 
 definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec3 (h, f) ==
     letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
       \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
 syntax
   "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
   "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
   "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
     fun letrec_tr [f, x, a, b] =
       Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b;
     fun letrec2_tr [f, x, y, a, b] =
       Syntax.const \<^const_syntax>\<open>letrec2\<close> $ abs_tr x (abs_tr y (abs_tr f a)) $ abs_tr f b;
     fun letrec3_tr [f, x, y, z, a, b] =
       Syntax.const \<^const_syntax>\<open>letrec3\<close> $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b;
   in
     [(\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
      (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
      (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
   end
 \<close>
 print_translation \<open>
   let
     val bound = Syntax_Trans.mark_bound_abs;
 
     fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
       let
         val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
         val (_,a'') = Syntax_Trans.variant_abs'(f,S,a)
         val (x',a') = Syntax_Trans.variant_abs'(x,T,a'')
       in
         Syntax.const \<^syntax_const>\<open>_letrec\<close> $ bound(f',SS) $ bound(x',T) $ a' $ b'
       end;
 
     fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
       let
         val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
         val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a)
         val (y',a2) = Syntax_Trans.variant_abs'(y,U,a1)
         val (x',a') = Syntax_Trans.variant_abs'(x,T,a2)
       in
         Syntax.const \<^syntax_const>\<open>_letrec2\<close> $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ a' $ b'
       end;
 
     fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
       let
         val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
         val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a)
         val (z',a2) = Syntax_Trans.variant_abs'(z,V,a1)
         val (y',a3) = Syntax_Trans.variant_abs'(y,U,a2)
         val (x',a') = Syntax_Trans.variant_abs'(x,T,a3)
       in
         Syntax.const \<^syntax_const>\<open>_letrec3\<close> $
           bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b'
       end;
   in
     [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
      (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
      (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
   end
 \<close>
 
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
 definition nil :: "i"  ("([])")
   where "[] == inl(one)"
 
 definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
   where "h$t == inr(<h,t>)"
 
 definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
 
 definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
 definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
   where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
   and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
 lemmas simp_defs = simp_can_defs simp_ncan_defs
 
 lemmas ind_can_defs = zero_def succ_def nil_def cons_def
   and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def
 lemmas ind_defs = ind_can_defs ind_ncan_defs
 
 lemmas data_defs = simp_defs ind_defs napply_def
   and genrec_defs = letrec_def letrec2_def letrec3_def
 
 
 subsection \<open>Beta Rules, including strictness\<close>
 
 lemma letB: "\<not> t=bot \<Longrightarrow> let x be t in f(x) = f(t)"
   apply (unfold let_def)
   apply (erule rev_mp)
   apply (rule_tac t = "t" in term_case)
-      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+      apply simp_all
   done
 
 lemma letBabot: "let x be bot in f(x) = bot"
-  apply (unfold let_def)
-  apply (rule caseBbot)
-  done
+  unfolding let_def by (rule caseBbot)
 
 lemma letBbbot: "let x be t in bot = bot"
   apply (unfold let_def)
   apply (rule_tac t = t in term_case)
       apply (rule caseBbot)
-     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+     apply simp_all
   done
 
 lemma applyB: "(lam x. b(x)) ` a = b(a)"
-  apply (unfold apply_def)
-  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
-  done
+  by (simp add: apply_def)
 
 lemma applyBbot: "bot ` a = bot"
-  apply (unfold apply_def)
-  apply (rule caseBbot)
-  done
+  unfolding apply_def by (rule caseBbot)
 
 lemma fixB: "fix(f) = f(fix(f))"
   apply (unfold fix_def)
   apply (rule applyB [THEN ssubst], rule refl)
   done
 
-lemma letrecB:
-    "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
+lemma letrecB: "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
   apply (unfold letrec_def)
   apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
   done
 
 lemmas rawBs = caseBs applyB applyBbot
 
 method_setup beta_rl = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (CHANGED o
-      simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))))
+    let val ctxt' = Context_Position.set_visible false ctxt in
+      SIMPLE_METHOD' (CHANGED o
+        simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))
+    end)
 \<close>
 
 lemma ifBtrue: "if true then t else u = t"
   and ifBfalse: "if false then t else u = u"
   and ifBbot: "if bot then t else u = bot"
   unfolding data_defs by beta_rl+
 
 lemma whenBinl: "when(inl(a),t,u) = t(a)"
   and whenBinr: "when(inr(a),t,u) = u(a)"
   and whenBbot: "when(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma splitB: "split(<a,b>,h) = h(a,b)"
   and splitBbot: "split(bot,h) = bot"
   unfolding data_defs by beta_rl+
 
 lemma fstB: "fst(<a,b>) = a"
   and fstBbot: "fst(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma sndB: "snd(<a,b>) = b"
   and sndBbot: "snd(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma thdB: "thd(<a,<b,c>>) = c"
   and thdBbot: "thd(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma ncaseBzero: "ncase(zero,t,u) = t"
   and ncaseBsucc: "ncase(succ(n),t,u) = u(n)"
   and ncaseBbot: "ncase(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma nrecBzero: "nrec(zero,t,u) = t"
   and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"
   and nrecBbot: "nrec(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma lcaseBnil: "lcase([],t,u) = t"
   and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)"
   and lcaseBbot: "lcase(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma lrecBnil: "lrec([],t,u) = t"
   and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"
   and lrecBbot: "lrec(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma letrec2B:
   "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,\<lambda>u v. letrec g x y be h(x,y,g) in g(u,v))"
   unfolding data_defs letrec2_def by beta_rl+
 
 lemma letrec3B:
   "letrec g x y z be h(x,y,z,g) in g(p,q,r) =
     h(p,q,r,\<lambda>u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"
   unfolding data_defs letrec3_def by beta_rl+
 
 lemma napplyBzero: "f^zero`a = a"
   and napplyBsucc: "f^succ(n)`a = f(f^n`a)"
   unfolding data_defs by beta_rl+
 
 lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot
   sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr
   whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc
   nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot
   napplyBzero napplyBsucc
 
 
 subsection \<open>Constructors are injective\<close>
 
 lemma term_injs:
   "(inl(a) = inl(a')) \<longleftrightarrow> (a=a')"
   "(inr(a) = inr(a')) \<longleftrightarrow> (a=a')"
   "(succ(a) = succ(a')) \<longleftrightarrow> (a=a')"
   "(a$b = a'$b') \<longleftrightarrow> (a=a' \<and> b=b')"
   by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
 
 
 subsection \<open>Constructors are distinct\<close>
 
 ML \<open>
 ML_Thms.bind_thms ("term_dstncts",
   mkall_dstnct_thms \<^context> @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
     [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
 \<close>
 
 
 subsection \<open>Rules for pre-order \<open>[=\<close>\<close>
 
 lemma term_porews:
   "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"
   "inr(b) [= inr(b') \<longleftrightarrow> b [= b'"
   "succ(n) [= succ(n') \<longleftrightarrow> n [= n'"
   "x$xs [= x'$xs' \<longleftrightarrow> x [= x' \<and> xs [= xs'"
   by (simp_all add: data_defs ccl_porews)
 
 
 subsection \<open>Rewriting and Proving\<close>
 
 ML \<open>
   ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
 \<close>
 
 lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
 
 lemmas [simp] = term_rews
 lemmas [elim!] = term_dstncts [THEN notE]
 lemmas [dest!] = term_injDs
 
 end
diff --git a/src/CCL/Trancl.thy b/src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy
+++ b/src/CCL/Trancl.thy
@@ -1,209 +1,206 @@
 (*  Title:      CCL/Trancl.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Transitive closure of a relation\<close>
 
 theory Trancl
 imports CCL
 begin
 
 definition trans :: "i set \<Rightarrow> o"  (*transitivity predicate*)
   where "trans(r) == (ALL x y z. <x,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <x,z>:r)"
 
 definition id :: "i set"  (*the identity relation*)
   where "id == {p. EX x. p = <x,x>}"
 
 definition relcomp :: "[i set,i set] \<Rightarrow> i set"  (infixr "O" 60)  (*composition of relations*)
   where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
 
 definition rtrancl :: "i set \<Rightarrow> i set"  ("(_^*)" [100] 100)
   where "r^* == lfp(\<lambda>s. id Un (r O s))"
 
 definition trancl :: "i set \<Rightarrow> i set"  ("(_^+)" [100] 100)
   where "r^+ == r O rtrancl(r)"
 
 
 subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close>
 
 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)"
   unfolding trans_def by blast
 
 lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r"
   unfolding trans_def by blast
 
 
 subsection \<open>Identity relation\<close>
 
 lemma idI: "<a,a> : id"
   apply (unfold id_def)
   apply (rule CollectI)
   apply (rule exI)
   apply (rule refl)
   done
 
 lemma idE: "\<lbrakk>p: id;  \<And>x. p = <x,x> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (unfold id_def)
   apply (erule CollectE)
   apply blast
   done
 
 
 subsection \<open>Composition of two relations\<close>
 
 lemma compI: "\<lbrakk><a,b>:s; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c> : r O s"
   unfolding relcomp_def by blast
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
 lemma compE: "\<lbrakk>xz : r O s; \<And>x y z. \<lbrakk>xz = <x,z>; <x,y>:s; <y,z>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   unfolding relcomp_def by blast
 
 lemma compEpair: "\<lbrakk><a,c> : r O s; \<And>y. \<lbrakk><a,y>:s; <y,c>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (erule compE)
   apply (simp add: pair_inject)
   done
 
 lemmas [intro] = compI idI
   and [elim] = compE idE
-  and [elim!] = pair_inject
 
 lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)"
   by blast
 
 
 subsection \<open>The relation rtrancl\<close>
 
 lemma rtrancl_fun_mono: "mono(\<lambda>s. id Un (r O s))"
   apply (rule monoI)
   apply (rule monoI subset_refl comp_mono Un_mono)+
   apply assumption
   done
 
 lemma rtrancl_unfold: "r^* = id Un (r O r^*)"
   by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]])
 
 (*Reflexivity of rtrancl*)
 lemma rtrancl_refl: "<a,a> : r^*"
   apply (subst rtrancl_unfold)
   apply blast
   done
 
 (*Closure under composition with r*)
 lemma rtrancl_into_rtrancl: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^*"
   apply (subst rtrancl_unfold)
   apply blast
   done
 
 (*rtrancl of r contains r*)
 lemma r_into_rtrancl: "<a,b> : r \<Longrightarrow> <a,b> : r^*"
   apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
   apply assumption
   done
 
 
 subsection \<open>standard induction rule\<close>
 
 lemma rtrancl_full_induct:
   "\<lbrakk><a,b> : r^*;
       \<And>x. P(<x,x>);
       \<And>x y z. \<lbrakk>P(<x,y>); <x,y>: r^*; <y,z>: r\<rbrakk>  \<Longrightarrow> P(<x,z>)\<rbrakk>
    \<Longrightarrow>  P(<a,b>)"
   apply (erule def_induct [OF rtrancl_def])
    apply (rule rtrancl_fun_mono)
   apply blast
   done
 
 (*nice induction rule*)
 lemma rtrancl_induct:
   "\<lbrakk><a,b> : r^*;
       P(a);
       \<And>y z. \<lbrakk><a,y> : r^*; <y,z> : r;  P(y)\<rbrakk> \<Longrightarrow> P(z) \<rbrakk>
     \<Longrightarrow> P(b)"
 (*by induction on this formula*)
   apply (subgoal_tac "ALL y. <a,b> = <a,y> \<longrightarrow> P(y)")
 (*now solve first subgoal: this formula is sufficient*)
   apply blast
 (*now do the induction*)
   apply (erule rtrancl_full_induct)
    apply blast
   apply blast
   done
 
 (*transitivity of transitive closure!! -- by induction.*)
 lemma trans_rtrancl: "trans(r^*)"
   apply (rule transI)
   apply (rule_tac b = z in rtrancl_induct)
     apply (fast elim: rtrancl_into_rtrancl)+
   done
 
 (*elimination of rtrancl -- by induction on a special formula*)
 lemma rtranclE:
   "\<lbrakk><a,b> : r^*; a = b \<Longrightarrow> P; \<And>y. \<lbrakk><a,y> : r^*; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (subgoal_tac "a = b | (EX y. <a,y> : r^* \<and> <y,b> : r)")
    prefer 2
    apply (erule rtrancl_induct)
     apply blast
    apply blast
   apply blast
   done
 
 
 subsection \<open>The relation trancl\<close>
 
 subsubsection \<open>Conversions between trancl and rtrancl\<close>
 
 lemma trancl_into_rtrancl: "<a,b> : r^+ \<Longrightarrow> <a,b> : r^*"
   apply (unfold trancl_def)
   apply (erule compEpair)
   apply (erule rtrancl_into_rtrancl)
   apply assumption
   done
 
 (*r^+ contains r*)
 lemma r_into_trancl: "<a,b> : r \<Longrightarrow> <a,b> : r^+"
   unfolding trancl_def by (blast intro: rtrancl_refl)
 
 (*intro rule by definition: from rtrancl and r*)
 lemma rtrancl_into_trancl1: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^+"
   unfolding trancl_def by blast
 
 (*intro rule from r and rtrancl*)
 lemma rtrancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^*\<rbrakk> \<Longrightarrow> <a,c> : r^+"
   apply (erule rtranclE)
    apply (erule subst)
    apply (erule r_into_trancl)
   apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1])
     apply (assumption | rule r_into_rtrancl)+
   done
 
 (*elimination of r^+ -- NOT an induction rule*)
 lemma tranclE:
   "\<lbrakk><a,b> : r^+;
     <a,b> : r \<Longrightarrow> P;
     \<And>y. \<lbrakk><a,y> : r^+; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ \<and> <y,b> : r)")
    apply blast
   apply (unfold trancl_def)
   apply (erule compEpair)
   apply (erule rtranclE)
    apply blast
   apply (blast intro!: rtrancl_into_trancl1)
   done
 
 (*Transitivity of r^+.
   Proved by unfolding since it uses transitivity of rtrancl. *)
 lemma trans_trancl: "trans(r^+)"
   apply (unfold trancl_def)
   apply (rule transI)
   apply (erule compEpair)+
   apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]])
     apply assumption+
   done
 
 lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
-  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
-   apply assumption+
-  done
+  by (rule r_into_trancl [THEN trans_trancl [THEN transD]])
 
 end