# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269512185 -3600
# Node ID 0e705352bcef61afcf37a991bfcdb8fbf24ad5ea
# Parent  953403c5faa01990f2984cd51e660a2a393091de
Properly defined permute_bn. No more sorry's in Let strong induction.

diff -r 953403c5faa0 -r 0e705352bcef Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Mar 25 11:10:15 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 11:16:25 2010 +0100
@@ -30,19 +30,35 @@
 thm trm_lts.distinct
 thm trm_lts.fv[simplified trm_lts.supp]
 
-consts
-  permute_bn :: "perm \<Rightarrow> lts \<Rightarrow> lts"
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
+| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "permute_bn_raw"
 
-lemma test:
-  "permute_bn pi (Lnil) = Lnil"
-  "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)"
-  sorry
+lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+  apply simp_all
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma permute_bn_zero:
   "permute_bn 0 a = a"
   apply(induct a rule: trm_lts.inducts(2))
   apply(rule TrueI)
-  apply(simp_all add:test eqvts)
+  apply(simp_all add:permute_bn eqvts)
   done
 
 lemma permute_bn_add:
@@ -52,14 +68,14 @@
 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
   apply(induct lts rule: trm_lts.inducts(2))
   apply(rule TrueI)
-  apply(simp_all add:test eqvts trm_lts.eq_iff)
+  apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
   done
 
 lemma perm_bn:
   "p \<bullet> bn l = bn(permute_bn p l)"
   apply(induct l rule: trm_lts.inducts(2))
   apply(rule TrueI)
-  apply(simp_all add:test eqvts)
+  apply(simp_all add:permute_bn eqvts)
   done
 
 lemma Lt_subst:
@@ -83,7 +99,7 @@
 lemma fin_bn:
   "finite (bn l)"
   apply(induct l rule: trm_lts.inducts(2))
-  apply(simp_all add:test eqvts)
+  apply(simp_all add:permute_bn eqvts)
   done
 
 lemma 
@@ -144,9 +160,9 @@
     apply(rule finite_Diff)
     apply(simp add: finite_supp)
     apply(simp add: fresh_star_def fresh_def supp_Abs)
-    apply(simp add: eqvts test)
+    apply(simp add: eqvts permute_bn)
     apply(rule a5)
-    apply(simp add: test)
+    apply(simp add: permute_bn)
     apply(rule a6)
     apply simp
     apply simp