# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324445105 -32400
# Node ID 3750c08f627e5da9ec214ba6952d9bcd2a5f599a
# Parent  25d813c5042d843687e3f848cdf5c361aef8d16e
Remove transitivity from the definition of One_star and show it instead.

diff -r 25d813c5042d -r 3750c08f627e Nominal/Ex/CR.thy
--- a/Nominal/Ex/CR.thy	Wed Dec 21 13:06:09 2011 +0900
+++ b/Nominal/Ex/CR.thy	Wed Dec 21 14:25:05 2011 +0900
@@ -17,7 +17,7 @@
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
-  apply(auto simp add: lam.distinct lam.eq_iff)
+  apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
@@ -211,9 +211,15 @@
 inductive
   One_star :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>1* _" [80,80] 80)
 where
-  os1[intro]: "t \<longrightarrow>1* t"
-| os2[intro]: "t \<longrightarrow>1 s \<Longrightarrow> t \<longrightarrow>1* s"
-| os3[intro, trans]: "t1 \<longrightarrow>1* t2 \<Longrightarrow> t2 \<longrightarrow>1* t3 \<Longrightarrow> t1 \<longrightarrow>1* t3"
+  os1[intro, simp]: "t \<longrightarrow>1* t"
+| os2[intro]: "t \<longrightarrow>1* r \<Longrightarrow> r \<longrightarrow>1 s \<Longrightarrow> t \<longrightarrow>1* s"
+
+lemma os3[intro, trans]:
+  assumes a1: "M1 \<longrightarrow>1* M2"
+  and     a2: "M2 \<longrightarrow>1* M3"
+  shows "M1 \<longrightarrow>1* M3"
+  using a2 a1
+  by induct auto
 
 section {* Complete Development Reduction *}