only destruct cases equipped with the right stuff (in particular, 'sel_split')
authorblanchet
Fri Jan 10 14:39:37 2014 +0100 (2014-01-10)
changeset 54970891141de5672
parent 54969 0ac0b6576d21
child 54971 b4b828025880
only destruct cases equipped with the right stuff (in particular, 'sel_split')
src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     1.3 @@ -158,10 +158,10 @@
     1.4              (case fastype_of1 (bound_Ts, nth args n) of
     1.5                Type (s, Ts) =>
     1.6                (case dest_case ctxt s Ts t of
     1.7 -                NONE => apsnd (f conds t)
     1.8 -              | SOME (conds', branches) =>
     1.9 -                apfst (cons s) o fold_rev (uncurry fld)
    1.10 -                  (map (append conds o conjuncts_s) conds' ~~ branches))
    1.11 +                SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) =>
    1.12 +                apfst (cons ctr_sugar) o fold_rev (uncurry fld)
    1.13 +                  (map (append conds o conjuncts_s) conds' ~~ branches)
    1.14 +              | _ => apsnd (f conds t))
    1.15              | _ => apsnd (f conds t))
    1.16            else
    1.17              apsnd (f conds t)
    1.18 @@ -171,7 +171,10 @@
    1.19      fld [] t o pair []
    1.20    end;
    1.21  
    1.22 -fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
    1.23 +fun case_of ctxt s =
    1.24 +  (case ctr_sugar_of ctxt s of
    1.25 +    SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
    1.26 +  | _ => NONE);
    1.27  
    1.28  fun massage_let_if_case ctxt has_call massage_leaf =
    1.29    let
    1.30 @@ -319,8 +322,6 @@
    1.31      if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
    1.32    end;
    1.33  
    1.34 -val fold_rev_corec_call = fold_rev_let_if_case;
    1.35 -
    1.36  fun expand_to_ctr_term ctxt s Ts t =
    1.37    (case ctr_sugar_of ctxt s of
    1.38      SOME {ctrs, casex, ...} =>
    1.39 @@ -342,10 +343,7 @@
    1.40    snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
    1.41  
    1.42  fun case_thms_of_term ctxt bound_Ts t =
    1.43 -  let
    1.44 -    val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
    1.45 -    val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
    1.46 -  in
    1.47 +  let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in
    1.48      (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
    1.49       maps #sel_split_asms ctr_sugars)
    1.50    end;
    1.51 @@ -876,7 +874,7 @@
    1.52    let
    1.53      val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
    1.54        |> find_index (curry (op =) sel) o #sels o the;
    1.55 -    fun find t = if has_call t then snd (fold_rev_corec_call ctxt (K cons) [] t []) else [];
    1.56 +    fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else [];
    1.57    in
    1.58      find rhs_term
    1.59      |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     2.3 @@ -52,7 +52,8 @@
     2.4    val name_of_ctr: term -> string
     2.5    val name_of_disc: term -> string
     2.6    val dest_ctr: Proof.context -> string -> term -> term * term list
     2.7 -  val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
     2.8 +  val dest_case: Proof.context -> string -> typ list -> term ->
     2.9 +    (ctr_sugar * term list * term list) option
    2.10  
    2.11    val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    2.12      (((bool * (bool * bool)) * term list) * binding) *
    2.13 @@ -266,7 +267,7 @@
    2.14    (case Term.strip_comb t of
    2.15      (Const (c, _), args as _ :: _) =>
    2.16      (case ctr_sugar_of ctxt s of
    2.17 -      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
    2.18 +      SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) =>
    2.19        if case_name = c then
    2.20          let val n = length discs0 in
    2.21            if n < length args then
    2.22 @@ -278,7 +279,7 @@
    2.23                val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
    2.24                val branches' = map2 (curry Term.betapplys) branches branch_argss;
    2.25              in
    2.26 -              SOME (conds, branches')
    2.27 +              SOME (ctr_sugar, conds, branches')
    2.28              end
    2.29            else
    2.30              NONE