--- 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);
--- 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"
--- 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