renamed confusing variable names
authorblanchet
Wed Dec 21 11:14:37 2016 +0100 (2016-12-21)
changeset 64624f3f457535fe2
parent 64608 20ccca53dd73
child 64625 c6330e16743f
renamed confusing variable names
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 20 16:18:56 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Dec 21 11:14:37 2016 +0100
     1.3 @@ -1721,7 +1721,7 @@
     1.4    end;
     1.5  
     1.6  fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
     1.7 -    live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses pre_type_definitions
     1.8 +    live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss pre_abs_inverses pre_type_definitions
     1.9      abs_inverses ctrss ctr_defss recs rec_defs lthy =
    1.10    let
    1.11      val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
    1.12 @@ -1758,14 +1758,13 @@
    1.13            Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem lthy nn ps)))
    1.14              (raw_premss, concl);
    1.15          val vars = Variable.add_free_names lthy goal [];
    1.16 -
    1.17          val kksss = map (map (map (fst o snd) o #2)) raw_premss;
    1.18  
    1.19          val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss);
    1.20  
    1.21          val thm =
    1.22            Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
    1.23 -            mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
    1.24 +            mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses
    1.25                abs_inverses fp_nesting_set_maps pre_set_defss)
    1.26            |> Thm.close_derivation;
    1.27        in
    1.28 @@ -1805,7 +1804,7 @@
    1.29  
    1.30          val tacss = @{map 4} (map ooo
    1.31                mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
    1.32 -            ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
    1.33 +            ctor_rec_thms pre_abs_inverses abs_inverses ctr_defss;
    1.34  
    1.35          fun prove goal tac =
    1.36            Goal.prove_sorry lthy [] [] goal (tac o #context)
    1.37 @@ -2035,7 +2034,7 @@
    1.38    end;
    1.39  
    1.40  fun derive_coinduct_thms_for_types strong alter_r pre_bnfs dtor_coinduct dtor_ctors
    1.41 -    live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss
    1.42 +    live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss
    1.43      (ctr_sugars : ctr_sugar list) ctxt =
    1.44    let
    1.45      val nn = length pre_bnfs;
    1.46 @@ -2108,7 +2107,7 @@
    1.47      fun prove dtor_coinduct' goal =
    1.48        Variable.add_free_names ctxt goal []
    1.49        |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
    1.50 -        mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
    1.51 +        mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses
    1.52            abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss))
    1.53        |> Thm.close_derivation;
    1.54  
    1.55 @@ -2125,7 +2124,7 @@
    1.56  
    1.57  fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
    1.58      dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
    1.59 -    kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
    1.60 +    kss mss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
    1.61      corecs corec_defs ctxt =
    1.62    let
    1.63      fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
    1.64 @@ -2147,7 +2146,7 @@
    1.65      val sel_thmsss = map #sel_thmss ctr_sugars;
    1.66  
    1.67      val coinduct_thms_pairs = derive_coinduct_thms_for_types true I pre_bnfs dtor_coinduct
    1.68 -      dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p
    1.69 +      dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p
    1.70        ctr_defss ctr_sugars ctxt;
    1.71  
    1.72      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 20 16:18:56 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 11:14:37 2016 +0100
     2.3 @@ -177,10 +177,10 @@
     2.4          rec_o_map_simps) ctxt))
     2.5    end;
     2.6  
     2.7 -fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
     2.8 +fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec pre_abs_inverse abs_inverse ctr_def ctxt =
     2.9    HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
    2.10      else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
    2.11 -  unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    2.12 +  unfold_thms_tac ctxt (ctor_rec :: pre_abs_inverse :: abs_inverse :: rec_defs @
    2.13      pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac ctxt refl);
    2.14  
    2.15  fun mk_rec_transfer_tac ctxt nn ns actives passives xssss rec_defs ctor_rec_transfers rel_pre_T_defs
    2.16 @@ -314,15 +314,15 @@
    2.17      resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
    2.18    (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
    2.19  
    2.20 -fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
    2.21 +fun mk_induct_leverage_prem_prems_tac ctxt nn kks pre_abs_inverses abs_inverses set_maps
    2.22      pre_set_defs =
    2.23    HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
    2.24      etac ctxt meta_mp,
    2.25 -    SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
    2.26 +    SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ pre_abs_inverses @ abs_inverses @ set_maps @
    2.27        sumprod_thms_set)),
    2.28      solve_prem_prem_tac ctxt]) (rev kks)));
    2.29  
    2.30 -fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k
    2.31 +fun mk_induct_discharge_prem_tac ctxt nn n pre_abs_inverses abs_inverses set_maps pre_set_defs m k
    2.32      kks =
    2.33    let val r = length kks in
    2.34      HEADGOAL (EVERY' [select_prem_tac ctxt n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
    2.35 @@ -330,11 +330,11 @@
    2.36      EVERY [REPEAT_DETERM_N r
    2.37          (HEADGOAL (rotate_tac ~1 THEN' dtac ctxt meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
    2.38        if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL (assume_tac ctxt),
    2.39 -      mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
    2.40 +      mk_induct_leverage_prem_prems_tac ctxt nn kks pre_abs_inverses abs_inverses set_maps
    2.41          pre_set_defs]
    2.42    end;
    2.43  
    2.44 -fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps
    2.45 +fun mk_induct_tac ctxt nn ns mss kksss ctr_defs ctor_induct' pre_abs_inverses abs_inverses set_maps
    2.46      pre_set_defss =
    2.47    let val n = Integer.sum ns in
    2.48      (if exists is_def_looping ctr_defs then
    2.49 @@ -343,17 +343,17 @@
    2.50         unfold_thms_tac ctxt ctr_defs) THEN
    2.51      HEADGOAL (rtac ctxt ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
    2.52      EVERY (@{map 4} (EVERY oooo @{map 3} o
    2.53 -        mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)
    2.54 -      pre_set_defss mss (unflat mss (1 upto n)) kkss)
    2.55 +        mk_induct_discharge_prem_tac ctxt nn n pre_abs_inverses abs_inverses set_maps)
    2.56 +      pre_set_defss mss (unflat mss (1 upto n)) kksss)
    2.57    end;
    2.58  
    2.59 -fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def fp_abs_inverse abs_inverse dtor_ctor ctr_def
    2.60 +fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def pre_abs_inverse abs_inverse dtor_ctor ctr_def
    2.61      discs sels =
    2.62    hyp_subst_tac ctxt THEN'
    2.63    CONVERSION (hhf_concl_conv
    2.64      (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
    2.65    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
    2.66 -  SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
    2.67 +  SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: pre_abs_inverse :: abs_inverse :: dtor_ctor ::
    2.68      sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
    2.69    (assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
    2.70       full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
    2.71 @@ -369,7 +369,7 @@
    2.72      full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt)
    2.73    end;
    2.74  
    2.75 -fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse
    2.76 +fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def pre_abs_inverse abs_inverse
    2.77      dtor_ctor exhaust ctr_defs discss selss =
    2.78    let val ks = 1 upto n in
    2.79      EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
    2.80 @@ -380,18 +380,18 @@
    2.81          EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
    2.82            map2 (fn k' => fn discs' =>
    2.83              if k' = k then
    2.84 -              mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def fp_abs_inverse abs_inverse
    2.85 +              mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def pre_abs_inverse abs_inverse
    2.86                  dtor_ctor ctr_def discs sels
    2.87              else
    2.88                mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
    2.89    end;
    2.90  
    2.91 -fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses
    2.92 +fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses abs_inverses
    2.93      dtor_ctors exhausts ctr_defss discsss selsss =
    2.94    HEADGOAL (rtac ctxt dtor_coinduct' THEN'
    2.95      EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
    2.96 -      (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
    2.97 -      selsss));
    2.98 +      (1 upto nn) ns pre_rel_defs pre_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss
    2.99 +      discsss selsss));
   2.100  
   2.101  fun mk_map_tac ctxt abs_inverses pre_map_def map_ctor live_nesting_map_id0s ctr_defs'
   2.102      extra_unfolds =