# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307107904 -32400
# Node ID 812cfadeb8b743d61e8f3e3e13293a8b721ae032
# Parent  887d8bd4eb99ca7e659a83be5aa22fe958208831
FiniteSupp precondition in the function is enough to get rid of completeness obligationss

diff -r 887d8bd4eb99 -r 812cfadeb8b7 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Fri Jun 03 12:46:23 2011 +0100
+++ b/Nominal/Ex/Lambda_F_T.thy	Fri Jun 03 22:31:44 2011 +0900
@@ -137,3 +137,26 @@
 apply (simp add: eqvts permute_pure)
 done
 
+lemma lam_strong_exhaust2:
+  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
+    \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
+    \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
+    finite (supp c)\<rbrakk>
+    \<Longrightarrow> P"
+sorry
+
+nominal_primrec
+  g
+where
+  "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
+| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
+| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
+| "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
+  apply (simp add: eqvt_def g_graph_def)
+  apply (rule, perm_simp, rule)
+  apply (case_tac x)
+  apply (case_tac "finite (supp (a, b, c))")
+  prefer 2
+  apply simp
+  apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
+  apply simp_all