# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1292191751 0
# Node ID 86e3b39c2a6061984aa0c1c3179f3644cba629cd
# Parent  7430e07a5d619bfd7f44be0fbd80b5e45a5789a3
created strong_exhausts terms

diff -r 7430e07a5d61 -r 86e3b39c2a60 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Dec 12 22:09:11 2010 +0000
@@ -24,6 +24,8 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+thm foo.exhaust
+
 ML {* 
   Variable.import;
   Variable.import true @{thms foo.exhaust} @{context}
diff -r 7430e07a5d61 -r 86e3b39c2a60 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 12 22:09:11 2010 +0000
@@ -18,60 +18,104 @@
 text {* TEST *}
 
 ML {*
-fun strip_prems_concl trm =
-  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+fun list_implies_rev concl trms = Logic.list_implies (trms, concl)
+
+fun mk_all (a, T) t = Const ("all", (T --> propT) --> propT) $ Abs (a, T, t)
+
+fun strip_prems_concl (Const("==>", _) $ A $ B) = strip_prems_concl B |>> cons A
+  | strip_prems_concl B = ([], B) 
 
 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
   | strip_outer_params B = ([], B)
+
+fun strip_params_prems_concl trm =
+  let
+    val (params, body) = strip_outer_params trm
+    val (prems, concl) = strip_prems_concl body
+  in
+    (params, prems, concl)
+  end
+
+fun list_params_prems_concl params prems concl =
+  Logic.list_implies (prems, concl)
+  |> fold_rev mk_all params
+
+
+fun mk_binop_env tys c (t, u) =
+  let val ty = fastype_of1 (tys, t) in
+    Const (c, [ty, ty] ---> ty) $ t $ u
+  end
+
+fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1
+  | mk_union_env tys (@{term "{}::atom set"}, t2) = t2
+  | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
+  | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
+  | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  
+
+fun fold_union_env tys trms = fold_rev (curry (mk_union_env tys)) trms @{term "{}::atom set"}
+
 *}
 
 
 ML {*
-fun binders bclauses = 
+fun process_ecase lthy c (params, prems, concl) bclauses =
   let
-    fun aux1 (NONE, i) = Bound i 
-      | aux1 (SOME bn, i) = bn $ Bound i         
+    fun binder tys (opt, i) = 
+      let
+        val t = Bound (length tys - i - 1)
+      in
+        case opt of
+          NONE => setify_ty lthy (nth tys i) t 
+        | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   
+      end 
+
+    val param_tys = map snd params
+       
+    val fresh_prem = 
+      case (get_all_binders bclauses) of
+        [] => []                              (* case: no binders *)
+      | binders => binders                    (* case: binders *) 
+          |> map (binder param_tys)
+          |> fold_union_env param_tys
+          |> (fn t => mk_fresh_star t c)
+          |> HOLogic.mk_Trueprop
+          |> single 
   in
-    bclauses
-    |> map (fn (BC (_, x, _)) => x)
-    |> flat
-    |> map aux1
-  end
+    list_params_prems_concl params (fresh_prem @ prems) concl
+  end  
 *}
 
+
 ML {*
-fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
+fun mk_strong_exhausts_goal lthy qexhausts bclausesss =
   let
     val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
 
     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c = Free (c, TFree (a, @{sort fs}))
 
-    val (cses, main_concls) = qexhausts'
+    val (ecases, main_concls) = qexhausts'
       |> map prop_of
       |> map strip_prems_concl
       |> split_list
+      |>> map (map strip_params_prems_concl)            
+  in
+    map2 (map2 (process_ecase lthy'' c)) ecases bclausesss
+    |> map2 list_implies_rev main_concls
+    |> rpair lthy''
+  end
 
-    fun process_case cse bclauses =
-      let
-        val (params, (body, concl)) = cse
-          |> strip_outer_params
-          ||> Logic.dest_implies
-        
-        (*val bnds = HOLogic.mk_tuple (binders bclauses)*)
-        val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c))
-      in
-        Logic.mk_implies (prem, Logic.mk_implies (body, concl)) 
-      end  
-  
-    val cses' = map2 (map2 process_case) cses bclausess
-      |> map (map (Syntax.string_of_term lthy''))
-      |> map commas
+fun prove_strong_exhausts lthy qexhausts qtrms bclausesss =
+  let
+    val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss
+
+    val _ = goal
+      |> map (Syntax.check_term lthy')
+      |> map (Syntax.string_of_term lthy')
       |> cat_lines
-
-    val _ = tracing ("cases\n " ^ cses')
+      |> tracing
   in
-    ()
+    @{thms TrueI}
   end
 *}
 
@@ -230,9 +274,6 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("bclauses\n" ^ cat_lines (map @{make_string} bclauses))
-  val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses))
-
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
diff -r 7430e07a5d61 -r 86e3b39c2a60 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 22:09:11 2010 +0000
@@ -13,11 +13,12 @@
   (* info of raw binding functions *)
   type bn_info = term * int * (int * term option) list list
 
