# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308880471 -32400
# Node ID 8ec94871de1e910465ee90dbea4847c228ff68c6
# Parent  589b1a0c75e6dc915ee2b242477eaf740105bf10
More usual names for substitution properties

diff -r 589b1a0c75e6 -r 8ec94871de1e Nominal/Ex/SFT/Lambda.thy
--- 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)
 
diff -r 589b1a0c75e6 -r 8ec94871de1e Nominal/Ex/SFT/Theorem.thy
--- 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