# HG changeset patch
# User berghofe
# Date 1263559061 -3600
# Node ID f625d8d6fcf3a339b06ce81ef72b1909aa51fc64
# Parent  7894c7dab1328f3e9c3890a00770b4299b3a569d
Eliminated is_open option of Rule_Cases.make_nested/make_common;
use Rule_Cases.internalize_params to rename parameters instead.

diff -r 7894c7dab132 -r f625d8d6fcf3 src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sun Jan 10 18:43:45 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Jan 15 13:37:41 2010 +0100
@@ -69,8 +69,9 @@
       |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
     Seq.maps (fn (names, st) =>
       CASES
-        (Rule_Cases.make_common false
-          (ProofContext.theory_of ctxt, Thm.prop_of st) names)
+        (Rule_Cases.make_common
+          (ProofContext.theory_of ctxt,
+           Thm.prop_of (Rule_Cases.internalize_params st)) names)
         Tactical.all_tac st))
 in
 val setup_boogie_cases = Method.setup @{binding boogie_cases}
diff -r 7894c7dab132 -r f625d8d6fcf3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jan 10 18:43:45 2010 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 15 13:37:41 2010 +0100
@@ -387,7 +387,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
 fun apply_method current_context meth state =
   let
diff -r 7894c7dab132 -r f625d8d6fcf3 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Jan 10 18:43:45 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Jan 15 13:37:41 2010 +0100
@@ -25,8 +25,8 @@
     binds: (indexname * term option) list,
     cases: (string * T) list}
   val strip_params: term -> (string * typ) list
-  val make_common: bool -> theory * term -> (string * string list) list -> cases
-  val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
+  val make_common: theory * term -> (string * string list) list -> cases
+  val make_nested: term -> theory * term -> (string * string list) list -> cases
   val apply: term list -> T -> T
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
@@ -43,6 +43,7 @@
   val get: thm -> (string * string list) list * int
   val rename_params: string list list -> thm -> thm
   val params: string list list -> attribute
+  val internalize_params: thm -> thm
   val mutual_rule: Proof.context -> thm list -> (int list * thm) option
   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
 end;
@@ -90,18 +91,15 @@
         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
 
-fun extract_case is_open thy (case_outline, raw_prop) name concls =
+fun extract_case thy (case_outline, raw_prop) name concls =
   let
-    val rename = if is_open then I else apfst (Name.internal o Name.clean);
-
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
     val len = length props;
     val nested = is_some case_outline andalso len > 1;
 
     fun extract prop =
       let
-        val (fixes1, fixes2) = extract_fixes case_outline prop
-          |> apfst (map rename);
+        val (fixes1, fixes2) = extract_fixes case_outline prop;
         val abs_fixes = abs (fixes1 @ fixes2);
         fun abs_fixes1 t =
           if not nested then abs_fixes t
@@ -135,7 +133,7 @@
     else SOME (nested_case (hd cases))
   end;
 
-fun make is_open rule_struct (thy, prop) cases =
+fun make rule_struct (thy, prop) cases =
   let
     val n = length cases;
     val nprems = Logic.count_prems prop;
@@ -143,13 +141,13 @@
       ((case try (fn () =>
           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
         NONE => (name, NONE)
-      | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
+      | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
 
 in
 
-fun make_common is_open = make is_open NONE;
-fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
+val make_common = make NONE;
+fun make_nested rule_struct = make (SOME rule_struct);
 
 fun apply args =
   let
@@ -334,6 +332,20 @@
 fun params xss = Thm.rule_attribute (K (rename_params xss));
 
 
+(* internalize parameter names *)
+
+fun internalize_params rule =
+  let
+    fun rename prem =
+      let val xs =
+        map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
+      in Logic.list_rename_params (xs, prem) end;
+    fun rename_prems prop =
+      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
+      in Logic.list_implies (map rename As, C) end;
+  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
+
+
 
 (** mutual_rule **)