# HG changeset patch
# User blanchet
# Date 1346777380 -7200
# Node ID 3c26e17b2849d46d67927bfb92ad170ef70c5b9b
# Parent  b5413cb7d860bf45b2c6562707523c2220ec20c2
implemented "mk_case_tac" -- and got rid of "cheat_tac"

diff -r b5413cb7d860 -r 3c26e17b2849 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 18:14:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 18:49:40 2012 +0200
@@ -132,11 +132,11 @@
 
         val unf_T = domain_type (fastype_of fld);
         val prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
-        val caseofC_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
+        val caseC_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
 
         val ((((fs, u), v), xss), _) =
           lthy
-          |> mk_Frees "f" caseofC_Ts
+          |> mk_Frees "f" caseC_Ts
           ||>> yield_singleton (mk_Frees "u") unf_T
           ||>> yield_singleton (mk_Frees "v") T
           ||>> mk_Freess "x" ctr_Tss;
@@ -149,24 +149,26 @@
           map2 (fn k => fn xs =>
             fold_rev Term.lambda xs (fld $ mk_InN prod_Ts (HOLogic.mk_tuple xs) k)) ks xss;
 
-        val caseof_binder = Binding.suffix_name ("_" ^ caseN) b;
+        val case_binder = Binding.suffix_name ("_" ^ caseN) b;
 
-        val caseof_rhs = fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN uncurried_fs $ (unf $ v));
+        val case_rhs = fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN uncurried_fs $ (unf $ v));
 
