# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265185521 -3600
# Node ID 135bf399c036aca00ff34c492cebf8cc95fbd763
# Parent  bcf6e7d20c20a8d77eea9cebb15e1f0112732123
The trm1_support lemma explicitly and stated a strong induction principle.

diff -r bcf6e7d20c20 -r 135bf399c036 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 08:32:24 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 09:25:21 2010 +0100
@@ -336,6 +336,21 @@
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
 
+lemma trm1_supp:
+  "supp (Vr1 x) = {atom x}"
+  "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
+  "supp (Lm1 x t) = (supp t) - {atom x}"
+  "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
+  by (simp_all only: supp_fv fv_trm1)
+
+lemma trm1_induct_strong:
+  assumes "\<And>name b. P b (Vr1 name)"
+  and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
+  and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
+  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
+  shows   "P a rtrma"
+
+
 section {*** lets with single assignments ***}
 
 datatype trm2 =