# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1291828028 0
# Node ID 90779aefbf1ac75b2076d57081fed8600dd2d8a2
# Parent  bcf558c445a4386919a688292f486e519cee5065
first tests about exhaust

diff -r bcf558c445a4 -r 90779aefbf1a Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Wed Dec 08 13:16:25 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Wed Dec 08 17:07:08 2010 +0000
@@ -24,6 +24,10 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+term "bn"
+
+
+
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
diff -r bcf558c445a4 -r 90779aefbf1a Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 08 13:16:25 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 08 17:07:08 2010 +0000
@@ -15,6 +15,47 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+ML {*
+fun strip_prems_concl trm =
+  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+
+fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+  | strip_outer_params B = ([], B)
+*}
+
+ML {*
+fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
+  let
+    val (cses, main_concls) = qexhausts
+      |> map prop_of
+      |> map strip_prems_concl
+      |> split_list
+
+    fun process_case cse bclauses =
+      let
+        val (params, (body, concl)) = cse
+          |> strip_outer_params
+          ||> Logic.dest_implies
+      in
+        Logic.mk_implies (body, concl) 
+      end  
+  
+    val cses' = map2 (map2 process_case) cses bclausess
+      |> map (map (Syntax.string_of_term lthy))
+      |> map commas
+      |> cat_lines
+
+    val _ = tracing ("cases\n " ^ cses')
+  in
+    ()
+  end
+*}
+
+ML {*
+val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val simp_attr = Attrib.internal (K Simplifier.simp_add)
+*}
 
 section{* Interface for nominal_datatype *}
 
@@ -165,6 +206,7 @@
     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)
@@ -524,6 +566,8 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
+  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
diff -r bcf558c445a4 -r 90779aefbf1a Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Wed Dec 08 13:16:25 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 08 17:07:08 2010 +0000
@@ -65,11 +65,6 @@
 
   val to_set: term -> term
 
-  (* some attributes *)
-  val eqvt_attr : Args.src
-  val rsp_attr  : Args.src
-  val simp_attr : Args.src
-
   (* fresh arguments for a term *)
   val fresh_args: Proof.context -> term -> term list
 
@@ -214,12 +209,6 @@
   else t
 
 
-(* some frequently used attributes *)
-
-val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
-val simp_attr = Attrib.internal (K Simplifier.simp_add)
-
 
 
 (* produces fresh arguments for a term *)