-        val (((raw_ctrs, raw_ctr_defs), (raw_caseof, raw_caseof_def)), (lthy', lthy)) = no_defs_lthy
+        val (((raw_ctrs, raw_ctr_defs), (raw_case, raw_case_def)), (lthy', lthy)) = no_defs_lthy
           |> apfst split_list o fold_map2 (fn b => fn rhs =>
                Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
              ctr_binders ctr_rhss
-          ||>> (Local_Theory.define ((caseof_binder, NoSyn), ((Thm.def_binding caseof_binder, []),
-             caseof_rhs)) #>> apsnd snd)
+          ||>> (Local_Theory.define ((case_binder, NoSyn), ((Thm.def_binding case_binder, []),
+             case_rhs)) #>> apsnd snd)
           ||> `Local_Theory.restore;
 
         (*transforms defined frees into consts (and more)*)
         val phi = Proof_Context.export_morphism lthy lthy';
 
         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+        val case_def = Morphism.thm phi raw_case_def;
+
         val ctrs = map (Morphism.term phi) raw_ctrs;
-        val caseof = Morphism.term phi raw_caseof;
+        val casex = Morphism.term phi raw_case;
 
         val fld_iff_unf_thm =
           let
@@ -199,14 +201,13 @@
           map (map (fn (def, def') => fn {context = ctxt, ...} =>
             mk_half_distinct_tac ctxt fld_inject [def, def'])) (mk_half_pairss ctr_defs);
 
-        (*###*)
-        fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
-
-        val case_tacs = map (K cheat_tac) ks;
+        val case_tacs =
+          map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
+            mk_case_tac ctxt n k m case_def ctr_def unf_fld) ks ms ctr_defs;
 
         val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
       in
-        wrap_data tacss ((ctrs, caseof), (disc_binders, sel_binderss)) lthy'
+        wrap_data tacss ((ctrs, casex), (disc_binders, sel_binderss)) lthy'
       end;
   in
     lthy'
diff -r b5413cb7d860 -r 3c26e17b2849 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 18:14:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 18:49:40 2012 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_FP_SUGAR_TACTICS =
 sig
+  val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
   val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
@@ -20,6 +21,12 @@
 open BNF_Tactics
 open BNF_Util
 
+fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
+  Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
+  (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN'
+   REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
+   rtac refl) 1;
+
 fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
   Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
   rtac sumEN' 1 THEN
diff -r b5413cb7d860 -r 3c26e17b2849 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 18:14:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 18:49:40 2012 +0200
@@ -92,6 +92,7 @@
   val mk_union: term * term -> term
 
   val mk_sumEN: int -> thm
+  val mk_sum_casesN: int -> int -> thm
 
   val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
@@ -243,6 +244,11 @@
     | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
 end;
 
+fun mk_sum_casesN 1 1 = @{thm refl}
+  | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
+  | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
+  | mk_sum_casesN n m = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (m - 1)];
+
 fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
 
diff -r b5413cb7d860 -r 3c26e17b2849 src/HOL/Codatatype/Tools/bnf_gfp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 18:14:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 18:49:40 2012 +0200
@@ -36,7 +36,6 @@
   val mk_univ: term -> term
 
   val mk_specN: int -> thm -> thm
-  val mk_sum_casesN: int -> int -> thm
 
   val mk_InN_Field: int -> int -> thm
   val mk_InN_inject: int -> int -> thm
@@ -197,11 +196,6 @@
 fun mk_specN 0 thm = thm
   | mk_specN n thm = mk_specN (n - 1) (thm RS spec);
 
-fun mk_sum_casesN 1 1 = @{thm refl}
-  | mk_sum_casesN _ 1 = @{thm sum.cases(1)}
-  | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
-  | mk_sum_casesN n m = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (m - 1)];
-
 fun mk_rec_simps n rec_thm defs = map (fn i =>
   map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);
 
diff -r b5413cb7d860 -r 3c26e17b2849 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 18:14:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 18:49:40 2012 +0200
@@ -53,7 +53,7 @@
 
 fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
 
-fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;
+fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
 fun name_of_ctr t =
   case head_of t of
@@ -61,7 +61,7 @@
   | Free (s, _) => s
   | _ => error "Cannot extract name of constructor";
 
-fun prepare_wrap_data prep_term ((raw_ctrs, raw_caseof), (raw_disc_binders, raw_sel_binderss))
+fun prepare_wrap_data prep_term ((raw_ctrs, raw_case), (raw_disc_binders, raw_sel_binderss))
   no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -70,7 +70,7 @@
     (* TODO: integration with function package ("size") *)
 
     val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
-    val caseof0 = prep_term no_defs_lthy raw_caseof;
+    val case0 = prep_term no_defs_lthy raw_case;
 
     val n = length ctrs0;
     val ks = 1 upto n;
@@ -127,22 +127,22 @@
         else
           sel) (1 upto m) o pad_list no_binder m) ctrs0 ms;
 
-    fun mk_caseof Ts T =
+    fun mk_case Ts T =
       let
-        val (binders, body) = strip_type (fastype_of caseof0)
+        val (binders, body) = strip_type (fastype_of case0)
         val Type (_, Ts0) = List.last binders
-      in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) caseof0 end;
+      in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
 
-    val caseofB = mk_caseof As B;
-    val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
+    val caseB = mk_case As B;
+    val caseB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs);
+    fun mk_caseB_term eta_fs = Term.list_comb (caseB, eta_fs);
 
     val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
       mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
-      ||>> mk_Frees "f" caseofB_Ts
-      ||>> mk_Frees "g" caseofB_Ts
+      ||>> mk_Frees "f" caseB_Ts
+      ||>> mk_Frees "g" caseB_Ts
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
       ||>> yield_singleton (mk_Frees "w") T
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
@@ -155,15 +155,15 @@
     val xfs = map2 (curry Term.list_comb) fs xss;
     val xgs = map2 (curry Term.list_comb) gs xss;
 
-    val eta_fs = map2 eta_expand_caseof_arg xss xfs;
-    val eta_gs = map2 eta_expand_caseof_arg xss xgs;
+    val eta_fs = map2 eta_expand_case_arg xss xfs;
+    val eta_gs = map2 eta_expand_case_arg xss xgs;
 
-    val caseofB_fs = Term.list_comb (caseofB, eta_fs);
+    val caseB_fs = Term.list_comb (caseB, eta_fs);
 
     val exist_xs_v_eq_ctrs =
       map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
 
-    fun mk_sel_caseof_args k xs x T =
+    fun mk_sel_case_args k xs x T =
       map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks;
 
     fun disc_free b = Free (Binding.name_of b, T --> HOLogic.boolT);
@@ -180,7 +180,7 @@
     fun sel_spec b x xs k =
       let val T' = fastype_of x in
         mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v,
-          Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v)
+          Term.list_comb (mk_case As T', mk_sel_case_args k xs x T') $ v)
       end;
 
     val missing_disc_def = TrueI; (* marker *)
@@ -242,7 +242,7 @@
 
     val goal_cases =
       map3 (fn xs => fn xctr => fn xf =>
-        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (caseofB_fs $ xctr, xf))) xss xctrs xfs;
+        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (caseB_fs $ xctr, xf))) xss xctrs xfs;
 
     val goalss = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
 
@@ -282,7 +282,7 @@
                 val cTs =
                   map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree)
                     (rev (Term.add_tfrees goal_case []));
-                val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T);
+                val cxs = map (certify lthy) (mk_sel_case_args k xs x T);
               in
                 Local_Defs.fold lthy [sel_def]
                   (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
@@ -400,7 +400,7 @@
               | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) =
                 Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $
                   betapply (disc, v) $ mk_core f sels $ mk_rhs discs fs selss;
-            val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss);
+            val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
               mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
@@ -414,14 +414,13 @@
                 mk_Trueprop_eq (f, g)));
 
             val v_eq_w = mk_Trueprop_eq (v, w);
-            val caseof_fs = mk_caseofB_term eta_fs;
-            val caseof_gs = mk_caseofB_term eta_gs;
+            val case_fs = mk_caseB_term eta_fs;
+            val case_gs = mk_caseB_term eta_gs;
 
             val goal =
               Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
-                 mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w));
-            val goal_weak =
-              Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w));
+                 mk_Trueprop_eq (case_fs $ v, case_gs $ w));
+            val goal_weak = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (case_fs $ v, case_fs $ w));
           in
             (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
              Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
@@ -436,7 +435,7 @@
               list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
                 HOLogic.mk_not (q $ f_xs)));
 
-            val lhs = q $ (mk_caseofB_term eta_fs $ v);
+            val lhs = q $ (mk_caseB_term eta_fs $ v);
 
             val goal =
               mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));