# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 7a01387c47d51c0268d85dcb9bff872510b3ab2e
# Parent  5a63324f9002ee7f376a1932b561e7bb63406a1d
added tactic to prove 'disc_iff' properties in 'primcorec'

diff -r 5a63324f9002 -r 7a01387c47d5 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -336,7 +336,7 @@
             if exists (exists_subtype_in seen) mutual_Ts then
               (case gen_rhss_in gen_seen rho mutual_Ts of
                 [] => fresh_tyargs ()
-              | gen_tyargss as gen_tyargs :: gen_tyargss_tl =>
+              | gen_tyargs :: gen_tyargss_tl =>
                 let
                   val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
                   val mgu = Type.raw_unifys unify_pairs Vartab.empty;
diff -r 5a63324f9002 -r 7a01387c47d5 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -2806,8 +2806,8 @@
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
 val option_parser = Parse.group (fn () => "option")
-  ((Parse.reserved "sequential" >> K Option_Sequential)
-  || (Parse.reserved "exhaustive" >> K Option_Exhaustive))
+  ((Parse.reserved "sequential" >> K Sequential_Option)
+  || (Parse.reserved "exhaustive" >> K Exhaustive_Option))
 
 val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
   (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
diff -r 5a63324f9002 -r 7a01387c47d5 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -8,9 +8,8 @@
 
 signature BNF_GFP_REC_SUGAR =
 sig
-  datatype primcorec_option =
-    Option_Sequential |
-    Option_Exhaustive
+  datatype primcorec_option = Sequential_Option | Exhaustive_Option
+
   val add_primcorecursive_cmd: primcorec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
@@ -48,9 +47,7 @@
 fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]);
 fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns);
 
-datatype primcorec_option =
-  Option_Sequential |
-  Option_Exhaustive
+datatype primcorec_option = Sequential_Option | Exhaustive_Option;
 
 datatype corec_call =
   Dummy_No_Corec of int |
@@ -852,8 +849,8 @@
         [] => ()
       | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
 
-    val seq = member (op =) opts Option_Sequential;
-    val exhaustive = member (op =) opts Option_Exhaustive;
+    val seq = member (op =) opts Sequential_Option;
+    val exhaustive = member (op =) opts Exhaustive_Option;
 
     val fun_names = map Binding.name_of bs;
     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
diff -r 5a63324f9002 -r 7a01387c47d5 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -12,6 +12,7 @@
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
+  val mk_primcorec_disc_iff_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic
   val mk_primcorec_exhaust_tac: int -> thm -> tactic
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> thm option -> tactic
@@ -25,6 +26,7 @@
 open BNF_Util
 open BNF_Tactics
 
+val atomize_conjL = @{thm atomize_conjL};
 val falseEs = @{thms not_TrueE FalseE};
 val Let_def = @{thm Let_def};
 val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
@@ -74,6 +76,15 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
+fun mk_primcorec_disc_iff_tac ctxt k exhaust discs disc_excludess =
+  HEADGOAL (rtac iffI THEN'
+    rtac exhaust THEN'
+    EVERY' (map2 (fn disc => fn [] => REPEAT_DETERM o (atac ORELSE' etac conjI)
+        | [disc_exclude] =>
+          dtac disc THEN' (REPEAT_DETERM o atac) THEN' dtac disc_exclude THEN' etac notE THEN' atac)
+      discs disc_excludess) THEN'
+    etac (unfold_thms ctxt [atomize_conjL] (nth discs (k - 1))));
+
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
     exclsss =
   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
@@ -139,7 +150,7 @@
         (ms |> split_last ||> K [n - 1] |> op @,
          f_ctrs
          |> split_last
-         ||> unfold_thms ctxt @{thms atomize_conjL}
+         ||> unfold_thms ctxt [atomize_conjL]
          ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
          |> op @));
   in