src/HOLCF/domain/theorems.ML
changeset 16321 ef32a42f4079
parent 16224 57094b83774e
child 16385 a9dec1969348
     1.1 --- a/src/HOLCF/domain/theorems.ML	Wed Jun 08 01:41:20 2005 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Jun 08 02:27:19 2005 +0200
     1.3 @@ -304,30 +304,34 @@
     1.4      in map standard (distincts (cons~~distincts_le)) end;
     1.5  
     1.6  local 
     1.7 -  fun pgterm rel con args = let
     1.8 -                fun append s = upd_vname(fn v => v^s);
     1.9 -                val (largs,rargs) = (args, map (append "'") args);
    1.10 -                in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
    1.11 -                      lift_defined %: ((nonlazy largs),lift_defined %: ((nonlazy rargs),
    1.12 -                            mk_trp (foldr' mk_conj 
    1.13 -                                (ListPair.map rel
    1.14 -				 (map %# largs, map %# rargs)))))) end;
    1.15 +  fun pgterm rel con args =
    1.16 +    let
    1.17 +      fun append s = upd_vname(fn v => v^s);
    1.18 +      val (largs,rargs) = (args, map (append "'") args);
    1.19 +      val concl = mk_trp (foldr' mk_conj (ListPair.map rel (map %# largs, map %# rargs)));
    1.20 +      val prem = mk_trp (rel(con_app con largs,con_app con rargs));
    1.21 +      val prop = prem ===> lift_defined %: (nonlazy largs, concl);
    1.22 +    in pg con_appls prop end;
    1.23    val cons' = List.filter (fn (_,args) => args<>[]) cons;
    1.24  in
    1.25 -val inverts = map (fn (con,args) => 
    1.26 -                pgterm (op <<) con args (List.concat(map (fn arg => [
    1.27 -                                TRY(rtac conjI 1),
    1.28 -                                dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1,
    1.29 -                                asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
    1.30 -                                                      ) args))) cons';
    1.31 -val injects = map (fn ((con,args),inv_thm) => 
    1.32 -                           pgterm (op ===) con args [
    1.33 -                                etac (antisym_less_inverse RS conjE) 1,
    1.34 -                                dtac inv_thm 1, REPEAT(atac 1),
    1.35 -                                dtac inv_thm 1, REPEAT(atac 1),
    1.36 -                                TRY(safe_tac HOL_cs),
    1.37 -                                REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
    1.38 -                  (cons'~~inverts);
    1.39 +val inverts =
    1.40 +  let
    1.41 +    val abs_less = ax_abs_iso RS (allI RS injection_less) RS iffD1;
    1.42 +    val simps = [up_less, spair_less];
    1.43 +    val tacs = [
    1.44 +      dtac abs_less 1,
    1.45 +      REPEAT (dresolve_tac [sinl_less RS iffD1, sinr_less RS iffD1] 1),
    1.46 +      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
    1.47 +  in map (fn (con,args) => pgterm (op <<) con args tacs) cons' end;
    1.48 +val injects =
    1.49 +  let
    1.50 +    val abs_eq = ax_abs_iso RS (allI RS injection_eq) RS iffD1;
    1.51 +    val simps = [up_eq, spair_eq];
    1.52 +    val tacs = [
    1.53 +      dtac abs_eq 1,
    1.54 +      REPEAT (dresolve_tac [sinl_inject, sinr_inject] 1),
    1.55 +      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
    1.56 +  in map (fn (con,args) => pgterm (op ===) con args tacs) cons' end;
    1.57  end;
    1.58  
    1.59  (* ----- theorems concerning one induction step ----------------------------- *)