change generated lemmas dist_eqs and dist_les to iff-style
authorhuffman
Thu Feb 11 12:26:07 2010 -0800 (2010-02-11)
changeset 35117eeec2a320a77
parent 35060 6088dfd5f9c8
child 35118 724e8f77806a
change generated lemmas dist_eqs and dist_les to iff-style
src/HOLCF/Domain.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Domain.thy	Mon Feb 08 15:54:01 2010 -0800
     1.2 +++ b/src/HOLCF/Domain.thy	Thu Feb 11 12:26:07 2010 -0800
     1.3 @@ -222,6 +222,12 @@
     1.4  lemmas con_defined_iff_rules =
     1.5    sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
     1.6  
     1.7 +lemmas con_below_iff_rules =
     1.8 +  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
     1.9 +
    1.10 +lemmas con_eq_iff_rules =
    1.11 +  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
    1.12 +
    1.13  use "Tools/cont_consts.ML"
    1.14  use "Tools/cont_proc.ML"
    1.15  use "Tools/Domain/domain_library.ML"
     2.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Feb 08 15:54:01 2010 -0800
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Feb 11 12:26:07 2010 -0800
     2.3 @@ -300,14 +300,11 @@
     2.4  done
     2.5  
     2.6  lemma Cons_not_less_nil: "~a>>s << nil"
     2.7 -apply (subst Consq_def2)
     2.8 -apply (rule seq.rews)
     2.9 -apply (rule Def_not_UU)
    2.10 +apply (simp add: Consq_def2)
    2.11  done
    2.12  
    2.13  lemma Cons_not_nil: "a>>s ~= nil"
    2.14 -apply (subst Consq_def2)
    2.15 -apply (rule seq.rews)
    2.16 +apply (simp add: Consq_def2)
    2.17  done
    2.18  
    2.19  lemma Cons_not_nil2: "nil ~= a>>s"
     3.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 15:54:01 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Feb 11 12:26:07 2010 -0800
     3.3 @@ -512,18 +512,19 @@
     3.4  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
     3.5  
     3.6  val _ = trace " Proving dist_les...";
     3.7 -val distincts_le =
     3.8 +val dist_les =
     3.9    let
    3.10      fun dist (con1, args1) (con2, args2) =
    3.11        let
    3.12 -        val goal = lift_defined %: (nonlazy args1,
    3.13 -                        mk_trp (con_app con1 args1 ~<< con_app con2 args2));
    3.14 -        fun tacs ctxt = [
    3.15 -          rtac @{thm rev_contrapos} 1,
    3.16 -          eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
    3.17 -          @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
    3.18 -          @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
    3.19 -      in pg [] goal tacs end;
    3.20 +        fun iff_disj (t, []) = HOLogic.mk_not t
    3.21 +          | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
    3.22 +        val lhs = con_app con1 args1 << con_app con2 args2;
    3.23 +        val rhss = map (fn x => %:x === UU) (nonlazy args1);
    3.24 +        val goal = mk_trp (iff_disj (lhs, rhss));
    3.25 +        val rule1 = iso_locale RS @{thm iso.abs_below};
    3.26 +        val rules = rule1 :: @{thms con_below_iff_rules};
    3.27 +        val tacs = [simp_tac (HOL_ss addsimps rules) 1];
    3.28 +      in pg con_appls goal (K tacs) end;
    3.29  
    3.30      fun distinct (con1, args1) (con2, args2) =
    3.31          let
    3.32 @@ -533,28 +534,40 @@
    3.33                (args2, Name.variant_list (map vname args1) (map vname args2)));
    3.34          in [dist arg1 arg2, dist arg2 arg1] end;
    3.35      fun distincts []      = []
    3.36 -      | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
    3.37 +      | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
    3.38    in distincts cons end;
    3.39 -val dist_les = flat (flat distincts_le);
    3.40  
    3.41  val _ = trace " Proving dist_eqs...";
    3.42  val dist_eqs =
    3.43    let
    3.44 -    fun distinct (_,args1) ((_,args2), leqs) =
    3.45 +    fun dist (con1, args1) (con2, args2) =
    3.46        let
    3.47 -        val (le1,le2) = (hd leqs, hd(tl leqs));
    3.48 -        val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI)
    3.49 -      in
    3.50 -        if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
    3.51 -        if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
    3.52 -          [eq1, eq2]
    3.53 -      end;
    3.54 +        fun iff_disj (t, [], us) = HOLogic.mk_not t
    3.55 +          | iff_disj (t, ts, []) = HOLogic.mk_not t
    3.56 +          | iff_disj (t, ts, us) =
    3.57 +            let
    3.58 +              val disj1 = foldr1 HOLogic.mk_disj ts;
    3.59 +              val disj2 = foldr1 HOLogic.mk_disj us;
    3.60 +            in t === HOLogic.mk_conj (disj1, disj2) end;
    3.61 +        val lhs = con_app con1 args1 === con_app con2 args2;
    3.62 +        val rhss1 = map (fn x => %:x === UU) (nonlazy args1);
    3.63 +        val rhss2 = map (fn x => %:x === UU) (nonlazy args2);
    3.64 +        val goal = mk_trp (iff_disj (lhs, rhss1, rhss2));
    3.65 +        val rule1 = iso_locale RS @{thm iso.abs_eq};
    3.66 +        val rules = rule1 :: @{thms con_eq_iff_rules};
    3.67 +        val tacs = [simp_tac (HOL_ss addsimps rules) 1];
    3.68 +      in pg con_appls goal (K tacs) end;
    3.69 +
    3.70 +    fun distinct (con1, args1) (con2, args2) =
    3.71 +        let
    3.72 +          val arg1 = (con1, args1);
    3.73 +          val arg2 =
    3.74 +            (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
    3.75 +              (args2, Name.variant_list (map vname args1) (map vname args2)));
    3.76 +        in [dist arg1 arg2, dist arg2 arg1] end;
    3.77      fun distincts []      = []
    3.78 -      | distincts ((c,leqs)::cs) =
    3.79 -        flat
    3.80 -          (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    3.81 -        distincts cs;
    3.82 -  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
    3.83 +      | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
    3.84 +  in distincts cons end;
    3.85  
    3.86  local 
    3.87    fun pgterm rel con args =