src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35781 b7738ab762b1
parent 35777 bcc77916b7b9
child 35782 8a314dd86714
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 19:06:18 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 20:15:25 2010 -0800
     1.3 @@ -118,8 +118,8 @@
     1.4      Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
     1.5  
     1.6  val con_appls = #con_betas result;
     1.7 -val {exhaust, casedist, ...} = result;
     1.8 -val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
     1.9 +val {nchotomy, exhaust, ...} = result;
    1.10 +val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
    1.11  val {sel_rews, ...} = result;
    1.12  val when_rews = #cases result;
    1.13  val when_strict = hd when_rews;
    1.14 @@ -185,11 +185,11 @@
    1.15    thy
    1.16    |> PureThy.add_thmss [
    1.17       ((qualified "iso_rews"  , iso_rews    ), [simp]),
    1.18 -     ((qualified "exhaust"   , [exhaust]   ), []),
    1.19 -     ((qualified "casedist"  , [casedist]  ),
    1.20 +     ((qualified "nchotomy"  , [nchotomy]  ), []),
    1.21 +     ((qualified "exhaust"   , [exhaust]   ),
    1.22        [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
    1.23       ((qualified "when_rews" , when_rews   ), [simp]),
    1.24 -     ((qualified "compacts"  , con_compacts), [simp]),
    1.25 +     ((qualified "compacts"  , compacts    ), [simp]),
    1.26       ((qualified "con_rews"  , con_rews    ), [simp, fixrec_simp]),
    1.27       ((qualified "sel_rews"  , sel_rews    ), [simp]),
    1.28       ((qualified "dis_rews"  , dis_rews    ), [simp]),
    1.29 @@ -229,7 +229,7 @@
    1.30    in
    1.31      val axs_rep_iso = map (ga "rep_iso") dnames;
    1.32      val axs_abs_iso = map (ga "abs_iso") dnames;
    1.33 -    val cases = map (ga  "casedist" ) dnames;
    1.34 +    val exhausts = map (ga  "exhaust" ) dnames;
    1.35      val con_rews  = maps (gts "con_rews" ) dnames;
    1.36    end;
    1.37  
    1.38 @@ -317,12 +317,12 @@
    1.39              [resolve_tac prems 1] @
    1.40              map (K (atac 1)) (nonlazy args) @
    1.41              map (K (etac spec 1)) (filter is_rec args);
    1.42 -          fun cases_tacs (cons, cases) =
    1.43 -            res_inst_tac context [(("y", 0), "x")] cases 1 ::
    1.44 +          fun cases_tacs (cons, exhaust) =
    1.45 +            res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
    1.46              asm_simp_tac (take_ss addsimps prems) 1 ::
    1.47              maps con_tacs cons;
    1.48          in
    1.49 -          tacs1 @ maps cases_tacs (conss ~~ cases)
    1.50 +          tacs1 @ maps cases_tacs (conss ~~ exhausts)
    1.51          end;
    1.52      in pg'' thy [] goal tacf end;
    1.53  
    1.54 @@ -407,8 +407,8 @@
    1.55  in
    1.56    thy
    1.57    |> snd o PureThy.add_thmss [
    1.58 -     ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
    1.59 -     ((Binding.qualified true "ind"        comp_dbind, [ind]       ), [])]
    1.60 +     ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []),
    1.61 +     ((Binding.qualified true "induct"        comp_dbind, [ind]       ), [])]
    1.62    |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
    1.63  end; (* prove_induction *)
    1.64  
    1.65 @@ -554,7 +554,7 @@
    1.66  end; (* local *)
    1.67  
    1.68  in thy |> snd o PureThy.add_thmss
    1.69 -                  [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
    1.70 +    [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
    1.71  end; (* let *)
    1.72  
    1.73  fun comp_theorems