# HG changeset patch
# User urbanc
# Date 1210970125 -7200
# Node ID 19d8783a30de8b7e74135ce1a775eba628803a10
# Parent  ce964f0df281237994a175a1321c3d1e215013a4
added a lemma about existence of contexts

diff -r ce964f0df281 -r 19d8783a30de src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Fri May 16 21:56:13 2008 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri May 16 22:35:25 2008 +0200
@@ -141,8 +141,13 @@
   then show  "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
 qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
 
+lemma ctx_existence:
+  assumes a: "t \<longrightarrow>o t'"
+  shows "\<exists>C s s'. t = C\<lbrakk>s\<rbrakk> \<and> t' = C\<lbrakk>s'\<rbrakk> \<and> s \<longrightarrow>o s'"
+using a
+by (induct) (metis cong_red.intros filling.simps)+
 
-section {* We now use context in a CBV list machine. *}
+section {* We now use context in a CBV list machine *}
 
 text {* First, a function that composes a list of contexts. *}