src/HOLCF/domain/theorems.ML
changeset 8149 941afb897532
parent 7906 0576dad973b1
child 8438 b8389b4fca9c
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:22:02 2000 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Jan 28 11:23:41 2000 +0100
     1.3 @@ -27,14 +27,6 @@
     1.4  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
     1.5                                  | prems=> (cut_facts_tac prems 1)::tacsf);
     1.6  
     1.7 -fun REPEAT_DETERM_UNTIL p tac = 
     1.8 -let fun drep st = if p st then Seq.single st
     1.9 -                          else (case Seq.pull(tac st) of
    1.10 -                                  None        => Seq.empty
    1.11 -                                | Some(st',_) => drep st')
    1.12 -in drep end;
    1.13 -val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
    1.14 -
    1.15  local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
    1.16  val kill_neq_tac = dtac trueI2 end;
    1.17  fun case_UU_tac rews i v =      case_tac (v^"=UU") i THEN
    1.18 @@ -131,7 +123,7 @@
    1.19                                  rewrite_goals_tac axs_con_def,
    1.20                                  dtac iso_swap 1,
    1.21                                  simp_tac HOLCF_ss 1,
    1.22 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
    1.23 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
    1.24              fun sum_tac [(_,args)]       [p]        = 
    1.25                                  prod_tac args THEN sum_rest_tac p
    1.26              |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
    1.27 @@ -159,7 +151,7 @@
    1.28                                  else sum_tac cons (tl prems)])end;
    1.29  val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
    1.30                                  rtac casedist 1,
    1.31 -                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
    1.32 +                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
    1.33  end;
    1.34  
    1.35  local 
    1.36 @@ -197,7 +189,7 @@
    1.37                        defined(%%(dis_name con)`%x_name)) [
    1.38                                  rtac casedist 1,
    1.39                                  contr_tac 1,
    1.40 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
    1.41 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac 
    1.42                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
    1.43  in dis_stricts @ dis_defins @ dis_apps end;
    1.44  
    1.45 @@ -237,7 +229,7 @@
    1.46                          defined(%%(sel_of arg)`%x_name)) [
    1.47                                  rtac casedist 1,
    1.48                                  contr_tac 1,
    1.49 -                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
    1.50 +                                DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac 
    1.51                                               (HOLCF_ss addsimps sel_apps) 1))]) 
    1.52                   (filter_out is_lazy (snd(hd cons))) else [];
    1.53  val sel_rews = sel_stricts @ sel_defins @ sel_apps;