# HG changeset patch
# User haftmann
# Date 1276594719 -7200
# Node ID 4906ab9703165ded6f7feeb1ce117b9a848b9ddc
# Parent  4202e11ae7dc1d3c315f59b4ef20ce7bbf4a0617
maintain cong rules for case combinators

diff -r 4202e11ae7dc -r 4906ab970316 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 15 08:32:32 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 15 11:38:39 2010 +0200
@@ -72,6 +72,7 @@
   val is_abstr: theory -> string -> bool
   val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
   val get_case_scheme: theory -> string -> (int * (int * string list)) option
+  val get_case_cong: theory -> string -> thm option
   val undefineds: theory -> string list
   val print_codesetup: theory -> unit
 
@@ -168,7 +169,7 @@
     (*with explicit history*),
   types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
     (*with explicit history*),
-  cases: (int * (int * string list)) Symtab.table * unit Symtab.table
+  cases: ((int * (int * string list)) * thm) Symtab.table * unit Symtab.table
 };
 
 fun make_spec (history_concluded, ((signatures, functions), (types, cases))) =
@@ -935,7 +936,8 @@
   handle Bind => error "bad case certificate"
        | TERM _ => error "bad case certificate";
 
-fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
+fun get_case_scheme thy = Option.map fst o Symtab.lookup ((fst o the_cases o the_exec) thy);
+fun get_case_cong thy = Option.map snd o Symtab.lookup ((fst o the_cases o the_exec) thy);
 
 val undefineds = Symtab.keys o snd o the_cases o the_exec;
 
@@ -970,8 +972,8 @@
                       :: Pretty.str "of"
                       :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
       );
-    fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
-      | pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
+    fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
+      | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
           Pretty.str (string_of_const thy const), Pretty.str "with",
           (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
     val functions = the_functions exec
@@ -1108,14 +1110,34 @@
 
 (* cases *)
 
+fun case_cong thy case_const (num_args, (pos, constrs)) =
+  let
+    val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
+    val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
+    val (ws, vs) = chop pos zs;
+    val T = Logic.unvarifyT_global (const_typ thy case_const);
+    val Ts = (fst o strip_type) T;
+    val T_cong = nth Ts pos;
+    fun mk_prem z = Free (z, T_cong);
+    fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
+    val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
+    fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems
+      THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
+  in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
+
 fun add_case thm thy =
   let
-    val (c, (k, case_pats)) = case_cert thm;
+    val (case_const, (k, case_pats)) = case_cert thm;
     val _ = case filter_out (is_constr thy) case_pats
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
-    val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
-  in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+    val entry = (1 + Int.max (1, length case_pats), (k, case_pats));
+  in
+    thy
+    |> Theory.checkpoint
+    |> `(fn thy => case_cong thy case_const entry)
+    |-> (fn cong => (map_exec_purge o map_cases o apfst) (Symtab.update (case_const, (entry, cong))))
+  end;
 
 fun add_undefined c thy =
   (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
@@ -1138,7 +1160,7 @@
             then insert (op =) c else I)
             ((the_functions o the_exec) thy) (old_proj :: old_constrs);
     fun drop_outdated_cases cases = fold Symtab.delete_safe
-      (Symtab.fold (fn (c, (_, (_, cos))) =>
+      (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
         if exists (member (op =) old_constrs) cos
           then insert (op =) c else I) cases []) cases;
   in