src/CCL/ccl.ML
changeset 8 c3d2c6dcf3f0
parent 0 a5a9c433f639
child 280 fb379160f4de
     1.1 --- a/src/CCL/ccl.ML	Fri Sep 17 16:52:10 1993 +0200
     1.2 +++ b/src/CCL/ccl.ML	Mon Sep 20 17:02:11 1993 +0200
     1.3 @@ -10,30 +10,10 @@
     1.4  
     1.5  val ccl_data_defs = [apply_def,fix_def];
     1.6  
     1.7 -(*** Simplifier for pre-order and equality ***)
     1.8 -
     1.9 -structure CCL_SimpData : SIMP_DATA =
    1.10 -  struct
    1.11 -  val refl_thms		= [refl, po_refl, iff_refl]
    1.12 -  val trans_thms	= [trans, iff_trans, po_trans]
    1.13 -  val red1		= iffD1
    1.14 -  val red2		= iffD2
    1.15 -  val mk_rew_rules	= mk_rew_rules
    1.16 -  val case_splits	= []         (*NO IF'S!*)
    1.17 -  val norm_thms		= norm_thms
    1.18 -  val subst_thms	= [subst];
    1.19 -  val dest_red		= dest_red
    1.20 -  end;
    1.21 -
    1.22 -structure CCL_Simp = SimpFun(CCL_SimpData);
    1.23 -open CCL_Simp;
    1.24 -
    1.25 -val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps));
    1.26 -
    1.27  val po_refl_iff_T = make_iff_T po_refl;
    1.28  
    1.29 -val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs)
    1.30 -                     addrews  ([po_refl_iff_T] @ FOL_rews @ mem_rews);
    1.31 +val CCL_ss = FOL_ss addcongs set_congs
    1.32 +                    addsimps  ([po_refl_iff_T] @ mem_rews);
    1.33  
    1.34  (*** Congruence Rules ***)
    1.35  
    1.36 @@ -46,7 +26,7 @@
    1.37   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.38  
    1.39  goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
    1.40 -by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1);
    1.41 +by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
    1.42  by (fast_tac (set_cs addIs [po_abstractn]) 1);
    1.43  val abstractn = standard (allI RS (result() RS mp));
    1.44  
    1.45 @@ -61,11 +41,6 @@
    1.46     in do_prems 1 (prems_of thm) thm
    1.47     end;
    1.48  
    1.49 -fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs); 
    1.50 -
    1.51 -val ccl_congs = ccl_mk_congs CCL.thy 
    1.52 - ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"];
    1.53 -
    1.54  val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
    1.55  
    1.56  (*** Termination and Divergence ***)
    1.57 @@ -85,17 +60,16 @@
    1.58  by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
    1.59  val eq_lemma = result();
    1.60  
    1.61 -fun mk_inj_rl thy rews congs s = 
    1.62 +fun mk_inj_rl thy rews s = 
    1.63        let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
    1.64            val inj_lemmas = flat (map mk_inj_lemmas rews);
    1.65            val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
    1.66                              eresolve_tac inj_lemmas 1 ORELSE
    1.67 -                            ASM_SIMP_TAC (CCL_ss addrews rews 
    1.68 -                                                 addcongs congs) 1)
    1.69 +                            asm_simp_tac (CCL_ss addsimps rews) 1)
    1.70        in prove_goal thy s (fn _ => [tac])
    1.71        end;
    1.72  
    1.73 -val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs)
    1.74 +val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
    1.75                 ["<a,b> = <a',b'> <-> (a=a' & b=b')",
    1.76                  "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
    1.77  
    1.78 @@ -124,7 +98,7 @@
    1.79    fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
    1.80  
    1.81    val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
    1.82 -                   (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 1]) RS mp;
    1.83 +                   (fn _ => [simp_tac CCL_ss 1]) RS mp;
    1.84    fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL 
    1.85                             [distinctness RS notE,sym RS (distinctness RS notE)];
    1.86  in
    1.87 @@ -143,7 +117,7 @@
    1.88  
    1.89  fun mk_dstnct_thms thy defs inj_rls xs = 
    1.90            let fun mk_dstnct_thm rls s = prove_goalw thy defs s 
    1.91 -                               (fn _ => [SIMP_TAC (CCL_ss addrews (rls@inj_rls)) 1])
    1.92 +                               (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1])
    1.93            in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
    1.94  
    1.95  fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
    1.96 @@ -158,7 +132,7 @@
    1.97  val XH_to_Es = map XH_to_E;
    1.98  
    1.99  val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
   1.100 -val ccl_ss = CCL_ss addrews ccl_rews addcongs ccl_congs;
   1.101 +val ccl_ss = CCL_ss addsimps ccl_rews;
   1.102  
   1.103  val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) 
   1.104                      addSDs (XH_to_Ds ccl_injs);
   1.105 @@ -179,7 +153,7 @@
   1.106  br monoI 1;
   1.107  by (safe_tac ccl_cs);
   1.108  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.109 -by (ALLGOALS (SIMP_TAC ccl_ss));
   1.110 +by (ALLGOALS (simp_tac ccl_ss));
   1.111  by (ALLGOALS (fast_tac set_cs));
   1.112  val POgen_mono = result();
   1.113  
   1.114 @@ -194,7 +168,7 @@
   1.115    "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
   1.116  \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
   1.117  \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
   1.118 -by (SIMP_TAC (ccl_ss addrews [PO_iff]) 1);
   1.119 +by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
   1.120  br (rewrite_rule [POgen_def,SIM_def] 
   1.121                   (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   1.122  br (iff_refl RS XHlemma2) 1;
   1.123 @@ -202,27 +176,27 @@
   1.124  
   1.125  goal CCL.thy "bot [= b";
   1.126  br (poXH RS iffD2) 1;
   1.127 -by (SIMP_TAC ccl_ss 1);
   1.128 +by (simp_tac ccl_ss 1);
   1.129  val po_bot = result();
   1.130  
   1.131  goal CCL.thy "a [= bot --> a=bot";
   1.132  br impI 1;
   1.133  bd (poXH RS iffD1) 1;
   1.134  be rev_mp 1;
   1.135 -by (SIMP_TAC ccl_ss 1);
   1.136 +by (simp_tac ccl_ss 1);
   1.137  val bot_poleast = result() RS mp;
   1.138  
   1.139  goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
   1.140  br (poXH RS iff_trans) 1;
   1.141 -by (SIMP_TAC ccl_ss 1);
   1.142 +by (simp_tac ccl_ss 1);
   1.143  by (fast_tac ccl_cs 1);
   1.144  val po_pair = result();
   1.145  
   1.146  goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
   1.147  br (poXH RS iff_trans) 1;
   1.148 -by (SIMP_TAC ccl_ss 1);
   1.149 +by (simp_tac ccl_ss 1);
   1.150  by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
   1.151 -by (ASM_SIMP_TAC ccl_ss 1);
   1.152 +by (asm_simp_tac ccl_ss 1);
   1.153  by (fast_tac ccl_cs 1);
   1.154  val po_lam = result();
   1.155  
   1.156 @@ -275,7 +249,7 @@
   1.157  
   1.158  fun mk_thm s = prove_goal CCL.thy s (fn _ => 
   1.159                            [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
   1.160 -                           ALLGOALS (SIMP_TAC ccl_ss),
   1.161 +                           ALLGOALS (simp_tac ccl_ss),
   1.162                             REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
   1.163  
   1.164  val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
   1.165 @@ -300,7 +274,7 @@
   1.166  br monoI 1;
   1.167  by (safe_tac set_cs);
   1.168  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.169 -by (ALLGOALS (SIMP_TAC ccl_ss));
   1.170 +by (ALLGOALS (simp_tac ccl_ss));
   1.171  by (ALLGOALS (fast_tac set_cs));
   1.172  val EQgen_mono = result();
   1.173  
   1.174 @@ -321,7 +295,7 @@
   1.175  \             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   1.176  \             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
   1.177  be rev_mp 1;
   1.178 -by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 1);
   1.179 +by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
   1.180  br (rewrite_rule [EQgen_def,SIM_def]
   1.181                   (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   1.182  br (iff_refl RS XHlemma2) 1;
   1.183 @@ -345,7 +319,7 @@
   1.184  
   1.185  goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
   1.186  by (safe_tac ccl_cs);
   1.187 -by (SIMP_TAC ccl_ss 1);
   1.188 +by (simp_tac ccl_ss 1);
   1.189  val cond_eta = result() RS mp;
   1.190  
   1.191  goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";