src/HOLCF/Tools/domain/domain_theorems.ML
changeset 26012 f6917792f8a4
parent 25895 0eaadfa8889e
child 26336 a0e2b706ce73
     1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 10:20:00 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 18:00:12 2008 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4    fun dis_app c (con, args) =
     1.5      let
     1.6        val lhs = %%:(dis_name c) ` con_app con args;
     1.7 -      val rhs = %%:(if con = c then TT_N else FF_N);
     1.8 +      val rhs = if con = c then TT else FF;
     1.9        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    1.10        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.11      in pg axs_dis_def goal tacs end;
    1.12 @@ -313,8 +313,8 @@
    1.13        val lhs = %%:(mat_name c) ` con_app con args;
    1.14        val rhs =
    1.15          if con = c
    1.16 -        then %%:returnN ` mk_ctuple (map %# args)
    1.17 -        else %%:failN;
    1.18 +        then mk_return (mk_ctuple (map %# args))
    1.19 +        else mk_fail;
    1.20        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    1.21        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.22      in pg axs_mat_def goal tacs end;
    1.23 @@ -328,11 +328,11 @@
    1.24  local
    1.25    fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
    1.26  
    1.27 -  fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
    1.28 +  fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
    1.29  
    1.30 -  fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
    1.31 +  fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
    1.32      | pat_rhs (con,args) =
    1.33 -        (%%:branchN $ foldr1 cpair_pat (ps args))
    1.34 +        (mk_branch (mk_ctuple_pat (ps args)))
    1.35            `(%:"rhs")`(mk_ctuple (map %# args));
    1.36  
    1.37    fun pat_strict c =
    1.38 @@ -346,7 +346,7 @@
    1.39      let
    1.40        val axs = @{thm branch_def} :: axs_pat_def;
    1.41        val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
    1.42 -      val rhs = if con = fst c then pat_rhs c else %%:failN;
    1.43 +      val rhs = if con = fst c then pat_rhs c else mk_fail;
    1.44        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    1.45        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.46      in pg axs goal tacs end;
    1.47 @@ -389,8 +389,8 @@
    1.48      [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
    1.49    fun con_compact (con, args) =
    1.50      let
    1.51 -      val concl = mk_trp (%%:compactN $ con_app con args);
    1.52 -      val goal = lift (fn x => %%:compactN $ %#x) (args, concl);
    1.53 +      val concl = mk_trp (mk_compact (con_app con args));
    1.54 +      val goal = lift (fn x => mk_compact (%#x)) (args, concl);
    1.55        val tacs = [
    1.56          rtac (iso_locale RS iso_compact_abs) 1,
    1.57          REPEAT (resolve_tac rules 1 ORELSE atac 1)];
    1.58 @@ -890,7 +890,7 @@
    1.59  
    1.60          val goal =
    1.61            let
    1.62 -            fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n));
    1.63 +            fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
    1.64              fun concf n dn = %:(P_name n) $ %:(x_name n);
    1.65            in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
    1.66          fun tacf prems =