src/Sequents/ILL.ML

--- a/src/Sequents/ILL.ML	Thu Jul 06 11:23:39 2000 +0200
+++ b/src/Sequents/ILL.ML	Thu Jul 06 11:24:09 2000 +0200
@@ -16,102 +16,134 @@
 
 fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
 
-val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B"
-(fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2
-	THEN rtac context1 1 THEN rtac (hd(prems)) 1]);
+Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
+by (rtac derelict 1);
+by (rtac impl 1);
+by (rtac identity 2);
+by (rtac context1 1);
+by (assume_tac 1);
+qed "aux_impl";
+
+Goal " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C";
+by (rtac contract 1);
+by (res_inst_tac [("A","(!A) >< (!B)")] cut 1);
+by (rtac tensr 2);
+by (rtac (auto "! (A && B) |- !A") 3);
+by (rtac (auto "! (A && B) |- !B") 3);
+by (rtac context1 2);
+by (rtac tensl 2);
+by (assume_tac 2);
+by (rtac context3 1);
+by (rtac context3 1);
+by (rtac context1 1);
+qed "conj_lemma";
 
-val conj_lemma =
-prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
-(fn prems => [rtac contract 1,
-	res_inst_tac [("A","(!A) >< (!B)")] cut 1,
-	rtac tensr 2,
-	rtac (auto "! (A && B) |- !A") 3,
-	rtac (auto "! (A && B) |- !B") 3,
-	rtac context1 2,
-	rtac tensl 2,
-	rtac (hd(prems)) 2,
-	rtac context3 1,
-	rtac context3 1,
-	rtac context1 1]);
+Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
+by (rtac impr 1);
+by (rtac contract 1);
+by (assume_tac 1);
+qed "impr_contract";
+
 
-val impr_contract =
-prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B"
-(fn prems => [rtac impr 1 THEN rtac contract 1
-		 THEN rtac (hd(prems)) 1]);
+Goal "A, !A, $G |- B ==> $G |- (!A) -o B";
+by (rtac impr 1);
+by (rtac contract 1);
+by (rtac derelict 1);
+by (assume_tac 1);
+qed "impr_contr_der";
+
+val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
+by (rtac impl 1);
+by (rtac identity 3);
+by (rtac context3 1);
+by (rtac context1 1);
+by (rtac zerol 1);
+qed "contrad1";
 
 
-val impr_contr_der =
-prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B"
-(fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1
-		 THEN rtac (hd(prems)) 1]);
-
-val contrad1 =
-prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A"
-(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
-	  rtac zerol 1]);
+val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
+by (rtac impl 1);
+by (rtac identity 3);
+by (rtac context3 1);
+by (rtac context1 1);
+by (rtac zerol 1);
+qed "contrad2";
 
-
-val contrad2 =
-prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A"
-(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
-	  rtac zerol 1]);
-
-val ll_mp =
-prove_goal thy "A -o B, A |- B"
-(fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2
-	 THEN rtac context1 1]);
+val _ = goal thy "A -o B, A |- B";
+by (rtac impl 1);
+by (rtac identity 2);
+by (rtac identity 2);
+by (rtac context1 1);
+qed "ll_mp";
 
-val mp_rule1 =
-prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
-(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
-		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
-		rtac context1 1]);
+Goal "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C";
+by (res_inst_tac [("A","B")] cut 1);
+by (rtac ll_mp 2);
+by (assume_tac 2);
+by (rtac context3 1);
+by (rtac context3 1);
+by (rtac context1 1);
+qed "mp_rule1";
 
-val mp_rule2 =
-prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
-(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
-		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
-		rtac context1 1]);
+Goal "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C";
+by (res_inst_tac [("A","B")] cut 1);
+by (rtac ll_mp 2);
+by (assume_tac 2);
+by (rtac context3 1);
+by (rtac context3 1);
+by (rtac context1 1);
+qed "mp_rule2";
 
-val or_to_and =
-prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
-(fn _ => [best_tac lazy_cs 1]);
+val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
+by (best_tac lazy_cs 1);
+qed "or_to_and";
 
-val o_a_rule =
-prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
-\         $F, !((!(A ++ B)) -o 0), $G |- C"
-(fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2,
-		rtac context3 1, rtac context1 1]);
+Goal "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
+\         $F, !((!(A ++ B)) -o 0), $G |- C";
+by (rtac cut 1);
+by (rtac or_to_and 2);
+by (assume_tac 2);
+by (rtac context3 1);
+by (rtac context1 1);
+qed "o_a_rule";
 
 
 
-val conj_imp =
- prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
-(fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1,
-	  ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]);
+val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
+by (rtac impr 1);
+by (rtac conj_lemma 1);
+by (rtac disjl 1);
+by (ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs));
+qed "conj_imp";
 
 
 val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
 
-val a_not_a =
-prove_goal thy "!A -o (!A -o 0) |- !A -o 0"
-     (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1,
-	  rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]);
+Goal "!A -o (!A -o 0) |- !A -o 0";
+by (rtac impr 1);
+by (rtac contract 1);
+by (rtac impl 1);
+by (rtac identity 3);
+by (rtac context1 1);
+by (best_tac lazy_cs 1);
+qed "a_not_a";
 
-val a_not_a_rule =
-prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
- (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1,
-               rtac a_not_a 2 THEN rtac (hd(prems)) 2
-		 THEN best_tac lazy_cs 1]);
+Goal "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B";
+by (res_inst_tac [("A","!A -o 0")] cut 1);
+by (rtac a_not_a 2);
+by (assume_tac 2);
+by (best_tac lazy_cs 1);
+qed "a_not_a_rule";
 
 fun thm_to_rule x y =
-prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 2,
-				best_tac lazy_cs 1]);
+    prove_goal thy x
+      (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
+	 	     (best_tac lazy_cs 1)]);
 
 val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
-			contrad2, mp_rule1, mp_rule2, o_a_rule,
-			a_not_a_rule]
-		add_unsafes [aux_impl];
+				 contrad2, mp_rule1, mp_rule2, o_a_rule,
+				 a_not_a_rule]
+		      add_unsafes [aux_impl];
 
 val power_cs = safe_cs add_unsafes [impr_contr_der];