-  
   (* binding modes and binding clauses *)
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
+  val get_all_binders: bclause list -> (term option * int) list
+
   val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
     (term list * thm list * bn_info list * thm list * local_theory) 
@@ -57,6 +58,12 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
+fun get_all_binders bclauses = 
+  bclauses
+  |> map (fn (BC (_, x, _)) => x) 
+  |> flat
+  |> remove_dups (op =)
+
 fun lookup xs x = the (AList.lookup (op=) xs x)
 
 
diff -r 7430e07a5d61 -r 86e3b39c2a60 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/nominal_library.ML	Sun Dec 12 22:09:11 2010 +0000
@@ -8,6 +8,7 @@
 sig
   val last2: 'a list -> 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
+  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
 
   val is_true: term -> bool
  
@@ -47,14 +48,18 @@
   val is_atom_fset: Proof.context -> typ -> bool
   val is_atom_list: Proof.context -> typ -> bool
 
+  val to_atom_set: term -> term
+  val to_set_ty: typ -> term -> term
+  val to_set: term -> term
+  
   val setify_ty: Proof.context -> typ -> term -> term
   val setify: Proof.context -> term -> term
   val listify_ty: Proof.context -> typ -> term -> term
   val listify: Proof.context -> term -> term
 
-  val fresh_ty: typ -> typ -> typ
-  val fresh_star_const: typ -> typ -> term
-  val mk_fresh_star_ty: typ -> typ -> term -> term -> term
+  val fresh_star_ty: typ -> typ
+  val fresh_star_const: typ -> term
+  val mk_fresh_star_ty: typ -> term -> term -> term
   val mk_fresh_star: term -> term -> term
 
   val supp_ty: typ -> typ
@@ -86,8 +91,6 @@
   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
 
@@ -121,6 +124,13 @@
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys
 
+fun remove_dups eq [] = []
+  | remove_dups eq (x::xs) = 
+      if (member eq xs x) 
+      then remove_dups eq xs 
+      else x::(remove_dups eq xs)
+
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
@@ -206,19 +216,27 @@
 fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t
 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
 
+(* coerces a list into a set *)
+fun to_atom_set t = @{term "set :: atom list => atom set"} $ t
+  
+fun to_set_ty ty t =
+  if ty = @{typ "atom list"}
+  then to_atom_set t else t
+
+fun to_set t = to_set_ty (fastype_of t) t
 
 
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty
   | is_atom_set _ _ = false;
 
-fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty
   | is_atom_fset _ _ = false;
 
-fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty
   | is_atom_list _ _ = false
 
 
@@ -231,8 +249,11 @@
     then mk_atom_set_ty ty t
   else if is_atom_fset ctxt ty
     then mk_atom_fset_ty ty t
+  else if is_atom_list ctxt ty
+    then to_atom_set (mk_atom_list_ty ty t)
   else raise TERM ("setify", [t])
 
+
 (* functions that coerces singletons and lists of concrete atoms
    into lists of general atoms  *)
 fun listify_ty ctxt ty t =
@@ -245,10 +266,10 @@
 fun setify ctxt t = setify_ty ctxt (fastype_of t) t
 fun listify ctxt t = listify_ty ctxt (fastype_of t) t
 
-fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool}
-fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2)
-fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2
-fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2
+fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool}
+fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty)
+fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2
+fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2
 
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
@@ -302,15 +323,6 @@
 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 =