# HG changeset patch
# User wenzelm
# Date 1633363975 -7200
# Node ID 63a697f1fb8f6b25a4fd2e9d5e99dfca2424ae09
# Parent  30995552ea4ca4188b11b66b7cd71d93e66e79f5
tuned proofs;
fewer warnings;

diff -r 30995552ea4c -r 63a697f1fb8f src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Mon Oct 04 18:02:04 2021 +0200
+++ b/src/CCL/CCL.thy	Mon Oct 04 18:12:55 2021 +0200
@@ -232,15 +232,15 @@
 
 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);
diff -r 30995552ea4c -r 63a697f1fb8f src/CCL/Term.thy
--- a/src/CCL/Term.thy	Mon Oct 04 18:02:04 2021 +0200
+++ b/src/CCL/Term.thy	Mon Oct 04 18:12:55 2021 +0200
@@ -159,38 +159,31 @@
   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
@@ -199,8 +192,10 @@
 
 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"
diff -r 30995552ea4c -r 63a697f1fb8f src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Mon Oct 04 18:02:04 2021 +0200
+++ b/src/CCL/Trancl.thy	Mon Oct 04 18:12:55 2021 +0200
@@ -66,7 +66,6 @@
 
 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
@@ -202,8 +201,6 @@
   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