tuning (systematic 1-based indices)
authorblanchet
Wed Sep 05 11:18:48 2012 +0200 (2012-09-05)
changeset 49152feb984727eec
parent 49151 ff86a2253f05
child 49153 c15a7123605c
tuning (systematic 1-based indices)
src/HOL/Codatatype/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:16:34 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:18:48 2012 +0200
     1.3 @@ -99,10 +99,10 @@
     1.4  
     1.5      val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
     1.6  
     1.7 -    fun can_rely_on_disc i =
     1.8 -      not (Binding.eq_name (nth raw_disc_binders' i, no_binder)) orelse nth ms i = 0;
     1.9 +    fun can_rely_on_disc k =
    1.10 +      not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
    1.11      fun can_omit_disc_binder k m =
    1.12 -      n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (2 - k))
    1.13 +      n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k))
    1.14  
    1.15      val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr;
    1.16  
    1.17 @@ -174,12 +174,14 @@
    1.18  
    1.19      fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
    1.20  
    1.21 -    fun alternate_disc_lhs i =
    1.22 +    fun alternate_disc_lhs k =
    1.23        HOLogic.mk_not
    1.24 -        (case nth disc_binders i of NONE => nth exist_xs_v_eq_ctrs i | SOME b => disc_free b $ v);
    1.25 +        (case nth disc_binders (k - 1) of
    1.26 +          NONE => nth exist_xs_v_eq_ctrs (k - 1)
    1.27 +        | SOME b => disc_free b $ v);
    1.28  
    1.29      fun alternate_disc k =
    1.30 -      if n = 2 then Term.lambda v (alternate_disc_lhs (2 - k)) else error "Cannot use \"*\" here"
    1.31 +      if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here"
    1.32  
    1.33      fun sel_spec b x xs k =
    1.34        let val T' = fastype_of x in
    1.35 @@ -312,7 +314,7 @@
    1.36          fun mk_alternate_disc_def k =
    1.37            let
    1.38              val goal =
    1.39 -              mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (2 - k)),
    1.40 +              mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)),
    1.41                  nth exist_xs_v_eq_ctrs (k - 1));
    1.42            in
    1.43              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>