# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268326049 -3600
# Node ID 4029105011cab324cb4aec532735eb4c018a5e0e
# Parent  b355cab42841f77f473b83d2d1682cb0250dfbce
Show that the new types are in finite support typeclass.

diff -r b355cab42841 -r 4029105011ca Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -119,7 +119,7 @@
     fold (fn a => fn b =>
       if a = @{term True} then b else
       if b = @{term True} then a else
-      HOLogic.mk_conj (a, b)) props @{term True};
+      HOLogic.mk_conj (a, b)) (rev props) @{term True};
   fun mk_diff a b =
     if b = noatoms then a else
     if b = a then noatoms else
@@ -718,17 +718,21 @@
 *}
 
 ML {*
-fun mk_supports_eq cnstr =
+fun mk_supp ty x =
+  Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+*}
+
+ML {*
+fun mk_supports_eq thy cnstr =
 let
   val (tys, ty) = (strip_type o fastype_of) cnstr
   val names = Datatype_Prop.make_tnames tys
   val frees = map Free (names ~~ tys)
   val rhs = list_comb (cnstr, frees)
-  fun mk_supp ty x =
-    Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+
   fun mk_supp_arg (x, ty) =
-    if is_atom @{theory} ty then mk_supp @{typ atom} (mk_atom ty $ x) else
-    if is_atom_set @{theory} ty then mk_supp @{typ "atom set"} (mk_atoms x)
+    if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atoms x)
     else mk_supp ty x
   val lhss = map mk_supp_arg (frees ~~ tys)
   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
@@ -738,4 +742,40 @@
 end
 *}
 
+ML {*
+fun prove_supports ctxt perms cnst =
+let
+  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+in
+  Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
 end
+*}
+
+ML {*
+fun mk_fs tys =
+let
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val supps = map2 mk_supp tys frees
+  val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
+in
+  (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
+end
+*}
+
+ML {*
+fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
+  rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un})
+*}
+
+ML {*
+fun prove_fs ctxt induct supports tys =
+let
+  val (names, eq) = mk_fs tys
+in
+  Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
+end
+*}
+
+end
diff -r b355cab42841 -r 4029105011ca Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -283,6 +283,7 @@
 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 
+
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
@@ -304,7 +305,7 @@
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
   val rel_dtinfos = List.take (dtinfos, (length dts));
   val inject = flat (map #inject dtinfos);
-  val distinct = flat (map #distinct dtinfos);
+  val distincts = flat (map #distinct dtinfos);
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
@@ -331,7 +332,7 @@
   val alpha_intros = #intrs alpha;
   val alpha_cases_loc = #elims alpha
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
-  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
+  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
@@ -362,7 +363,11 @@
         Const (cname, map (typ_of_dtyp descr sorts) dts --->
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
-  val (consts, const_defs) = split_list consts_defs;
+  val (consts_loc, const_defs) = split_list consts_defs;
+  val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7;
+  val consts = map (Morphism.term morphism_8_7) consts_loc;
+  (* Could be done nicer *)
+  val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -406,8 +411,15 @@
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+  val supports = map (prove_supports lthy20 q_perm) consts
+  val _ = map tracing (map PolyML.makestring supports);
+  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
+  val thy3 = Local_Theory.exit_global lthy20;
+  val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
+  fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
+  val lthy22 = Class.prove_instantiation_instance tac lthy21;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22)
 end
 *}
 
diff -r b355cab42841 -r 4029105011ca Nominal/Term1.thy
--- a/Nominal/Term1.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Term1.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -137,11 +137,7 @@
   "{} supports BUnit"
   "(supp (atom x)) supports (BVr x)"
   "(supp a \<union> supp b) supports (BPr a b)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
-apply(rule_tac [!] allI)+
-apply(rule_tac [!] impI)
-apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
-apply(simp_all add: fresh_atom)
+apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
 lemma rtrm1_bp_fs:
diff -r b355cab42841 -r 4029105011ca Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -4,6 +4,8 @@
 
 text {* example 1, equivalent to example 2 from Terms *}
 
+atom_decl name
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -21,6 +23,9 @@
 thm lam_bp_perm
 thm lam_bp_induct
 thm lam_bp_distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+
+term "supp (x :: lam)"
 
 (* compat should be
 compat (BP x t) pi (BP x' t')