# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289814749 0
# Node ID f0252365936ca69c8f0faba01ec3b74ba0c34549
# Parent  1c77e15c4259d6bfebfc9d0aafef41160a369746
proved that bn functions return a finite set

diff -r 1c77e15c4259 -r f0252365936c Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Nov 15 09:52:29 2010 +0000
@@ -7,6 +7,7 @@
   binding function
 *}
 
+
 atom_decl name
 
 nominal_datatype foo: trm =
@@ -49,6 +50,7 @@
 thm foo.fsupp
 thm foo.supp
 thm foo.fresh
+thm foo.bn_finite
 
 lemma uu1:
   shows "alpha_bn1 as (permute_bn1 p as)"
@@ -124,13 +126,6 @@
 apply(simp add: atom_eqvt insert_eqvt)
 done
 
-lemma bn_finite:
-  shows "(\<lambda>x. True) t"
-  and  "finite (set (bn1 as)) \<and> finite (set (bn2 as)) \<and> finite (set (bn3 as))"
-  and  "finite (bn4 as')"
-apply(induct "t::trm" and as and as' rule: foo.inducts)
-apply(simp_all add: foo.bn_defs)
-done
 
 
 lemma strong_exhaust1:
@@ -154,6 +149,7 @@
 apply(rule assms(3))
 apply(perm_simp)
 apply(assumption)
+apply(simp)
 apply(drule supp_perm_eq[symmetric])
 apply(perm_simp)
 apply(simp)
@@ -216,12 +212,13 @@
 apply(simp)
 apply(simp add: tt4 uu4)
 apply(rule at_set_avoiding2)
-apply(simp add: bn_finite)
+apply(simp add: foo.bn_finite)
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: Abs_fresh_star)
 done
 
+
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
   shows "P"
diff -r 1c77e15c4259 -r f0252365936c Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Mon Nov 15 09:52:29 2010 +0000
@@ -3,11 +3,13 @@
 begin
 
 atom_decl name
-declare [[STEPS = 100]]
 
 class s1
 class s2
 
+instance nat :: s1 ..
+instance int :: s2 .. 
+
 nominal_datatype ('a, 'b) lam =
   Var "name"
 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
diff -r 1c77e15c4259 -r f0252365936c Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Nov 15 09:52:29 2010 +0000
@@ -586,6 +586,12 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
+  (* proving that the qbn result is finite *)
+  val qbn_finite_thms =
+    if get_STEPS lthy > 33
+    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
+    else []
+
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
@@ -632,6 +638,7 @@
      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
+     ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
diff -r 1c77e15c4259 -r f0252365936c Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -145,12 +145,6 @@
     else raise TERM ("listify", [t])
   end
 
-(* coerces a list into a set *)
-fun to_set t =
-  if fastype_of t = @{typ "atom list"}
-  then @{term "set :: atom list => atom set"} $ t
-  else t
-
 
 (** functions that construct the equations for fv and fv_bn **)
 
diff -r 1c77e15c4259 -r f0252365936c Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -15,6 +15,9 @@
 
   val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> 
     thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
+
+  val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
+
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -145,7 +148,7 @@
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
-  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
+  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 
 fun p_tac msg i = 
   if false then print_tac ("ptest: " ^ msg) else all_tac
@@ -189,5 +192,22 @@
   end
 
 
+fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
+  let
+    fun mk_goal qbn = 
+      let
+        val arg_ty = domain_type (fastype_of qbn)
+        val finite = @{term "finite :: atom set => bool"}
+      in
+        (arg_ty, fn x => finite $ (to_set (qbn $ x)))
+      end
+
+    val props = map mk_goal qbns
+    val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
+      @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
+  in
+    induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt
+  end
+
 
 end (* structure *)
diff -r 1c77e15c4259 -r f0252365936c Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -49,7 +49,6 @@
   val mk_finite_ty: typ -> term -> term
   val mk_finite: term -> term
 
-
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -61,6 +60,8 @@
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
+  val to_set: term -> term
+
   (* fresh arguments for a term *)
   val fresh_args: Proof.context -> term -> term list
 
@@ -185,6 +186,13 @@
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
 
+(* coerces a list into a set *)
+fun to_set t =
+  if fastype_of t = @{typ "atom list"}
+  then @{term "set :: atom list => atom set"} $ t
+  else t
+
+
 (* produces fresh arguments for a term *)
 
 fun fresh_args ctxt f =