declare take_rews as simp rules
authorhuffman
Wed Apr 22 07:12:21 2009 -0700 (2009-04-22)
changeset 31004ac7e90792089
parent 30922 96d053e00ec0
child 31005 e55eed7d9b55
declare take_rews as simp rules
src/HOLCF/Tools/domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Apr 21 17:07:44 2009 -0700
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:12:21 2009 -0700
     1.3 @@ -608,23 +608,22 @@
     1.4  in
     1.5    thy
     1.6      |> Sign.add_path (Long_Name.base_name dname)
     1.7 -    |> (snd o PureThy.add_thmss [
     1.8 -        ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
     1.9 -        ((Binding.name "exhaust"  , [exhaust] ), []),
    1.10 -        ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
    1.11 -        ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
    1.12 -        ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
    1.13 -        ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
    1.14 -        ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
    1.15 -        ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
    1.16 -        ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
    1.17 -        ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
    1.18 -        ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
    1.19 -        ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
    1.20 -        ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
    1.21 -        ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
    1.22 -        ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
    1.23 -       ])
    1.24 +    |> snd o PureThy.add_thmss [
    1.25 +        ((Binding.name "iso_rews"  , iso_rews    ), [Simplifier.simp_add]),
    1.26 +        ((Binding.name "exhaust"   , [exhaust]   ), []),
    1.27 +        ((Binding.name "casedist"  , [casedist]  ), [Induct.cases_type dname]),
    1.28 +        ((Binding.name "when_rews" , when_rews   ), [Simplifier.simp_add]),
    1.29 +        ((Binding.name "compacts"  , con_compacts), [Simplifier.simp_add]),
    1.30 +        ((Binding.name "con_rews"  , con_rews    ), [Simplifier.simp_add]),
    1.31 +        ((Binding.name "sel_rews"  , sel_rews    ), [Simplifier.simp_add]),
    1.32 +        ((Binding.name "dis_rews"  , dis_rews    ), [Simplifier.simp_add]),
    1.33 +        ((Binding.name "pat_rews"  , pat_rews    ), [Simplifier.simp_add]),
    1.34 +        ((Binding.name "dist_les"  , dist_les    ), [Simplifier.simp_add]),
    1.35 +        ((Binding.name "dist_eqs"  , dist_eqs    ), [Simplifier.simp_add]),
    1.36 +        ((Binding.name "inverts"   , inverts     ), [Simplifier.simp_add]),
    1.37 +        ((Binding.name "injects"   , injects     ), [Simplifier.simp_add]),
    1.38 +        ((Binding.name "copy_rews" , copy_rews   ), [Simplifier.simp_add]),
    1.39 +        ((Binding.name "match_rews", mat_rews    ), [Simplifier.simp_add])]
    1.40      |> Sign.parent_path
    1.41      |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    1.42          pat_rews @ dist_les @ dist_eqs @ copy_rews)
    1.43 @@ -1004,14 +1003,14 @@
    1.44  fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
    1.45  
    1.46  in thy |> Sign.add_path comp_dnam
    1.47 -       |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
    1.48 -		("take_rews"  , take_rews  ),
    1.49 -		("take_lemmas", take_lemmas),
    1.50 -		("finites"    , finites    ),
    1.51 -		("finite_ind", [finite_ind]),
    1.52 -		("ind"       , [ind       ]),
    1.53 -		("coind"     , [coind     ])])))
    1.54 -       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
    1.55 +       |> snd o PureThy.add_thmss [
    1.56 +           ((Binding.name "take_rews"  , take_rews   ), [Simplifier.simp_add]),
    1.57 +           ((Binding.name "take_lemmas", take_lemmas ), []),
    1.58 +           ((Binding.name "finites"    , finites     ), []),
    1.59 +           ((Binding.name "finite_ind" , [finite_ind]), []),
    1.60 +           ((Binding.name "ind"        , [ind]       ), []),
    1.61 +           ((Binding.name "coind"      , [coind]     ), [])]
    1.62 +       |> snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))
    1.63         |> Sign.parent_path |> pair take_rews
    1.64  end; (* let *)
    1.65  end; (* local *)