infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
authornipkow
Mon Aug 01 12:08:53 2011 +0200 (2011-08-01)
changeset 440452814ff2a6e3e
parent 44005 421f8bc19ce4
child 44046 a43ca8ed6564
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Boogie/Tools/boogie_tactics.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/inductive_set.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
src/Tools/case_product.ML
     1.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Sun Jul 31 11:13:38 2011 -0700
     1.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Aug 01 12:08:53 2011 +0200
     1.3 @@ -1056,8 +1056,7 @@
     1.4         (is "PROP ?Hyp Env B t A")  
     1.5    proof (induct)
     1.6      case Skip 
     1.7 -    from Skip.prems Skip.hyps 
     1.8 -    show ?case by cases simp
     1.9 +    then show ?case by cases simp
    1.10    next
    1.11      case Expr 
    1.12      from Expr.prems Expr.hyps 
     2.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sun Jul 31 11:13:38 2011 -0700
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Mon Aug 01 12:08:53 2011 +0200
     2.3 @@ -91,7 +91,7 @@
     2.4        CASES
     2.5          (Rule_Cases.make_common
     2.6            (Proof_Context.theory_of ctxt,
     2.7 -           Thm.prop_of (Rule_Cases.internalize_params st)) names)
     2.8 +           Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names))
     2.9          Tactical.all_tac st))
    2.10  in
    2.11  val setup_boogie_cases = Method.setup @{binding boogie_cases}
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 31 11:13:38 2011 -0700
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Aug 01 12:08:53 2011 +0200
     3.3 @@ -158,7 +158,7 @@
     3.4          [] => ()
     3.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     3.6            commas_quote xs));
     3.7 -    val induct_cases = map fst (fst (Rule_Cases.get (the
     3.8 +    val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
     3.9        (Induct.lookup_inductP ctxt (hd names)))));
    3.10      val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
    3.11      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 31 11:13:38 2011 -0700
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Aug 01 12:08:53 2011 +0200
     4.3 @@ -165,7 +165,7 @@
     4.4          [] => ()
     4.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     4.6            commas_quote xs));
     4.7 -    val induct_cases = map fst (fst (Rule_Cases.get (the
     4.8 +    val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
     4.9        (Induct.lookup_inductP ctxt (hd names)))));
    4.10      val induct_cases' = if null induct_cases then replicate (length intrs) ""
    4.11        else induct_cases;
     5.1 --- a/src/HOL/Tools/inductive_set.ML	Sun Jul 31 11:13:38 2011 -0700
     5.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Aug 01 12:08:53 2011 +0200
     5.3 @@ -524,7 +524,7 @@
     5.4        Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
     5.5          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
     5.6          (map (fn th => (to_set [] (Context.Proof lthy3) th,
     5.7 -           map fst (fst (Rule_Cases.get th)),
     5.8 +           map (fst o fst) (fst (Rule_Cases.get th)),
     5.9             Rule_Cases.get_constraints th)) elims)
    5.10          (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
    5.11    in
     6.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 31 11:13:38 2011 -0700
     6.2 +++ b/src/Pure/Isar/proof.ML	Mon Aug 01 12:08:53 2011 +0200
     6.3 @@ -391,7 +391,7 @@
     6.4  fun no_goal_cases st = map (rpair NONE) (goals st);
     6.5  
     6.6  fun goal_cases st =
     6.7 -  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
     6.8 +  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
     6.9  
    6.10  fun apply_method current_context meth state =
    6.11    let
     7.1 --- a/src/Pure/Isar/rule_cases.ML	Sun Jul 31 11:13:38 2011 -0700
     7.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Aug 01 12:08:53 2011 +0200
     7.3 @@ -24,9 +24,12 @@
     7.4      assumes: (string * term list) list,
     7.5      binds: (indexname * term option) list,
     7.6      cases: (string * T) list}
     7.7 +  val case_hypsN: string
     7.8    val strip_params: term -> (string * typ) list
     7.9 -  val make_common: theory * term -> (string * string list) list -> cases
    7.10 -  val make_nested: term -> theory * term -> (string * string list) list -> cases
    7.11 +  val make_common: theory * term ->
    7.12 +    ((string * string list) * string list) list -> cases
    7.13 +  val make_nested: term -> theory * term ->
    7.14 +    ((string * string list) * string list) list -> cases
    7.15    val apply: term list -> T -> T
    7.16    val consume: thm list -> thm list -> ('a * int) * thm ->
    7.17      (('a * (int * thm list)) * thm) Seq.seq
    7.18 @@ -38,11 +41,12 @@
    7.19    val constraints: int -> attribute
    7.20    val name: string list -> thm -> thm
    7.21    val case_names: string list -> attribute
    7.22 +  val cases_hyp_names: string list list -> attribute
    7.23    val case_conclusion: string * string list -> attribute
    7.24    val is_inner_rule: thm -> bool
    7.25    val inner_rule: attribute
    7.26    val save: thm -> thm -> thm
    7.27 -  val get: thm -> (string * string list) list * int
    7.28 +  val get: thm -> ((string * string list) * string list) list * int
    7.29    val rename_params: string list list -> thm -> thm
    7.30    val params: string list list -> attribute
    7.31    val internalize_params: thm -> thm
    7.32 @@ -87,15 +91,21 @@
    7.33    | extract_fixes (SOME outline) prop =
    7.34        chop (length (Logic.strip_params outline)) (strip_params prop);
    7.35  
    7.36 -fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    7.37 -  | extract_assumes qual (SOME outline) prop =
    7.38 -      let val (hyps, prems) =
    7.39 -        chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    7.40 -      in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
    7.41 +fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
    7.42 +  | extract_assumes qual hnames (SOME outline) prop =
    7.43 +      let
    7.44 +        val (hyps, prems) =
    7.45 +          chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
    7.46 +        fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
    7.47 +        val (hyps1,hyps2) = chop (length hnames) hyps;
    7.48 +        val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1;
    7.49 +        val pairs = pairs1 @ (map (pair case_hypsN) hyps2);
    7.50 +        val named_hyps = map extract (partition_eq (eq_fst op =) pairs)
    7.51 +      in (named_hyps, [(qual case_premsN, prems)]) end;
    7.52  
    7.53  fun bindings args = map (apfst Binding.name) args;
    7.54  
    7.55 -fun extract_case thy (case_outline, raw_prop) name concls =
    7.56 +fun extract_case thy (case_outline, raw_prop) name hnames concls =
    7.57    let
    7.58      val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
    7.59      val len = length props;
    7.60 @@ -108,8 +118,7 @@
    7.61          fun abs_fixes1 t =
    7.62            if not nested then abs_fixes t
    7.63            else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
    7.64 -
    7.65 -        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
    7.66 +        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
    7.67            |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
    7.68  
    7.69          val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
    7.70 @@ -142,11 +151,11 @@
    7.71    let
    7.72      val n = length cases;
    7.73      val nprems = Logic.count_prems prop;
    7.74 -    fun add_case (name, concls) (cs, i) =
    7.75 +    fun add_case ((name, hnames), concls) (cs, i) =
    7.76        ((case try (fn () =>
    7.77            (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
    7.78          NONE => (name, NONE)
    7.79 -      | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
    7.80 +      | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
    7.81    in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
    7.82  
    7.83  in
    7.84 @@ -286,6 +295,26 @@
    7.85  fun case_names ss = Thm.rule_attribute (K (name ss));
    7.86  
    7.87  
    7.88 +(** hyp names **)
    7.89 +
    7.90 +val implode_hyps = implode_args o map (suffix "," o space_implode ",");
    7.91 +val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
    7.92 +
    7.93 +val cases_hyp_names_tagN = "cases_hyp_names";
    7.94 +
    7.95 +fun add_cases_hyp_names NONE = I
    7.96 +  | add_cases_hyp_names (SOME namess) =
    7.97 +      Thm.untag_rule cases_hyp_names_tagN
    7.98 +      #> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess);
    7.99 +
   7.100 +fun lookup_cases_hyp_names th =
   7.101 +  AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN
   7.102 +  |> Option.map explode_hyps;
   7.103 +
   7.104 +val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
   7.105 +fun cases_hyp_names ss =
   7.106 +  Thm.rule_attribute (K (add_cases_hyp_names (SOME ss)));
   7.107 +
   7.108  
   7.109  (** case conclusions **)
   7.110  
   7.111 @@ -339,6 +368,7 @@
   7.112    save_consumes th #>
   7.113    save_constraints th #>
   7.114    save_case_names th #>
   7.115 +  save_cases_hyp_names th #>
   7.116    save_case_concls th #>
   7.117    save_inner_rule th;
   7.118  
   7.119 @@ -349,7 +379,11 @@
   7.120        (case lookup_case_names th of
   7.121          NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
   7.122        | SOME names => map (fn name => (name, get_case_concls th name)) names);
   7.123 -  in (cases, n) end;
   7.124 +    val cases_hyps = (case lookup_cases_hyp_names th of
   7.125 +        NONE => replicate (length cases) []
   7.126 +      | SOME names => names);
   7.127 +    fun regroup ((name,concls),hyps) = ((name,hyps),concls)
   7.128 +  in (map regroup (cases ~~ cases_hyps), n) end;
   7.129  
   7.130  
   7.131  (* params *)
     8.1 --- a/src/Tools/case_product.ML	Sun Jul 31 11:13:38 2011 -0700
     8.2 +++ b/src/Tools/case_product.ML	Mon Aug 01 12:08:53 2011 +0200
     8.3 @@ -90,9 +90,9 @@
     8.4  
     8.5  fun annotation thm1 thm2 =
     8.6    let
     8.7 -    val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
     8.8 -    val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
     8.9 -    val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
    8.10 +    val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
    8.11 +    val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
    8.12 +    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
    8.13    in
    8.14      Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
    8.15    end