# HG changeset patch
# User urbanc
# Date 1173772198 -3600
# Node ID 7e4f4f19002f9d0e52daf32e39a79e8ad6e23293
# Parent  b709739c69e65b0c56fbf9274296f1512581baa2
deleted function for defining candidates and used nominal_primrec instead

diff -r b709739c69e6 -r 7e4f4f19002f src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Mon Mar 12 19:23:49 2007 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Tue Mar 13 08:49:58 2007 +0100
@@ -502,38 +502,15 @@
 
 section {* Candidates *}
 
-lemma ty_cases:
-  fixes x::ty
-  shows "(\<exists>X. x= TVar X) \<or> (\<exists>T1 T2. x=T1\<rightarrow>T2)"
-by (induct x rule: ty.induct_weak) (auto)
-
-function
+consts
   RED :: "ty \<Rightarrow> lam set"
-where
+
+nominal_primrec
   "RED (TVar X) = {t. SN(t)}"
-| "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
-apply(auto simp add: ty.inject)
-apply(subgoal_tac "(\<exists>X. x= TVar X) \<or> (\<exists>T1 T2. x=T1\<rightarrow>T2)")
-apply(blast)
-apply(rule ty_cases)
+  "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
+apply(rule TrueI)+
 done
 
-instance ty :: size ..
-
-nominal_primrec
-  "size (TVar X) = 1"
-  "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
-by (rule TrueI)+
-
-lemma ty_size_greater_zero[simp]:
-  fixes T::"ty"
-  shows "size T > 0"
-by (nominal_induct T rule: ty.induct) (simp_all)
-
-termination
-apply(relation "measure size") 
-apply(auto)
-done
 
 constdefs
   NEUT :: "lam \<Rightarrow> bool"