--- a/Nominal/Ex/SFT/Lambda.thy Fri Jun 24 10:30:06 2011 +0900
+++ b/Nominal/Ex/SFT/Lambda.thy Fri Jun 24 10:54:31 2011 +0900
@@ -52,19 +52,19 @@
by (relation "measure (\<lambda>(t,_,_). size t)")
(simp_all add: lam.size)
-lemma subst4[eqvt]:
+lemma subst_eqvt[eqvt]:
shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
by (induct t x s rule: subst.induct) (simp_all)
-lemma subst1[simp]:
+lemma forget[simp]:
shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
by (nominal_induct t avoiding: x s rule: lam.strong_induct)
(auto simp add: lam.fresh fresh_at_base)
-lemma subst2[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
+lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
by (simp add: fresh_def)
-lemma subst3[simp]: "M [x ::= V x] = M"
+lemma subst_id[simp]: "M [x ::= V x] = M"
by (rule_tac lam="M" and c="x" in lam.strong_induct)
(simp_all add: fresh_star_def lam.fresh fresh_Pair)
--- a/Nominal/Ex/SFT/Theorem.thy Fri Jun 24 10:30:06 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy Fri Jun 24 10:54:31 2011 +0900
@@ -1,10 +1,8 @@
header {* The main lemma about Num and the Second Fixed Point Theorem *}
theory Theorem imports Consts begin
-(*<*)
lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6
lemmas app = Ltgt1_app
-(*>*)
lemma Num:
shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
@@ -67,4 +65,5 @@
also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..
finally show ?thesis by blast
qed
-(*>*)
+
+end