clarified interaction with dead variables in the composition of BNFs
authortraytel
Mon Feb 24 10:16:10 2014 +0100 (2014-02-24)
changeset 5570750cf04dd2584
parent 55706 064c7c249f55
child 55717 601ea66c5bcd
clarified interaction with dead variables in the composition of BNFs
src/HOL/Basic_BNFs.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
     1.1 --- a/src/HOL/Basic_BNFs.thy	Mon Feb 24 00:04:48 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Feb 24 10:16:10 2014 +0100
     1.3 @@ -25,11 +25,9 @@
     1.4  
     1.5  bnf DEADID: 'a
     1.6    map: "id :: 'a \<Rightarrow> 'a"
     1.7 -  bd: "natLeq +c |UNIV :: 'a set|"
     1.8 +  bd: natLeq
     1.9    rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 -by (auto simp add: Grp_def
    1.11 -  card_order_csum natLeq_card_order card_of_card_order_on
    1.12 -  cinfinite_csum natLeq_cinfinite)
    1.13 +by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    1.14  
    1.15  definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    1.16  "setl x = (case x of Inl z => {z} | _ => {})"
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Feb 24 00:04:48 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Feb 24 10:16:10 2014 +0100
     2.3 @@ -301,10 +301,7 @@
     2.4      val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     2.5      val sets = drop n bnf_sets;
     2.6  
     2.7 -    (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
     2.8 -    val bnf_bd = mk_bd_of_bnf Ds As bnf;
     2.9 -    val bd = mk_cprod
    2.10 -      (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
    2.11 +    val bd = mk_bd_of_bnf Ds As bnf;
    2.12  
    2.13      fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
    2.14      fun map_comp0_tac ctxt =
    2.15 @@ -313,11 +310,9 @@
    2.16      fun map_cong0_tac ctxt =
    2.17        mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    2.18      val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
    2.19 -    fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    2.20 -    fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    2.21 -    val set_bd_tacs =
    2.22 -      map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
    2.23 -        (drop n (set_bd_of_bnf bnf));
    2.24 +    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    2.25 +    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    2.26 +    val set_bd_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_bd_of_bnf bnf));
    2.27  
    2.28      val in_alt_thm =
    2.29        let
    2.30 @@ -611,8 +606,9 @@
    2.31      (*bd may depend only on dead type variables*)
    2.32      val bd_repT = fst (dest_relT (fastype_of bnf_bd));
    2.33      val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
    2.34 -    val params = fold Term.add_tfreesT Ds [];
    2.35 +    val params = Term.add_tfreesT bd_repT [];
    2.36      val deads = map TFree params;
    2.37 +    val all_deads = map TFree (fold Term.add_tfreesT Ds []);
    2.38  
    2.39      val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
    2.40        typedef (bdT_bind, params, NoSyn)
    2.41 @@ -649,11 +645,11 @@
    2.42        mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
    2.43  
    2.44      val (bnf', lthy') =
    2.45 -      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
    2.46 +      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads)
    2.47          Binding.empty Binding.empty []
    2.48          ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    2.49    in
    2.50 -    ((bnf', deads), lthy')
    2.51 +    ((bnf', all_deads), lthy')
    2.52    end;
    2.53  
    2.54  fun key_of_types Ts = Type ("", Ts);
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Feb 24 00:04:48 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Feb 24 10:16:10 2014 +0100
     3.3 @@ -19,11 +19,8 @@
     3.4    val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
     3.5    val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
     3.6  
     3.7 -  val mk_kill_bd_card_order_tac: int -> thm -> tactic
     3.8 -  val mk_kill_bd_cinfinite_tac: thm -> tactic
     3.9    val kill_in_alt_tac: tactic
    3.10    val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
    3.11 -  val mk_kill_set_bd_tac: thm -> thm -> tactic
    3.12  
    3.13    val empty_natural_tac: tactic
    3.14    val lift_in_alt_tac: tactic
    3.15 @@ -42,10 +39,8 @@
    3.16  open BNF_Util
    3.17  open BNF_Tactics
    3.18  
    3.19 -val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
    3.20  val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
    3.21  val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs};
    3.22 -val csum_Cnotzero1 = @{thm csum_Cnotzero1};
    3.23  val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
    3.24  val trans_o_apply = @{thm trans[OF o_apply]};
    3.25  
    3.26 @@ -180,28 +175,6 @@
    3.27    (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
    3.28      EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
    3.29  
    3.30 -fun mk_kill_bd_card_order_tac n bd_card_order =
    3.31 -  (rtac @{thm card_order_cprod} THEN'
    3.32 -  K (REPEAT_DETERM_N (n - 1)
    3.33 -    ((rtac @{thm card_order_csum} THEN'
    3.34 -    rtac @{thm card_of_card_order_on}) 1)) THEN'
    3.35 -  rtac @{thm card_of_card_order_on} THEN'
    3.36 -  rtac bd_card_order) 1;
    3.37 -
    3.38 -fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
    3.39 -  (rtac @{thm cinfinite_cprod2} THEN'
    3.40 -  TRY o rtac csum_Cnotzero1 THEN'
    3.41 -  rtac Cnotzero_UNIV THEN'
    3.42 -  rtac bd_Cinfinite) 1;
    3.43 -
    3.44 -fun mk_kill_set_bd_tac bd_Card_order set_bd =
    3.45 -  (rtac ctrans THEN'
    3.46 -  rtac set_bd THEN'
    3.47 -  rtac @{thm ordLeq_cprod2} THEN'
    3.48 -  TRY o rtac csum_Cnotzero1 THEN'
    3.49 -  rtac Cnotzero_UNIV THEN'
    3.50 -  rtac bd_Card_order) 1
    3.51 -
    3.52  val kill_in_alt_tac =
    3.53    ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
    3.54    REPEAT_DETERM (CHANGED (etac conjE 1)) THEN