Instantiated the one-point-rule quantifier simpprocs for FOL
authorpaulson
Wed Dec 03 10:48:16 1997 +0100 (1997-12-03 ago)
changeset 434950403e5a44c0
parent 4348 c7f6b4256964
child 4350 1983e4054fd8
Instantiated the one-point-rule quantifier simpprocs for FOL

New file fologic.ML holds abstract syntax operations

Also, miniscoping provided for intuitionistic logic
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/FOL/fologic.ML
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/IsaMakefile	Wed Dec 03 10:47:13 1997 +0100
     1.2 +++ b/src/FOL/IsaMakefile	Wed Dec 03 10:48:16 1997 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  	simplifier.ML splitter.ML ind.ML 
     1.5  
     1.6  FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
     1.7 -	cladata.ML $(PROVERS:%=../Provers/%)
     1.8 +	fologic.ML cladata.ML $(PROVERS:%=../Provers/%)
     1.9  
    1.10  EX_NAMES = If List Nat Nat2 Prolog IffOracle
    1.11  EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
     2.1 --- a/src/FOL/ROOT.ML	Wed Dec 03 10:47:13 1997 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Wed Dec 03 10:48:16 1997 +0100
     2.3 @@ -19,8 +19,10 @@
     2.4  use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
     2.5  use "$ISABELLE_HOME/src/Provers/classical.ML";
     2.6  use "$ISABELLE_HOME/src/Provers/blast.ML";
     2.7 +use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
     2.8  
     2.9  use_thy "IFOL";
    2.10 +use "fologic.ML";
    2.11  
    2.12  (** Applying HypsubstFun to generate hyp_subst_tac **)
    2.13  structure Hypsubst_Data =
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/FOL/fologic.ML	Wed Dec 03 10:48:16 1997 +0100
     3.3 @@ -0,0 +1,52 @@
     3.4 +(*  Title:      FOL/fologic.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson
     3.7 +
     3.8 +Abstract syntax operations for FOL.
     3.9 +*)
    3.10 +
    3.11 +signature FOLOGIC =
    3.12 +sig
    3.13 +  val oT: typ
    3.14 +  val mk_Trueprop: term -> term
    3.15 +  val dest_Trueprop: term -> term
    3.16 +  val conj: term
    3.17 +  val disj: term
    3.18 +  val imp: term
    3.19 +  val eq_const: typ -> term
    3.20 +  val all_const: typ -> term
    3.21 +  val exists_const: typ -> term
    3.22 +  val mk_eq: term * term -> term
    3.23 +  val mk_all: term * term -> term
    3.24 +  val mk_exists: term * term -> term
    3.25 +end;
    3.26 +
    3.27 +
    3.28 +structure FOLogic: FOLOGIC =
    3.29 +struct
    3.30 +
    3.31 +val oT = Type("o",[]);
    3.32 +
    3.33 +val Trueprop = Const("Trueprop", oT-->propT);
    3.34 +
    3.35 +fun mk_Trueprop P = Trueprop $ P;
    3.36 +
    3.37 +fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    3.38 +  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    3.39 +
    3.40 +(** Logical constants **)
    3.41 +
    3.42 +val conj = Const("op &", [oT,oT]--->oT)
    3.43 +and disj = Const("op |", [oT,oT]--->oT)
    3.44 +and imp = Const("op -->", [oT,oT]--->oT);
    3.45 +
    3.46 +fun eq_const T = Const ("op =", [T, T] ---> oT);
    3.47 +fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    3.48 +
    3.49 +fun all_const T = Const ("All", [T --> oT] ---> oT);
    3.50 +fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    3.51 +
    3.52 +fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
    3.53 +fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    3.54 +
    3.55 +end;
     4.1 --- a/src/FOL/simpdata.ML	Wed Dec 03 10:47:13 1997 +0100
     4.2 +++ b/src/FOL/simpdata.ML	Wed Dec 03 10:48:16 1997 +0100
     4.3 @@ -41,8 +41,14 @@
     4.4    "(P <-> P) <-> True",
     4.5    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
     4.6  
     4.7 +(*The x=t versions are needed for the simplification procedures*)
     4.8  val quant_simps = map int_prove_fun
     4.9 - ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    4.10 + ["(ALL x. P) <-> P",   
    4.11 +  "(ALL x. x=t --> P(x)) <-> P(t)",
    4.12 +  "(ALL x. t=x --> P(x)) <-> P(t)",
    4.13 +  "(EX x. P) <-> P",
    4.14 +  "(EX x. x=t & P(x)) <-> P(t)", 
    4.15 +  "(EX x. t=x & P(x)) <-> P(t)"];
    4.16  
    4.17  (*These are NOT supplied by default!*)
    4.18  val distrib_simps  = map int_prove_fun
    4.19 @@ -96,30 +102,43 @@
    4.20    cases boil down to the same thing.*) 
    4.21  val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
    4.22  
    4.23 -(*At present, miniscoping is for classical logic only.  We do NOT include
    4.24 -  distribution of ALL over &, or dually that of EX over |.*)
    4.25 +
    4.26 +(*** Miniscoping: pushing quantifiers in
    4.27 +     We do NOT distribute of ALL over &, or dually that of EX over |
    4.28 +     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
    4.29 +     show that this step can increase proof length!
    4.30 +***)
    4.31 +
    4.32 +(*existential miniscoping*)
    4.33 +val int_ex_simps = map int_prove_fun 
    4.34 +		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    4.35 +		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    4.36 +		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    4.37 +		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    4.38 +
    4.39 +(*classical rules*)
    4.40 +val cla_ex_simps = map prove_fun 
    4.41 +                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    4.42 +		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    4.43  
    4.44 -(*Miniscoping: pushing in existential quantifiers*)
    4.45 -val ex_simps = map prove_fun 
    4.46 -                ["(EX x. x=t & P(x)) <-> P(t)",
    4.47 -                 "(EX x. t=x & P(x)) <-> P(t)",
    4.48 -                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    4.49 -                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    4.50 -                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    4.51 -                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    4.52 -                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    4.53 -                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    4.54 +val ex_simps = int_ex_simps @ cla_ex_simps;
    4.55 +
    4.56 +(*universal miniscoping*)
    4.57 +val int_all_simps = map int_prove_fun
    4.58 +		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    4.59 +		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    4.60 +		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    4.61 +		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    4.62  
    4.63 -(*Miniscoping: pushing in universal quantifiers*)
    4.64 -val all_simps = map prove_fun
    4.65 -                ["(ALL x. x=t --> P(x)) <-> P(t)",
    4.66 -                 "(ALL x. t=x --> P(x)) <-> P(t)",
    4.67 -                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    4.68 -                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    4.69 -                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    4.70 -                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
    4.71 -                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    4.72 -                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    4.73 +(*classical rules*)
    4.74 +val cla_all_simps = map prove_fun
    4.75 +                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    4.76 +		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    4.77 +
    4.78 +val all_simps = int_all_simps @ cla_all_simps;
    4.79 +
    4.80 +
    4.81 +(*** Named rewrite rules proved for IFOL ***)
    4.82  
    4.83  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
    4.84      (fn prems => [ (cut_facts_tac prems 1), 
    4.85 @@ -168,7 +187,50 @@
    4.86  val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
    4.87    (fn [prem] => [rewtac prem, rtac refl 1]);
    4.88  
    4.89 -(*** case splitting ***)
    4.90 +
    4.91 +open Simplifier;
    4.92 +
    4.93 +(** make simplification procedures for quantifier elimination **)
    4.94 +structure Quantifier1 = Quantifier1Fun(
    4.95 +struct
    4.96 +  (*abstract syntax*)
    4.97 +  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    4.98 +    | dest_eq _ = None;
    4.99 +  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
   4.100 +    | dest_conj _ = None;
   4.101 +  val conj = FOLogic.conj
   4.102 +  val imp  = FOLogic.imp
   4.103 +  (*rules*)
   4.104 +  val iff_reflection = iff_reflection
   4.105 +  val iffI = iffI
   4.106 +  val sym  = sym
   4.107 +  val conjI= conjI
   4.108 +  val conjE= conjE
   4.109 +  val impI = impI
   4.110 +  val impE = impE
   4.111 +  val mp   = mp
   4.112 +  val exI  = exI
   4.113 +  val exE  = exE
   4.114 +  val allI = allI
   4.115 +  val allE = allE
   4.116 +end);
   4.117 +
   4.118 +local
   4.119 +val ex_pattern =
   4.120 +  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
   4.121 +
   4.122 +val all_pattern =
   4.123 +  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
   4.124 +
   4.125 +in
   4.126 +val defEX_regroup =
   4.127 +  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
   4.128 +val defALL_regroup =
   4.129 +  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
   4.130 +end;
   4.131 +
   4.132 +
   4.133 +(*** Case splitting ***)
   4.134  
   4.135  qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
   4.136          (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   4.137 @@ -192,7 +254,7 @@
   4.138  
   4.139  structure Induction = InductionFun(struct val spec=IFOL.spec end);
   4.140  
   4.141 -open Simplifier Induction;
   4.142 +open Induction;
   4.143  
   4.144  (*Add congruence rules for = or <-> (instead of ==) *)
   4.145  infix 4 addcongs delcongs;
   4.146 @@ -222,12 +284,13 @@
   4.147  
   4.148  (*No simprules, but basic infastructure for simplification*)
   4.149  val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   4.150 +                            addsimprocs [defALL_regroup,defEX_regroup]
   4.151  			    setSSolver   safe_solver
   4.152  			    setSolver  unsafe_solver
   4.153  			    setmksimps (map mk_meta_eq o atomize o gen_all);
   4.154  
   4.155  (*intuitionistic simprules only*)
   4.156 -val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
   4.157 +val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
   4.158  			   addcongs [imp_cong];
   4.159  
   4.160  val cla_simps = 
   4.161 @@ -240,7 +303,7 @@
   4.162        "(~P <-> ~Q) <-> (P<->Q)"];
   4.163  
   4.164  (*classical simprules too*)
   4.165 -val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
   4.166 +val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
   4.167  
   4.168  simpset_ref() := FOL_ss;
   4.169