installation of simplifier and classical reasoner, better rules etc
authorpaulson
Tue Jul 27 19:02:43 1999 +0200 (1999-07-27)
changeset 709886583034aacf
parent 7097 5ab37ed3d53c
child 7099 8142ccd13963
installation of simplifier and classical reasoner, better rules etc
src/Sequents/IsaMakefile
src/Sequents/Modal0.thy
src/Sequents/ROOT.ML
src/Sequents/Sequents.thy
src/Sequents/simpdata.ML
     1.1 --- a/src/Sequents/IsaMakefile	Tue Jul 27 19:01:46 1999 +0200
     1.2 +++ b/src/Sequents/IsaMakefile	Tue Jul 27 19:02:43 1999 +0200
     1.3 @@ -26,7 +26,8 @@
     1.4  Pure:
     1.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.6  
     1.7 -$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK.ML LK.thy ROOT.ML S4.ML \
     1.8 +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.ML LK0.thy LK.thy \
     1.9 +  modal.ML ROOT.ML simpdata.ML S4.ML \
    1.10    S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML
    1.11  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
    1.12  
    1.13 @@ -46,7 +47,7 @@
    1.14  Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
    1.15  
    1.16  $(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
    1.17 -  LK/prop.ML LK/quant.ML
    1.18 +  LK/prop.ML LK/quant.ML LK/Nat.thy LK/Nat.ML
    1.19  	@$(ISATOOL) usedir $(OUT)/Sequents LK
    1.20  
    1.21  
     2.1 --- a/src/Sequents/Modal0.thy	Tue Jul 27 19:01:46 1999 +0200
     2.2 +++ b/src/Sequents/Modal0.thy	Tue Jul 27 19:02:43 1999 +0200
     2.3 @@ -1,10 +1,10 @@
     2.4 -(*  Title:      Modal/modal0
     2.5 +(*  Title:      Sequents/Modal0
     2.6      ID:         $Id$
     2.7      Author:     Martin Coen
     2.8      Copyright   1991  University of Cambridge
     2.9  *)
    2.10  
    2.11 -Modal0 = LK +
    2.12 +Modal0 = LK0 +
    2.13  
    2.14  consts
    2.15    box           :: "o=>o"       ("[]_" [50] 50)
     3.1 --- a/src/Sequents/ROOT.ML	Tue Jul 27 19:01:46 1999 +0200
     3.2 +++ b/src/Sequents/ROOT.ML	Tue Jul 27 19:02:43 1999 +0200
     3.3 @@ -11,12 +11,17 @@
     3.4  
     3.5  print_depth 1;  
     3.6  
     3.7 +use "~~/src/Provers/simplifier.ML";
     3.8 +
     3.9  use_thy "Sequents";
    3.10  use "prover.ML";
    3.11  
    3.12  use_thy "LK";
    3.13 +use "simpdata.ML";
    3.14 +
    3.15  use_thy "ILL";
    3.16  
    3.17 +use "modal.ML";
    3.18  use_thy "Modal0";
    3.19  use_thy"T";
    3.20  use_thy"S4";
     4.1 --- a/src/Sequents/Sequents.thy	Tue Jul 27 19:01:46 1999 +0200
     4.2 +++ b/src/Sequents/Sequents.thy	Tue Jul 27 19:02:43 1999 +0200
     4.3 @@ -8,6 +8,8 @@
     4.4  
     4.5  Sequents = Pure +
     4.6  
     4.7 +global
     4.8 +
     4.9  types
    4.10    o 
    4.11  
    4.12 @@ -39,7 +41,7 @@
    4.13   SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    4.14    
    4.15   SeqO           :: "o => seqobj"                        ("_")
    4.16 - SeqId          :: "id => seqobj"                       ("$_")
    4.17 + SeqId          :: "'a => seqobj"                       ("$_")
    4.18   SeqVar         :: "var => seqobj"                      ("$_")
    4.19  
    4.20  types
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Sequents/simpdata.ML	Tue Jul 27 19:02:43 1999 +0200
     5.3 @@ -0,0 +1,209 @@
     5.4 +(*  Title:      Sequents/simpdata.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson
     5.7 +    Copyright   1999  University of Cambridge
     5.8 +
     5.9 +Instantiation of the generic simplifier for LK
    5.10 +
    5.11 +Borrows from the DC simplifier of Soren Heilmann.
    5.12 +
    5.13 +MAJOR LIMITATION: left-side sequent formulae are not added to the simpset.
    5.14 +  However, congruence rules for --> and & are available.
    5.15 +  The rule backwards_impR can be used to convert assumptions into right-side
    5.16 +  implications.
    5.17 +*)
    5.18 +
    5.19 +(*** Rewrite rules ***)
    5.20 +
    5.21 +fun prove_fun s = 
    5.22 + (writeln s;  
    5.23 +  prove_goal LK.thy s
    5.24 +   (fn prems => [ (cut_facts_tac prems 1), 
    5.25 +                  (fast_tac LK_pack 1) ]));
    5.26 +
    5.27 +val conj_simps = map prove_fun
    5.28 + ["|- P & True <-> P",      "|- True & P <-> P",
    5.29 +  "|- P & False <-> False", "|- False & P <-> False",
    5.30 +  "|- P & P <-> P", "        |- P & P & Q <-> P & Q",
    5.31 +  "|- P & ~P <-> False",    "|- ~P & P <-> False",
    5.32 +  "|- (P & Q) & R <-> P & (Q & R)"];
    5.33 +
    5.34 +val disj_simps = map prove_fun
    5.35 + ["|- P | True <-> True",  "|- True | P <-> True",
    5.36 +  "|- P | False <-> P",    "|- False | P <-> P",
    5.37 +  "|- P | P <-> P",        "|- P | P | Q <-> P | Q",
    5.38 +  "|- (P | Q) | R <-> P | (Q | R)"];
    5.39 +
    5.40 +val not_simps = map prove_fun
    5.41 + ["|- ~ False <-> True",   "|- ~ True <-> False"];
    5.42 +
    5.43 +val imp_simps = map prove_fun
    5.44 + ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
    5.45 +  "|- (False --> P) <-> True",     "|- (True --> P) <-> P", 
    5.46 +  "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
    5.47 +
    5.48 +val iff_simps = map prove_fun
    5.49 + ["|- (True <-> P) <-> P",         "|- (P <-> True) <-> P",
    5.50 +  "|- (P <-> P) <-> True",
    5.51 +  "|- (False <-> P) <-> ~P",       "|- (P <-> False) <-> ~P"];
    5.52 +
    5.53 +(*These are NOT supplied by default!*)
    5.54 +val distrib_simps  = map prove_fun
    5.55 + ["|- P & (Q | R) <-> P&Q | P&R", 
    5.56 +  "|- (Q | R) & P <-> Q&P | R&P",
    5.57 +  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
    5.58 +
    5.59 +(** Conversion into rewrite rules **)
    5.60 +
    5.61 +fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    5.62 +
    5.63 +
    5.64 +(*Make atomic rewrite rules*)
    5.65 +fun atomize r =
    5.66 + case concl_of r of
    5.67 +   Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    5.68 +     (case (forms_of_seq a, forms_of_seq c) of
    5.69 +	([], [p]) =>
    5.70 +	  (case p of
    5.71 +	       Const("op -->",_)$_$_ => atomize(r RS mp_R)
    5.72 +	     | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    5.73 +		   atomize(r RS conjunct2)
    5.74 +	     | Const("All",_)$_      => atomize(r RS spec)
    5.75 +	     | Const("True",_)       => []    (*True is DELETED*)
    5.76 +	     | Const("False",_)      => []    (*should False do something?*)
    5.77 +	     | _                     => [r])
    5.78 +      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
    5.79 + | _ => [r];
    5.80 +
    5.81 +
    5.82 +qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)"
    5.83 +    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
    5.84 +val iff_reflection_F = P_iff_F RS iff_reflection;
    5.85 +
    5.86 +qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)"
    5.87 +    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
    5.88 +val iff_reflection_T = P_iff_T RS iff_reflection;
    5.89 +
    5.90 +(*Make meta-equalities.*)
    5.91 +fun mk_meta_eq th = case concl_of th of
    5.92 +    Const("==",_)$_$_           => th
    5.93 +  | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    5.94 +	(case (forms_of_seq a, forms_of_seq c) of
    5.95 +	     ([], [p]) => 
    5.96 +		 (case p of
    5.97 +		      (Const("op =",_)$_$_)   => th RS eq_reflection
    5.98 +		    | (Const("op <->",_)$_$_) => th RS iff_reflection
    5.99 +		    | (Const("Not",_)$_)      => th RS iff_reflection_F
   5.100 +		    | _                       => th RS iff_reflection_T)
   5.101 +	   | _ => error ("addsimps: unable to use theorem\n" ^
   5.102 +			 string_of_thm th));
   5.103 +
   5.104 +
   5.105 +(*** Named rewrite rules proved for PL ***)
   5.106 +
   5.107 +fun prove nm thm  = qed_goal nm LK.thy thm
   5.108 +    (fn prems => [ (cut_facts_tac prems 1), 
   5.109 +                   (fast_tac LK_pack 1) ]);
   5.110 +
   5.111 +prove "conj_commute" "|- P&Q <-> Q&P";
   5.112 +prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)";
   5.113 +val conj_comms = [conj_commute, conj_left_commute];
   5.114 +
   5.115 +prove "disj_commute" "|- P|Q <-> Q|P";
   5.116 +prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)";
   5.117 +val disj_comms = [disj_commute, disj_left_commute];
   5.118 +
   5.119 +prove "conj_disj_distribL" "|- P&(Q|R) <-> (P&Q | P&R)";
   5.120 +prove "conj_disj_distribR" "|- (P|Q)&R <-> (P&R | Q&R)";
   5.121 +
   5.122 +prove "disj_conj_distribL" "|- P|(Q&R) <-> (P|Q) & (P|R)";
   5.123 +prove "disj_conj_distribR" "|- (P&Q)|R <-> (P|R) & (Q|R)";
   5.124 +
   5.125 +prove "imp_conj_distrib" "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)";
   5.126 +prove "imp_conj"         "|- ((P&Q)-->R)   <-> (P --> (Q --> R))";
   5.127 +prove "imp_disj"         "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)";
   5.128 +
   5.129 +prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)";
   5.130 +prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)";
   5.131 +
   5.132 +prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)";
   5.133 +prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)";
   5.134 +
   5.135 +prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
   5.136 +
   5.137 +prove "iff_refl" "|- (P <-> P)";
   5.138 +
   5.139 +
   5.140 +val [p1,p2] = Goal 
   5.141 +    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
   5.142 +by (lemma_tac p1 1);
   5.143 +by (Safe_tac 1);
   5.144 +by (REPEAT (rtac cut 1 
   5.145 +	    THEN
   5.146 +	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.147 +	    THEN
   5.148 +	    Safe_tac 1));
   5.149 +qed "imp_cong";
   5.150 +
   5.151 +val [p1,p2] = Goal 
   5.152 +    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
   5.153 +by (lemma_tac p1 1);
   5.154 +by (Safe_tac 1);
   5.155 +by (REPEAT (rtac cut 1 
   5.156 +	    THEN
   5.157 +	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.158 +	    THEN
   5.159 +	    Safe_tac 1));
   5.160 +qed "conj_cong";
   5.161 +
   5.162 +
   5.163 +open Simplifier;
   5.164 +
   5.165 +(*** Standard simpsets ***)
   5.166 +
   5.167 +(*Add congruence rules for = or <-> (instead of ==) *)
   5.168 +infix 4 addcongs delcongs;
   5.169 +fun ss addcongs congs =
   5.170 +        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
   5.171 +fun ss delcongs congs =
   5.172 +        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
   5.173 +
   5.174 +fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
   5.175 +fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
   5.176 +
   5.177 +val triv_rls = [FalseL, TrueR, basic, refl, iff_refl];
   5.178 +
   5.179 +fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   5.180 +				 assume_tac];
   5.181 +(*No premature instantiation of variables during simplification*)
   5.182 +fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
   5.183 +				 eq_assume_tac];
   5.184 +
   5.185 +(*No simprules, but basic infrastructure for simplification*)
   5.186 +val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
   5.187 +			   setSSolver   safe_solver
   5.188 +			   setSolver    unsafe_solver
   5.189 +			   setmksimps   (map mk_meta_eq o atomize o gen_all);
   5.190 +
   5.191 +val LK_simps =
   5.192 +   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
   5.193 +    imp_simps @ iff_simps @
   5.194 +    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
   5.195 +    map prove_fun
   5.196 +     ["|- P | ~P",             "|- ~P | P",
   5.197 +      "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
   5.198 +      "|- (~P <-> ~Q) <-> (P<->Q)"];
   5.199 +
   5.200 +val LK_ss = LK_basic_ss addsimps LK_simps addcongs [imp_cong];
   5.201 +
   5.202 +simpset_ref() := LK_ss;
   5.203 +
   5.204 +
   5.205 +(* Subst rule *)
   5.206 +
   5.207 +qed_goal "subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   5.208 +  (fn prems =>
   5.209 +   [cut_facts_tac prems 1,
   5.210 +    asm_simp_tac LK_basic_ss 1]);
   5.211 +
   5.212 +