--- a/src/Sequents/ILL.ML Mon Nov 20 23:47:10 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-(* Title: Sequents/ILL.ML
- ID: $Id$
- Author: Sara Kalvala and Valeria de Paiva
- Copyright 1992 University of Cambridge
-*)
-
-val lazy_cs = empty_pack
- add_safes [tensl, conjr, disjl, promote0,
- context2,context3]
- add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
- impr, tensr, impl, derelict, weaken,
- promote1, promote2,context1,context4a,context4b];
-
-fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
-
-fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 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";
-
-Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
-by (rtac impr 1);
-by (rtac contract 1);
-by (assume_tac 1);
-qed "impr_contract";
-
-
-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 (the_context ()) "$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 _ = goal (the_context ()) "$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 _ = goal (the_context ()) "A -o B, A |- B";
-by (rtac impl 1);
-by (rtac identity 2);
-by (rtac identity 2);
-by (rtac context1 1);
-qed "ll_mp";
-
-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";
-
-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 _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
-by (best_tac lazy_cs 1);
-qed "or_to_and";
-
-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 _ = goal (the_context ()) "((!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";
-
-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";
-
-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 (the_context ()) 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];
-
-val power_cs = safe_cs add_unsafes [impr_contr_der];
-
-fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
-
-fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
-
-
-(* some examples from Troelstra and van Dalen
-
-auto1 "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
-
-auto1 "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
-
-auto1 "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
-\ (!A) -o ( (! ((!B) -o 0)) -o 0)";
-
-
-auto2 "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |- \
-\ (!((! ((!A) -o B) ) -o 0)) -o 0";
-
-
- *)
--- a/src/Sequents/ILL.thy Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/ILL.thy Tue Nov 21 00:00:39 2006 +0100
@@ -123,6 +123,185 @@
context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G"
context5: "$F, $G :=: $H ==> $G, $F :=: $H"
-ML {* use_legacy_bindings (the_context ()) *}
+
+ML {*
+
+val lazy_cs = empty_pack
+ add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
+ thm "context2", thm "context3"]
+ add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
+ thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
+ thm "derelict", thm "weaken", thm "promote1", thm "promote2",
+ thm "context1", thm "context4a", thm "context4b"];
+
+local
+ val promote0 = thm "promote0"
+ val promote1 = thm "promote1"
+ val promote2 = thm "promote2"
+in
+
+fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
end
+*}
+
+method_setup best_lazy =
+{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac lazy_cs)) *}
+"lazy classical reasoning"
+
+lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
+ apply (rule derelict)
+ apply (rule impl)
+ apply (rule_tac [2] identity)
+ apply (rule context1)
+ apply assumption
+ done
+
+lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
+ apply (rule contract)
+ apply (rule_tac A = " (!A) >< (!B) " in cut)
+ apply (rule_tac [2] tensr)
+ prefer 3
+ apply (subgoal_tac "! (A && B) |- !A")
+ apply assumption
+ apply best_lazy
+ prefer 3
+ apply (subgoal_tac "! (A && B) |- !B")
+ apply assumption
+ apply best_lazy
+ apply (rule_tac [2] context1)
+ apply (rule_tac [2] tensl)
+ prefer 2 apply (assumption)
+ apply (rule context3)
+ apply (rule context3)
+ apply (rule context1)
+ done
+
+lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
+ apply (rule impr)
+ apply (rule contract)
+ apply assumption
+ done
+
+lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
+ apply (rule impr)
+ apply (rule contract)
+ apply (rule derelict)
+ apply assumption
+ done
+
+lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
+ apply (rule impl)
+ apply (rule_tac [3] identity)
+ apply (rule context3)
+ apply (rule context1)
+ apply (rule zerol)
+ done
+
+
+lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
+ apply (rule impl)
+ apply (rule_tac [3] identity)
+ apply (rule context3)
+ apply (rule context1)
+ apply (rule zerol)
+ done
+
+lemma ll_mp: "A -o B, A |- B"
+ apply (rule impl)
+ apply (rule_tac [2] identity)
+ apply (rule_tac [2] identity)
+ apply (rule context1)
+ done
+
+lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
+ apply (rule_tac A = "B" in cut)
+ apply (rule_tac [2] ll_mp)
+ prefer 2 apply (assumption)
+ apply (rule context3)
+ apply (rule context3)
+ apply (rule context1)
+ done
+
+lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
+ apply (rule_tac A = "B" in cut)
+ apply (rule_tac [2] ll_mp)
+ prefer 2 apply (assumption)
+ apply (rule context3)
+ apply (rule context3)
+ apply (rule context1)
+ done
+
+lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
+ by best_lazy
+
+lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>
+ $F, !((!(A ++ B)) -o 0), $G |- C"
+ apply (rule cut)
+ apply (rule_tac [2] or_to_and)
+ prefer 2 apply (assumption)
+ apply (rule context3)
+ apply (rule context1)
+ done
+
+lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
+ apply (rule impr)
+ apply (rule conj_lemma)
+ apply (rule disjl)
+ apply (rule mp_rule1, best_lazy)+
+ done
+
+lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
+ by best_lazy
+
+lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
+ apply (rule impr)
+ apply (rule contract)
+ apply (rule impl)
+ apply (rule_tac [3] identity)
+ apply (rule context1)
+ apply best_lazy
+ done
+
+lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
+ apply (rule_tac A = "!A -o 0" in cut)
+ apply (rule_tac [2] a_not_a)
+ prefer 2 apply (assumption)
+ apply best_lazy
+ done
+
+ML {*
+
+val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
+ thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
+ thm "a_not_a_rule"]
+ add_unsafes [thm "aux_impl"];
+
+val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
+*}
+
+
+method_setup best_safe =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
+
+method_setup best_power =
+ {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
+
+
+(* Some examples from Troelstra and van Dalen *)
+
+lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
+ by best_safe
+
+lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
+ by best_safe
+
+lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
+ (!A) -o ( (! ((!B) -o 0)) -o 0)"
+ by best_safe
+
+lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |-
+ (!((! ((!A) -o B) ) -o 0)) -o 0"
+ by best_power
+
+end
--- a/src/Sequents/ILL_predlog.thy Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/ILL_predlog.thy Tue Nov 21 00:00:39 2006 +0100
@@ -29,107 +29,102 @@
(* another translations for linear implication:
"[* A > B *]" == "!([*A*] -o [*B*])" *)
-method_setup auto1 =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
-method_setup auto2 =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
-
(* from [kleene 52] pp 118,119 *)
lemma k49a: "|- [* A > ( - ( - A)) *]"
- by auto1
+ by best_safe
lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
- by auto1
+ by best_safe
lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
- by auto1
+ by best_safe
lemma k50a: "|- [* - (A = - A) *]"
- by auto2
+ by best_power
lemma k51a: "|- [* - - (A | - A) *]"
- by auto1
+ by best_safe
lemma k51b: "|- [* - - (- - A > A) *]"
- by auto2
+ by best_power
lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
- by auto1
+ by best_safe
lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
- by auto1
+ by best_safe
lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
- by auto1
+ by best_safe
lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
- by auto2
+ by best_power
lemma k58a: "|- [* (A > B) > - (A & -B) *]"
- by auto1
+ by best_safe
lemma k58b: "|- [* (A > -B) = -(A & B) *]"
- by auto1
+ by best_safe
lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
- by auto1
+ by best_safe
lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
- by auto1
+ by best_safe
lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
- by auto1
+ by best_safe
lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
- by auto1
+ by best_safe
lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
- by auto1
+ by best_safe
lemma k59a: "|- [* (-A | B) > (A > B) *]"
- by auto1
+ by best_safe
lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
- by auto2
+ by best_power
lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
- by auto2
+ by best_power
lemma k60a: "|- [* (A & B) > - (A > -B) *]"
- by auto1
+ by best_safe
lemma k60b: "|- [* (A & -B) > - (A > B) *]"
- by auto1
+ by best_safe
lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
- by auto1
+ by best_safe
lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
- by auto1
+ by best_safe
lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
- by auto1
+ by best_safe
lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
- by auto1
+ by best_safe
lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
- by auto2
+ by best_power
lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
- by auto1
+ by best_safe
lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
- by auto1
+ by best_safe
lemma k61a: "|- [* (A | B) > (-A > B) *]"
- by auto1
+ by best_safe
lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
- by auto2
+ by best_power
lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
- by auto1
+ by best_safe
end
--- a/src/Sequents/IsaMakefile Mon Nov 20 23:47:10 2006 +0100
+++ b/src/Sequents/IsaMakefile Tue Nov 21 00:00:39 2006 +0100
@@ -26,7 +26,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.thy LK.thy \
+$(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
ILL_predlog.thy Washing.thy
@$(ISATOOL) usedir -b $(OUT)/Pure Sequents