removal of batch style, and tidying
authorpaulson
Thu Jul 06 11:24:09 2000 +0200 (2000-07-06)
changeset 9259103acc345f75
parent 9258 2121ff73a37d
child 9260 678e718a5a86
removal of batch style, and tidying
src/Sequents/ILL.ML
src/Sequents/LK0.ML
src/Sequents/simpdata.ML
     1.1 --- a/src/Sequents/ILL.ML	Thu Jul 06 11:23:39 2000 +0200
     1.2 +++ b/src/Sequents/ILL.ML	Thu Jul 06 11:24:09 2000 +0200
     1.3 @@ -16,102 +16,134 @@
     1.4  
     1.5  fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
     1.6  
     1.7 -val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B"
     1.8 -(fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2
     1.9 -	THEN rtac context1 1 THEN rtac (hd(prems)) 1]);
    1.10 +Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
    1.11 +by (rtac derelict 1);
    1.12 +by (rtac impl 1);
    1.13 +by (rtac identity 2);
    1.14 +by (rtac context1 1);
    1.15 +by (assume_tac 1);
    1.16 +qed "aux_impl";
    1.17 +
    1.18 +Goal " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C";
    1.19 +by (rtac contract 1);
    1.20 +by (res_inst_tac [("A","(!A) >< (!B)")] cut 1);
    1.21 +by (rtac tensr 2);
    1.22 +by (rtac (auto "! (A && B) |- !A") 3);
    1.23 +by (rtac (auto "! (A && B) |- !B") 3);
    1.24 +by (rtac context1 2);
    1.25 +by (rtac tensl 2);
    1.26 +by (assume_tac 2);
    1.27 +by (rtac context3 1);
    1.28 +by (rtac context3 1);
    1.29 +by (rtac context1 1);
    1.30 +qed "conj_lemma";
    1.31  
    1.32 -val conj_lemma =
    1.33 -prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
    1.34 -(fn prems => [rtac contract 1,
    1.35 -	res_inst_tac [("A","(!A) >< (!B)")] cut 1,
    1.36 -	rtac tensr 2,
    1.37 -	rtac (auto "! (A && B) |- !A") 3,
    1.38 -	rtac (auto "! (A && B) |- !B") 3,
    1.39 -	rtac context1 2,
    1.40 -	rtac tensl 2,
    1.41 -	rtac (hd(prems)) 2,
    1.42 -	rtac context3 1,
    1.43 -	rtac context3 1,
    1.44 -	rtac context1 1]);
    1.45 +Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
    1.46 +by (rtac impr 1);
    1.47 +by (rtac contract 1);
    1.48 +by (assume_tac 1);
    1.49 +qed "impr_contract";
    1.50 +
    1.51  
    1.52 -val impr_contract =
    1.53 -prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B"
    1.54 -(fn prems => [rtac impr 1 THEN rtac contract 1
    1.55 -		 THEN rtac (hd(prems)) 1]);
    1.56 +Goal "A, !A, $G |- B ==> $G |- (!A) -o B";
    1.57 +by (rtac impr 1);
    1.58 +by (rtac contract 1);
    1.59 +by (rtac derelict 1);
    1.60 +by (assume_tac 1);
    1.61 +qed "impr_contr_der";
    1.62 +
    1.63 +val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
    1.64 +by (rtac impl 1);
    1.65 +by (rtac identity 3);
    1.66 +by (rtac context3 1);
    1.67 +by (rtac context1 1);
    1.68 +by (rtac zerol 1);
    1.69 +qed "contrad1";
    1.70  
    1.71  
    1.72 -val impr_contr_der =
    1.73 -prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B"
    1.74 -(fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1
    1.75 -		 THEN rtac (hd(prems)) 1]);
    1.76 -
    1.77 -val contrad1 =
    1.78 -prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A"
    1.79 -(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    1.80 -	  rtac zerol 1]);
    1.81 +val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
    1.82 +by (rtac impl 1);
    1.83 +by (rtac identity 3);
    1.84 +by (rtac context3 1);
    1.85 +by (rtac context1 1);
    1.86 +by (rtac zerol 1);
    1.87 +qed "contrad2";
    1.88  
    1.89 -
    1.90 -val contrad2 =
    1.91 -prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A"
    1.92 -(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    1.93 -	  rtac zerol 1]);
    1.94 -
    1.95 -val ll_mp =
    1.96 -prove_goal thy "A -o B, A |- B"
    1.97 -(fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2
    1.98 -	 THEN rtac context1 1]);
    1.99 +val _ = goal thy "A -o B, A |- B";
   1.100 +by (rtac impl 1);
   1.101 +by (rtac identity 2);
   1.102 +by (rtac identity 2);
   1.103 +by (rtac context1 1);
   1.104 +qed "ll_mp";
   1.105  
   1.106 -val mp_rule1 =
   1.107 -prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
   1.108 -(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
   1.109 -		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
   1.110 -		rtac context1 1]);
   1.111 +Goal "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C";
   1.112 +by (res_inst_tac [("A","B")] cut 1);
   1.113 +by (rtac ll_mp 2);
   1.114 +by (assume_tac 2);
   1.115 +by (rtac context3 1);
   1.116 +by (rtac context3 1);
   1.117 +by (rtac context1 1);
   1.118 +qed "mp_rule1";
   1.119  
   1.120 -val mp_rule2 =
   1.121 -prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
   1.122 -(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
   1.123 -		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
   1.124 -		rtac context1 1]);
   1.125 +Goal "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C";
   1.126 +by (res_inst_tac [("A","B")] cut 1);
   1.127 +by (rtac ll_mp 2);
   1.128 +by (assume_tac 2);
   1.129 +by (rtac context3 1);
   1.130 +by (rtac context3 1);
   1.131 +by (rtac context1 1);
   1.132 +qed "mp_rule2";
   1.133  
   1.134 -val or_to_and =
   1.135 -prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
   1.136 -(fn _ => [best_tac lazy_cs 1]);
   1.137 +val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
   1.138 +by (best_tac lazy_cs 1);
   1.139 +qed "or_to_and";
   1.140  
   1.141 -val o_a_rule =
   1.142 -prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
   1.143 -\         $F, !((!(A ++ B)) -o 0), $G |- C"
   1.144 -(fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2,
   1.145 -		rtac context3 1, rtac context1 1]);
   1.146 +Goal "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
   1.147 +\         $F, !((!(A ++ B)) -o 0), $G |- C";
   1.148 +by (rtac cut 1);
   1.149 +by (rtac or_to_and 2);
   1.150 +by (assume_tac 2);
   1.151 +by (rtac context3 1);
   1.152 +by (rtac context1 1);
   1.153 +qed "o_a_rule";
   1.154  
   1.155  
   1.156  
   1.157 -val conj_imp =
   1.158 - prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
   1.159 -(fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1,
   1.160 -	  ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]);
   1.161 +val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
   1.162 +by (rtac impr 1);
   1.163 +by (rtac conj_lemma 1);
   1.164 +by (rtac disjl 1);
   1.165 +by (ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs));
   1.166 +qed "conj_imp";
   1.167  
   1.168  
   1.169  val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
   1.170  
   1.171 -val a_not_a =
   1.172 -prove_goal thy "!A -o (!A -o 0) |- !A -o 0"
   1.173 -     (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1,
   1.174 -	  rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]);
   1.175 +Goal "!A -o (!A -o 0) |- !A -o 0";
   1.176 +by (rtac impr 1);
   1.177 +by (rtac contract 1);
   1.178 +by (rtac impl 1);
   1.179 +by (rtac identity 3);
   1.180 +by (rtac context1 1);
   1.181 +by (best_tac lazy_cs 1);
   1.182 +qed "a_not_a";
   1.183  
   1.184 -val a_not_a_rule =
   1.185 -prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   1.186 - (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1,
   1.187 -               rtac a_not_a 2 THEN rtac (hd(prems)) 2
   1.188 -		 THEN best_tac lazy_cs 1]);
   1.189 +Goal "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B";
   1.190 +by (res_inst_tac [("A","!A -o 0")] cut 1);
   1.191 +by (rtac a_not_a 2);
   1.192 +by (assume_tac 2);
   1.193 +by (best_tac lazy_cs 1);
   1.194 +qed "a_not_a_rule";
   1.195  
   1.196  fun thm_to_rule x y =
   1.197 -prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 2,
   1.198 -				best_tac lazy_cs 1]);
   1.199 +    prove_goal thy x
   1.200 +      (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
   1.201 +	 	     (best_tac lazy_cs 1)]);
   1.202  
   1.203  val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
   1.204 -			contrad2, mp_rule1, mp_rule2, o_a_rule,
   1.205 -			a_not_a_rule]
   1.206 -		add_unsafes [aux_impl];
   1.207 +				 contrad2, mp_rule1, mp_rule2, o_a_rule,
   1.208 +				 a_not_a_rule]
   1.209 +		      add_unsafes [aux_impl];
   1.210  
   1.211  val power_cs = safe_cs add_unsafes [impr_contr_der];
   1.212  
     2.1 --- a/src/Sequents/LK0.ML	Thu Jul 06 11:23:39 2000 +0200
     2.2 +++ b/src/Sequents/LK0.ML	Thu Jul 06 11:24:09 2000 +0200
     2.3 @@ -149,15 +149,20 @@
     2.4  by (rtac thinR 1 THEN rtac prem 1);
     2.5  qed "backwards_impR";
     2.6  
     2.7 - 
     2.8 -qed_goal "conjunct1" thy "|-P&Q ==> |-P"
     2.9 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    2.10 +Goal "|-P&Q ==> |-P";
    2.11 +by (etac (thinR RS cut) 1);
    2.12 +by (Fast_tac 1);		
    2.13 +qed "conjunct1";
    2.14  
    2.15 -qed_goal "conjunct2" thy "|-P&Q ==> |-Q"
    2.16 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    2.17 +Goal "|-P&Q ==> |-Q";
    2.18 +by (etac (thinR RS cut) 1);
    2.19 +by (Fast_tac 1);		
    2.20 +qed "conjunct2";
    2.21  
    2.22 -qed_goal "spec" thy "|- (ALL x. P(x)) ==> |- P(x)"
    2.23 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    2.24 +Goal "|- (ALL x. P(x)) ==> |- P(x)";
    2.25 +by (etac (thinR RS cut) 1);
    2.26 +by (Fast_tac 1);		
    2.27 +qed "spec";
    2.28  
    2.29  (** Equality **)
    2.30  
     3.1 --- a/src/Sequents/simpdata.ML	Thu Jul 06 11:23:39 2000 +0200
     3.2 +++ b/src/Sequents/simpdata.ML	Thu Jul 06 11:24:09 2000 +0200
     3.3 @@ -104,12 +104,18 @@
     3.4   | _ => [r];
     3.5  
     3.6  
     3.7 -qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)"
     3.8 -    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
     3.9 +Goal "|- ~P ==> |- (P <-> False)";
    3.10 +by (etac (thinR RS cut) 1);
    3.11 +by (Fast_tac 1);		
    3.12 +qed "P_iff_F";
    3.13 +
    3.14  val iff_reflection_F = P_iff_F RS iff_reflection;
    3.15  
    3.16 -qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)"
    3.17 -    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
    3.18 +Goal "|- P ==> |- (P <-> True)";
    3.19 +by (etac (thinR RS cut) 1);
    3.20 +by (Fast_tac 1);		
    3.21 +qed "P_iff_T";
    3.22 +
    3.23  val iff_reflection_T = P_iff_T RS iff_reflection;
    3.24  
    3.25  (*Make meta-equalities.*)