diff --git a/src/FOLP/IFOLP.thy b/src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy +++ b/src/FOLP/IFOLP.thy @@ -1,716 +1,715 @@ (* Title: FOLP/IFOLP.thy Author: Martin D Coen, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) section \Intuitionistic First-Order Logic with Proofs\ theory IFOLP imports Pure begin ML_file \~~/src/Tools/misc_legacy.ML\ setup Pure_Thy.old_appl_syntax_setup setup \Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\ class "term" default_sort "term" typedecl p typedecl o consts (*** Judgements ***) Proof :: "[o,p]=>prop" EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) (*** Logical Connectives -- Type Formers ***) eq :: "['a,'a] => o" (infixl "=" 50) True :: "o" False :: "o" conj :: "[o,o] => o" (infixr "&" 35) disj :: "[o,o] => o" (infixr "|" 30) imp :: "[o,o] => o" (infixr "-->" 25) (*Quantifiers*) All :: "('a => o) => o" (binder "ALL " 10) Ex :: "('a => o) => o" (binder "EX " 10) (*Rewriting gadgets*) NORM :: "o => o" norm :: "'a => 'a" (*** Proof Term Formers: precedence must exceed 50 ***) tt :: "p" contr :: "p=>p" fst :: "p=>p" snd :: "p=>p" pair :: "[p,p]=>p" ("(1<_,/_>)") split :: "[p, [p,p]=>p] =>p" inl :: "p=>p" inr :: "p=>p" "when" :: "[p, p=>p, p=>p]=>p" lambda :: "(p => p) => p" (binder "lam " 55) App :: "[p,p]=>p" (infixl "`" 60) alll :: "['a=>p]=>p" (binder "all " 55) app :: "[p,'a]=>p" (infixl "^" 55) exists :: "['a,p]=>p" ("(1[_,/_])") xsplit :: "[p,['a,p]=>p]=>p" ideq :: "'a=>p" idpeel :: "[p,'a=>p]=>p" nrm :: p NRM :: p syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5) parse_translation \ - let fun proof_tr [p, P] = Const (\<^const_syntax>\Proof\, dummyT) $ P $ p + let fun proof_tr [p, P] = Syntax.const \<^const_syntax>\Proof\ $ P $ p in [(\<^syntax_const>\_Proof\, K proof_tr)] end \ (*show_proofs = true displays the proof terms -- they are ENORMOUS*) ML \val show_proofs = Attrib.setup_config_bool \<^binding>\show_proofs\ (K false)\ print_translation \ let fun proof_tr' ctxt [P, p] = - if Config.get ctxt show_proofs then Const (\<^syntax_const>\_Proof\, dummyT) $ p $ P + if Config.get ctxt show_proofs then Syntax.const \<^syntax_const>\_Proof\ $ p $ P else P in [(\<^const_syntax>\Proof\, proof_tr')] end \ (**** Propositional logic ****) (*Equality*) (* Like Intensional Equality in MLTT - but proofs distinct from terms *) axiomatization where ieqI: "ideq(a) : a=a" and ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)" (* Truth and Falsity *) axiomatization where TrueI: "tt : True" and FalseE: "a:False ==> contr(a):P" (* Conjunction *) axiomatization where conjI: "[| a:P; b:Q |] ==> : P&Q" and conjunct1: "p:P&Q ==> fst(p):P" and conjunct2: "p:P&Q ==> snd(p):Q" (* Disjunction *) axiomatization where disjI1: "a:P ==> inl(a):P|Q" and disjI2: "b:Q ==> inr(b):P|Q" and disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R |] ==> when(a,f,g):R" (* Implication *) axiomatization where impI: "\P Q f. (!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" and mp: "\P Q f. [| f:P-->Q; a:P |] ==> f`a:Q" (*Quantifiers*) axiomatization where allI: "\P. (!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" and spec: "\P f. (f:ALL x. P(x)) ==> f^x : P(x)" axiomatization where exI: "p : P(x) ==> [x,p] : EX x. P(x)" and exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R" (**** Equality between proofs ****) axiomatization where prefl: "a : P ==> a = a : P" and psym: "a = b : P ==> b = a : P" and ptrans: "[| a = b : P; b = c : P |] ==> a = c : P" axiomatization where idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" axiomatization where fstB: "a:P ==> fst() = a : P" and sndB: "b:Q ==> snd() = b : Q" and pairEC: "p:P&Q ==> p = : P&Q" axiomatization where whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" and whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" and plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q" axiomatization where applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" and funEC: "f:P ==> f = lam x. f`x : P" axiomatization where specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" (**** Definitions ****) definition Not :: "o => o" ("~ _" [40] 40) where not_def: "~P == P-->False" definition iff :: "[o,o] => o" (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)" (*Unique existence*) definition Ex1 :: "('a => o) => o" (binder "EX! " 10) where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" (*Rewriting -- special constants to flag normalized terms and formulae*) axiomatization where norm_eq: "nrm : norm(x) = x" and NORM_iff: "NRM : NORM(P) <-> P" (*** Sequent-style elimination rules for & --> and ALL ***) schematic_goal conjE: assumes "p:P&Q" and "!!x y.[| x:P; y:Q |] ==> f(x,y):R" shows "?a:R" apply (rule assms(2)) apply (rule conjunct1 [OF assms(1)]) apply (rule conjunct2 [OF assms(1)]) done schematic_goal impE: assumes "p:P-->Q" and "q:P" and "!!x. x:Q ==> r(x):R" shows "?p:R" apply (rule assms mp)+ done schematic_goal allE: assumes "p:ALL x. P(x)" and "!!y. y:P(x) ==> q(y):R" shows "?p:R" apply (rule assms spec)+ done (*Duplicates the quantifier; for use with eresolve_tac*) schematic_goal all_dupE: assumes "p:ALL x. P(x)" and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R" shows "?p:R" apply (rule assms spec)+ done (*** Negation rules, which translate between ~P and P-->False ***) schematic_goal notI: assumes "!!x. x:P ==> q(x):False" shows "?p:~P" unfolding not_def apply (assumption | rule assms impI)+ done schematic_goal notE: "p:~P \ q:P \ ?p:R" unfolding not_def apply (drule (1) mp) apply (erule FalseE) done (*This is useful with the special implication rules for each kind of P. *) schematic_goal not_to_imp: assumes "p:~P" and "!!x. x:(P-->False) ==> q(x):Q" shows "?p:Q" apply (assumption | rule assms impI notE)+ done (* For substitution int an assumption P, reduce Q to P-->Q, substitute into this implication, then apply impI to move P back into the assumptions.*) schematic_goal rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q" apply (assumption | rule mp)+ done (*Contrapositive of an inference rule*) schematic_goal contrapos: assumes major: "p:~Q" and minor: "!!y. y:P==>q(y):Q" shows "?a:~P" apply (rule major [THEN notE, THEN notI]) apply (erule minor) done (** Unique assumption tactic. Ignores proof objects. Fails unless one assumption is equal and exactly one is unifiable **) ML \ local - fun discard_proof (Const (\<^const_name>\Proof\, _) $ P $ _) = P; + fun discard_proof \<^Const_>\Proof for P _\ = P; in fun uniq_assume_tac ctxt = SUBGOAL (fn (prem,i) => let val hyps = map discard_proof (Logic.strip_assums_hyp prem) and concl = discard_proof (Logic.strip_assums_concl prem) in if exists (fn hyp => hyp aconv concl) hyps then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of [_] => assume_tac ctxt i | _ => no_tac else no_tac end); end; \ (*** Modus Ponens Tactics ***) (*Finds P-->Q and P in the assumptions, replaces implication by Q *) ML \ fun mp_tac ctxt i = eresolve_tac ctxt [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac ctxt i \ method_setup mp = \Scan.succeed (SIMPLE_METHOD' o mp_tac)\ (*Like mp_tac but instantiates no variables*) ML \ fun int_uniq_mp_tac ctxt i = eresolve_tac ctxt [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac ctxt i \ (*** If-and-only-if ***) schematic_goal iffI: assumes "!!x. x:P ==> q(x):Q" and "!!x. x:Q ==> r(x):P" shows "?p:P<->Q" unfolding iff_def apply (assumption | rule assms conjI impI)+ done schematic_goal iffE: assumes "p:P <-> Q" and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" shows "?p:R" apply (rule conjE) apply (rule assms(1) [unfolded iff_def]) apply (rule assms(2)) apply assumption+ done (* Destruct rules for <-> similar to Modus Ponens *) schematic_goal iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q" unfolding iff_def apply (rule conjunct1 [THEN mp], assumption+) done schematic_goal iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P" unfolding iff_def apply (rule conjunct2 [THEN mp], assumption+) done schematic_goal iff_refl: "?p:P <-> P" apply (rule iffI) apply assumption+ done schematic_goal iff_sym: "p:Q <-> P ==> ?p:P <-> Q" apply (erule iffE) apply (rule iffI) apply (erule (1) mp)+ done schematic_goal iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R" apply (rule iffI) apply (assumption | erule iffE | erule (1) impE)+ done (*** Unique existence. NOTE THAT the following 2 quantifications EX!x such that [EX!y such that P(x,y)] (sequential) EX!x,y such that P(x,y) (simultaneous) do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. ***) schematic_goal ex1I: assumes "p:P(a)" and "!!x u. u:P(x) ==> f(u) : x=a" shows "?p:EX! x. P(x)" unfolding ex1_def apply (assumption | rule assms exI conjI allI impI)+ done schematic_goal ex1E: assumes "p:EX! x. P(x)" and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R" shows "?a : R" apply (insert assms(1) [unfolded ex1_def]) apply (erule exE conjE | assumption | rule assms(1))+ apply (erule assms(2), assumption) done (*** <-> congruence rules for simplification ***) (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) ML \ fun iff_tac ctxt prems i = resolve_tac ctxt (prems RL [@{thm iffE}]) i THEN REPEAT1 (eresolve_tac ctxt [asm_rl, @{thm mp}] i) \ method_setup iff = \Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\ schematic_goal conj_cong: assumes "p:P <-> P'" and "!!x. x:P' ==> q(x):Q <-> Q'" shows "?p:(P&Q) <-> (P'&Q')" apply (insert assms(1)) apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ done schematic_goal disj_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+ done schematic_goal imp_cong: assumes "p:P <-> P'" and "!!x. x:P' ==> q(x):Q <-> Q'" shows "?p:(P-->Q) <-> (P'-->Q')" apply (insert assms(1)) apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+ done schematic_goal iff_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" apply (erule iffE | assumption | rule iffI | mp)+ done schematic_goal not_cong: "p:P <-> P' ==> ?p:~P <-> ~P'" apply (assumption | rule iffI notI | mp | erule iffE notE)+ done schematic_goal all_cong: assumes "!!x. f(x):P(x) <-> Q(x)" shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))" apply (assumption | rule iffI allI | mp | erule allE | iff assms)+ done schematic_goal ex_cong: assumes "!!x. f(x):P(x) <-> Q(x)" shows "?p:(EX x. P(x)) <-> (EX x. Q(x))" apply (erule exE | assumption | rule iffI exI | mp | iff assms)+ done (*NOT PROVED ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ()) "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" (fn prems => [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ])) *) (*** Equality rules ***) lemmas refl = ieqI schematic_goal subst: assumes prem1: "p:a=b" and prem2: "q:P(a)" shows "?p : P(b)" apply (rule prem2 [THEN rev_mp]) apply (rule prem1 [THEN ieqE]) apply (rule impI) apply assumption done schematic_goal sym: "q:a=b ==> ?c:b=a" apply (erule subst) apply (rule refl) done schematic_goal trans: "[| p:a=b; q:b=c |] ==> ?d:a=c" apply (erule (1) subst) done (** ~ b=a ==> ~ a=b **) schematic_goal not_sym: "p:~ b=a ==> ?q:~ a=b" apply (erule contrapos) apply (erule sym) done schematic_goal ssubst: "p:b=a \ q:P(a) \ ?p:P(b)" apply (drule sym) apply (erule subst) apply assumption done (*A special case of ex1E that would otherwise need quantifier expansion*) schematic_goal ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b" apply (erule ex1E) apply (rule trans) apply (rule_tac [2] sym) apply (assumption | erule spec [THEN mp])+ done (** Polymorphic congruence rules **) schematic_goal subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)" apply (erule ssubst) apply (rule refl) done schematic_goal subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" apply (erule ssubst)+ apply (rule refl) done schematic_goal subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)" apply (erule ssubst)+ apply (rule refl) done (*Useful with eresolve_tac for proving equalties from known equalities. a = b | | c = d *) schematic_goal box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" apply (rule trans) apply (rule trans) apply (rule sym) apply assumption+ done (*Dual of box_equals: for proving equalities backwards*) schematic_goal simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" apply (rule trans) apply (rule trans) apply (assumption | rule sym)+ done (** Congruence rules for predicate letters **) schematic_goal pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')" apply (rule iffI) apply (tactic \ DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\) done schematic_goal pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" apply (rule iffI) apply (tactic \ DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\) done schematic_goal pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" apply (rule iffI) apply (tactic \ DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\) done lemmas pred_congs = pred1_cong pred2_cong pred3_cong (*special case for the equality predicate!*) lemmas eq_cong = pred2_cong [where P = "(=)"] (*** Simplifications of assumed implications. Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE used with mp_tac (restricted to atomic formulae) is COMPLETE for intuitionistic propositional logic. See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic (preprint, University of St Andrews, 1991) ***) schematic_goal conj_impE: assumes major: "p:(P&Q)-->S" and minor: "!!x. x:P-->(Q-->S) ==> q(x):R" shows "?p:R" apply (assumption | rule conjI impI major [THEN mp] minor)+ done schematic_goal disj_impE: assumes major: "p:(P|Q)-->S" and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R" shows "?p:R" apply (tactic \DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE resolve_tac \<^context> [@{thm disjI1}, @{thm disjI2}, @{thm impI}, @{thm major} RS @{thm mp}, @{thm minor}] 1)\) done (*Simplifies the implication. Classical version is stronger. Still UNSAFE since Q must be provable -- backtracking needed. *) schematic_goal imp_impE: assumes major: "p:(P-->Q)-->S" and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q" and r2: "!!x. x:S ==> r(x):R" shows "?p:R" apply (assumption | rule impI major [THEN mp] r1 r2)+ done (*Simplifies the implication. Classical version is stronger. Still UNSAFE since ~P must be provable -- backtracking needed. *) schematic_goal not_impE: assumes major: "p:~P --> S" and r1: "!!y. y:P ==> q(y):False" and r2: "!!y. y:S ==> r(y):R" shows "?p:R" apply (assumption | rule notI impI major [THEN mp] r1 r2)+ done (*Simplifies the implication. UNSAFE. *) schematic_goal iff_impE: assumes major: "p:(P<->Q)-->S" and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q" and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P" and r3: "!!x. x:S ==> s(x):R" shows "?p:R" apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ done (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) schematic_goal all_impE: assumes major: "p:(ALL x. P(x))-->S" and r1: "!!x. q:P(x)" and r2: "!!y. y:S ==> r(y):R" shows "?p:R" apply (assumption | rule allI impI major [THEN mp] r1 r2)+ done (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) schematic_goal ex_impE: assumes major: "p:(EX x. P(x))-->S" and r: "!!y. y:P(a)-->S ==> q(y):R" shows "?p:R" apply (assumption | rule exI impI major [THEN mp] r)+ done schematic_goal rev_cut_eq: assumes "p:a=b" and "!!x. x:a=b ==> f(x):R" shows "?p:R" apply (rule assms)+ done lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" . ML_file \hypsubst.ML\ ML \ structure Hypsubst = Hypsubst ( (*Take apart an equality judgement; otherwise raise Match!*) - fun dest_eq (Const (\<^const_name>\Proof\, _) $ - (Const (\<^const_name>\eq\, _) $ t $ u) $ _) = (t, u); + fun dest_eq \<^Const_>\Proof for \\<^Const_>\eq _ for t u\\ _\ = (t, u); val imp_intr = @{thm impI} (*etac rev_cut_eq moves an equality to be the last premise. *) val rev_cut_eq = @{thm rev_cut_eq} val rev_mp = @{thm rev_mp} val subst = @{thm subst} val sym = @{thm sym} val thin_refl = @{thm thin_refl} ); open Hypsubst; \ ML_file \intprover.ML\ (*** Rewrite rules ***) schematic_goal conj_rews: "?p1 : P & True <-> P" "?p2 : True & P <-> P" "?p3 : P & False <-> False" "?p4 : False & P <-> False" "?p5 : P & P <-> P" "?p6 : P & ~P <-> False" "?p7 : ~P & P <-> False" "?p8 : (P & Q) & R <-> P & (Q & R)" apply (tactic \fn st => IntPr.fast_tac \<^context> 1 st\)+ done schematic_goal disj_rews: "?p1 : P | True <-> True" "?p2 : True | P <-> True" "?p3 : P | False <-> P" "?p4 : False | P <-> P" "?p5 : P | P <-> P" "?p6 : (P | Q) | R <-> P | (Q | R)" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done schematic_goal not_rews: "?p1 : ~ False <-> True" "?p2 : ~ True <-> False" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done schematic_goal imp_rews: "?p1 : (P --> False) <-> ~P" "?p2 : (P --> True) <-> True" "?p3 : (False --> P) <-> True" "?p4 : (True --> P) <-> P" "?p5 : (P --> P) <-> True" "?p6 : (P --> ~P) <-> ~P" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done schematic_goal iff_rews: "?p1 : (True <-> P) <-> P" "?p2 : (P <-> True) <-> P" "?p3 : (P <-> P) <-> True" "?p4 : (False <-> P) <-> ~P" "?p5 : (P <-> False) <-> ~P" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done schematic_goal quant_rews: "?p1 : (ALL x. P) <-> P" "?p2 : (EX x. P) <-> P" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done (*These are NOT supplied by default!*) schematic_goal distrib_rews1: "?p1 : ~(P|Q) <-> ~P & ~Q" "?p2 : P & (Q | R) <-> P&Q | P&R" "?p3 : (Q | R) & P <-> Q&P | R&P" "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done schematic_goal distrib_rews2: "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))" "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)" "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))" "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))" apply (tactic \IntPr.fast_tac \<^context> 1\)+ done lemmas distrib_rews = distrib_rews1 distrib_rews2 schematic_goal P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)" apply (tactic \IntPr.fast_tac \<^context> 1\) done schematic_goal not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)" apply (tactic \IntPr.fast_tac \<^context> 1\) done end diff --git a/src/FOLP/hypsubst.ML b/src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML +++ b/src/FOLP/hypsubst.ML @@ -1,92 +1,92 @@ (* Title: FOLP/hypsubst.ML Author: Martin D Coen, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Original version of Provers/hypsubst. Cannot use new version because it relies on the new simplifier! Martin Coen's tactic for substitution in the hypotheses *) signature HYPSUBST_DATA = sig val dest_eq : term -> term*term val imp_intr : thm (* (P ==> Q) ==> P-->Q *) val rev_mp : thm (* [| P; P-->Q |] ==> Q *) val subst : thm (* [| a=b; P(a) |] ==> P(b) *) val sym : thm (* a=b ==> b=a *) end; signature HYPSUBST = sig val bound_hyp_subst_tac : Proof.context -> int -> tactic val hyp_subst_tac : Proof.context -> int -> tactic (*exported purely for debugging purposes*) val eq_var : bool -> term -> int * thm val inspect_pair : bool -> term * term -> thm end; functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = struct local open Data in exception EQ_VAR; (*It's not safe to substitute for a constant; consider 0=1. It's not safe to substitute for x=t[x] since x is not eliminated. It's not safe to substitute for a Var; what if it appears in other goals? It's not safe to substitute for a variable free in the premises, but how could we check for this?*) fun inspect_pair bnd (t, u) = (case (Envir.eta_contract t, Envir.eta_contract u) of (Bound i, _) => if loose_bvar1 (u, i) then raise Match else sym (*eliminates t*) | (_, Bound i) => if loose_bvar (t, i) then raise Match else asm_rl (*eliminates u*) | (Free _, _) => if bnd orelse Logic.occs (t, u) then raise Match else sym (*eliminates t*) | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match else asm_rl (*eliminates u*) | _ => raise Match); (*Locates a substitutable variable on the left (resp. right) of an equality assumption. Returns the number of intervening assumptions, paried with the rule asm_rl (resp. sym). *) fun eq_var bnd = - let fun eq_var_aux k (Const(\<^const_name>\Pure.all\,_) $ Abs(_,_,t)) = eq_var_aux k t - | eq_var_aux k (Const(\<^const_name>\Pure.imp\,_) $ A $ B) = + let fun eq_var_aux k \<^Const_>\Pure.all _ for \Abs(_,_,t)\\ = eq_var_aux k t + | eq_var_aux k \<^Const_>\Pure.imp for A B\ = ((k, inspect_pair bnd (dest_eq A)) (*Exception Match comes from inspect_pair or dest_eq*) handle Match => eq_var_aux (k+1) B) | eq_var_aux k _ = raise EQ_VAR in eq_var_aux 0 end; (*Select a suitable equality assumption and substitute throughout the subgoal Replaces only Bound variables if bnd is true*) fun gen_hyp_subst_tac bnd ctxt = SUBGOAL(fn (Bi,i) => let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,symopt) = eq_var bnd Bi in DETERM (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [rev_mp] i), eresolve_tac ctxt [revcut_rl] i, REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [rev_mp] i), eresolve_tac ctxt [symopt RS subst] i, REPEAT_DETERM_N n (resolve_tac ctxt [imp_intr] i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables*) val hyp_subst_tac = gen_hyp_subst_tac false; (*Substitutes for Bound variables only -- this is always safe*) val bound_hyp_subst_tac = gen_hyp_subst_tac true; end end; diff --git a/src/FOLP/simp.ML b/src/FOLP/simp.ML --- a/src/FOLP/simp.ML +++ b/src/FOLP/simp.ML @@ -1,593 +1,593 @@ (* Title: FOLP/simp.ML Author: Tobias Nipkow Copyright 1993 University of Cambridge FOLP version of... Generic simplifier, suitable for most logics. (from Provers) This version allows instantiation of Vars in the subgoal, since the proof term must change. *) signature SIMP_DATA = sig val case_splits : (thm * string) list val dest_red : term -> term * term * term val mk_rew_rules : thm -> thm list val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) val refl_thms : thm list val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) val trans_thms : thm list end; infix 4 addcongs delrews delcongs setauto; signature SIMP = sig type simpset val empty_ss : simpset val addcongs : simpset * thm list -> simpset val addrew : Proof.context -> thm -> simpset -> simpset val delcongs : simpset * thm list -> simpset val delrews : simpset * thm list -> simpset val dest_ss : simpset -> thm list * thm list val print_ss : Proof.context -> simpset -> unit val setauto : simpset * (Proof.context -> int -> tactic) -> simpset val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic val ASM_SIMP_TAC : Proof.context -> simpset -> int -> tactic val CASE_TAC : Proof.context -> simpset -> int -> tactic val SIMP_CASE2_TAC : Proof.context -> simpset -> int -> tactic val SIMP_THM : Proof.context -> simpset -> thm -> thm val SIMP_TAC : Proof.context -> simpset -> int -> tactic val SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic val mk_congs : Proof.context -> string list -> thm list val mk_typed_congs : Proof.context -> (string * string) list -> thm list (* temporarily disabled: val extract_free_congs : unit -> thm list *) val tracing : bool Unsynchronized.ref end; functor SimpFun (Simp_data: SIMP_DATA) : SIMP = struct local open Simp_data in (*For taking apart reductions into left, right hand sides*) val lhs_of = #2 o dest_red; val rhs_of = #3 o dest_red; (*** Indexing and filtering of theorems ***) fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); (*insert a thm in a discrimination net by its lhs*) fun lhs_insert_thm th net = Net.insert_term eq_brl (lhs_of (Thm.concl_of th), (false,th)) net handle Net.INSERT => net; (*match subgoal i against possible theorems in the net. Similar to match_from_nat_tac, but the net does not contain numbers; rewrite rules are not ordered.*) fun net_tac ctxt net = SUBGOAL(fn (prem, i) => resolve_tac ctxt (Net.unify_term net (Logic.strip_assums_concl prem)) i); (*match subgoal i against possible theorems indexed by lhs in the net*) fun lhs_net_tac ctxt net = SUBGOAL(fn (prem,i) => biresolve_tac ctxt (Net.unify_term net (lhs_of (Logic.strip_assums_concl prem))) i); fun nth_subgoal i thm = nth (Thm.prems_of thm) (i - 1); fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); fun lhs_of_eq i thm = lhs_of(goal_concl i thm) and rhs_of_eq i thm = rhs_of(goal_concl i thm); fun var_lhs(thm,i) = let fun var(Var _) = true | var(Abs(_,_,t)) = var t | var(f$_) = var f | var _ = false; in var(lhs_of_eq i thm) end; fun contains_op opns = let fun contains(Const(s,_)) = member (op =) opns s | contains(s$t) = contains s orelse contains t | contains(Abs(_,_,t)) = contains t | contains _ = false; in contains end; fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; val (normI_thms,normE_thms) = split_list norm_thms; (*Get the norm constants from norm_thms*) val norms = let fun norm thm = case lhs_of (Thm.concl_of thm) of Const(n,_)$_ => n | _ => error "No constant in lhs of a norm_thm" in map norm normE_thms end; fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of Const(s,_)$_ => member (op =) norms s | _ => false; fun refl_tac ctxt = resolve_tac ctxt refl_thms; fun find_res thms thm = let fun find [] = error "Check Simp_Data" | find(th::thms) = thm RS th handle THM _ => find thms in find thms end; val mk_trans = find_res trans_thms; fun mk_trans2 thm = let fun mk[] = error"Check transitivity" | mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts in mk trans_thms end; (*Applies tactic and returns the first resulting state, FAILS if none!*) fun one_result(tac,thm) = case Seq.pull(tac thm) of SOME(thm',_) => thm' | NONE => raise THM("Simplifier: could not continue", 0, [thm]); fun res1 ctxt (thm,thms,i) = one_result (resolve_tac ctxt thms i,thm); (**** Adding "NORM" tags ****) (*get name of the constant from conclusion of a congruence rule*) fun cong_const cong = case head_of (lhs_of (Thm.concl_of cong)) of Const(c,_) => c | _ => "" (*a placeholder distinct from const names*); (*true if the term is an atomic proposition (no ==> signs) *) val atomic = null o Logic.strip_assums_hyp; (*ccs contains the names of the constants possessing congruence rules*) fun add_hidden_vars ccs = let fun add_hvars tm hvars = case tm of Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars) | _$_ => let val (f,args) = strip_comb tm in case f of - Const(c,T) => + Const(c,_) => if member (op =) ccs c then fold_rev add_hvars args hvars else Misc_Legacy.add_term_vars (tm, hvars) | _ => Misc_Legacy.add_term_vars (tm, hvars) end | _ => hvars; in add_hvars end; fun add_new_asm_vars new_asms = let fun itf (tm, at) vars = if at then vars else Misc_Legacy.add_term_vars(tm,vars) fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm in if length(tml)=length(al) then fold_rev itf (tml ~~ al) vars else vars end fun add_vars (tm,vars) = case tm of Abs (_,_,body) => add_vars(body,vars) | r$s => (case head_of tm of - Const(c,T) => (case AList.lookup (op =) new_asms c of + Const(c,_) => (case AList.lookup (op =) new_asms c of NONE => add_vars(r,add_vars(s,vars)) | SOME(al) => add_list(tm,al,vars)) | _ => add_vars(r,add_vars(s,vars))) | _ => vars in add_vars end; fun add_norms ctxt (congs,ccs,new_asms) thm = let val thm' = mk_trans2 thm; (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) val nops = Thm.nprems_of thm' val lhs = rhs_of_eq 1 thm' val rhs = lhs_of_eq nops thm' val asms = tl(rev(tl(Thm.prems_of thm'))) val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] val hvars = add_new_asm_vars new_asms (rhs,hvars) fun it_asms asm hvars = if atomic asm then add_new_asm_vars new_asms (asm,hvars) else Misc_Legacy.add_term_frees(asm,hvars) val hvars = fold_rev it_asms asms hvars val hvs = map (#1 o dest_Var) hvars fun norm_step_tac st = st |> (case head_of(rhs_of_eq 1 st) of Var(ixn,_) => if member (op =) hvs ixn then refl_tac ctxt 1 else resolve_tac ctxt normI_thms 1 ORELSE refl_tac ctxt 1 | Const _ => resolve_tac ctxt normI_thms 1 ORELSE resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1 | Free _ => resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1 | _ => refl_tac ctxt 1) val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac val SOME(thm'',_) = Seq.pull(add_norm_tac thm') in thm'' end; fun add_norm_tags ctxt congs = let val ccs = map cong_const congs val new_asms = filter (exists not o #2) (ccs ~~ (map (map atomic o Thm.prems_of) congs)); in add_norms ctxt (congs,ccs,new_asms) end; fun normed_rews ctxt congs = let val add_norms = add_norm_tags ctxt congs fun normed thm = let val ctxt' = Variable.declare_thm thm ctxt; in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end in normed end; fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac ctxt]; val trans_norms = map mk_trans normE_thms; (* SIMPSET *) datatype simpset = SS of {auto_tac: Proof.context -> int -> tactic, congs: thm list, cong_net: thm Net.net, mk_simps: Proof.context -> thm -> thm list, simps: (thm * thm list) list, simp_net: thm Net.net} val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty, mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty}; (** Insertion of congruences and rewrites **) (*insert a thm in a thm net*) fun insert_thm th net = Net.insert_term Thm.eq_thm_prop (Thm.concl_of th, th) net handle Net.INSERT => net; val insert_thms = fold_rev insert_thm; fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let val thms = map Thm.trim_context (mk_simps ctxt thm) in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} end; fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = map Thm.trim_context thms @ congs; in SS{auto_tac=auto_tac, congs= congs', cong_net= insert_thms (map mk_trans thms) cong_net, mk_simps = fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net} end; (** Deletion of congruences and rewrites **) (*delete a thm from a thm net*) fun delete_thm th net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net handle Net.DELETE => net; val delete_thms = fold_rev delete_thm; fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = fold (remove Thm.eq_thm_prop) thms congs in SS{auto_tac=auto_tac, congs= congs', cong_net= delete_thms (map mk_trans thms) cong_net, mk_simps= fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net} end; fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let fun find((p as (th,ths))::ps',ps) = if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) | find([],simps') = ([], simps') val (thms,simps') = find(simps,[]) in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = simps', simp_net = delete_thms thms simp_net } end; fun ss delrews thms = fold delrew thms ss; fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps=simps, simp_net=simp_net}; (** Inspection of a simpset **) fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); fun print_ss ctxt (SS{congs,simps,...}) = writeln (cat_lines (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @ ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps)); (* Rewriting with conditionals *) val (case_thms,case_consts) = split_list case_splits; val case_rews = map mk_trans case_thms; fun if_rewritable ifc i thm = let val tm = goal_concl i thm fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) | nobound(Bound n,j,k) = n < k orelse k+j <= n | nobound(_) = true; fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1) | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in case f of Const(c,_) => if c=ifc then check_args(al,j) else find_if(s,j) orelse find_if(t,j) | _ => find_if(s,j) orelse find_if(t,j) end | find_if(_) = false; in find_if(tm,0) end; fun IF1_TAC ctxt cong_tac i = let fun seq_try (ifth::ifths,ifc::ifcs) thm = (COND (if_rewritable ifc i) (DETERM(resolve_tac ctxt [ifth] i)) (seq_try(ifths,ifcs))) thm | seq_try([],_) thm = no_tac thm and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm and one_subt thm = let val test = has_fewer_prems (Thm.nprems_of thm + 1) fun loop thm = COND test no_tac ((try_rew THEN DEPTH_FIRST test (refl_tac ctxt i)) ORELSE (refl_tac ctxt i THEN loop)) thm in (cong_tac THEN loop) thm end in COND (may_match(case_consts,i)) try_rew no_tac end; fun CASE_TAC ctxt (SS{cong_net,...}) i = let val cong_tac = net_tac ctxt cong_net i in NORM ctxt (IF1_TAC ctxt cong_tac) i end; (* Rewriting Automaton *) datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE | PROVE | POP_CS | POP_ARTR | IF; fun simp_refl([],_,ss) = ss | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); (** Tracing **) val tracing = Unsynchronized.ref false; (*Replace parameters by Free variables in P*) fun variants_abs ([],P) = P | variants_abs ((a,T)::aTs, P) = variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P))); (*Select subgoal i from proof state; substitute parameters, for printing*) fun prepare_goal i st = let val subgi = nth_subgoal i st val params = rev (Logic.strip_params subgi) in variants_abs (params, Logic.strip_assums_concl subgi) end; (*print lhs of conclusion of subgoal i*) fun pr_goal_lhs ctxt i st = writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st))); (*print conclusion of subgoal i*) fun pr_goal_concl ctxt i st = writeln (Syntax.string_of_term ctxt (prepare_goal i st)) (*print subgoals i to j (inclusive)*) fun pr_goals ctxt (i,j) st = if i>j then () else (pr_goal_concl ctxt i st; pr_goals ctxt (i+1,j) st); (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, thm=old state, thm'=new state *) fun pr_rew ctxt (i,n,thm,thm',not_asms) = if !tracing then (if not_asms then () else writeln"Assumption used in"; pr_goal_lhs ctxt i thm; writeln"->"; pr_goal_lhs ctxt (i+n) thm'; if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n-1) thm') else (); writeln"" ) else (); (* Skip the first n hyps of a goal, and return the rest in generalized form *) -fun strip_varify(Const(\<^const_name>\Pure.imp\, _) $ H $ B, n, vs) = +fun strip_varify(\<^Const_>\Pure.imp for H B\, n, vs) = if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) else strip_varify(B,n-1,vs) - | strip_varify(Const(\<^const_name>\Pure.all\,_)$Abs(_,T,t), n, vs) = + | strip_varify(\<^Const_>\Pure.all _ for \Abs(_,T,t)\\, n, vs) = strip_varify(t,n,Var(("?",length vs),T)::vs) | strip_varify _ = []; fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) = let fun simp_lhs(thm,ss,anet,ats,cs) = if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else if lhs_is_NORM(thm,i) then (ss, res1 ctxt (thm,trans_norms,i), anet,ats,cs) else case Seq.pull(cong_tac i thm) of SOME(thm',_) => let val ps = Thm.prems_of thm and ps' = Thm.prems_of thm'; val n = length(ps')-length(ps); val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps')); in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end | NONE => (REW::ss,thm,anet,ats,cs); (*NB: the "Adding rewrites:" trace will look strange because assumptions are represented by rules, generalized over their parameters*) fun add_asms(ss,thm,a,anet,ats,cs) = let val As = strip_varify(nth_subgoal i thm, a, []); val thms = map (Thm.trivial o Thm.cterm_of ctxt) As; val new_rws = maps mk_rew_rules thms; val rwrls = map mk_trans (maps mk_rew_rules thms); val anet' = fold_rev lhs_insert_thm rwrls anet; in (ss,thm,anet',anet::ats,cs) end; fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of SOME(thm',seq') => let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm) in pr_rew ctxt (i,n,thm,thm',more); if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) end | NONE => if more then rew((lhs_net_tac ctxt anet i THEN assume_tac ctxt i) thm, thm,ss,anet,ats,cs,false) else (ss,thm,anet,ats,cs); fun try_true(thm,ss,anet,ats,cs) = case Seq.pull(auto_tac ctxt i thm) of SOME(thm',_) => (ss,thm',anet,ats,cs) | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs in if !tracing then (writeln"*** Failed to prove precondition. Normal form:"; pr_goal_concl ctxt i thm; writeln"") else (); rew(seq,thm0,ss0,anet0,ats0,cs0,more) end; fun if_exp(thm,ss,anet,ats,cs) = case Seq.pull (IF1_TAC ctxt (cong_tac i) i thm) of SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) | NONE => (ss,thm,anet,ats,cs); fun step(s::ss, thm, anet, ats, cs) = case s of MK_EQ => (ss, res1 ctxt (thm,[red2],i), anet, ats, cs) | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) | REW => rew(net_tac ctxt net i thm,thm,ss,anet,ats,cs,true) | REFL => (ss, res1 ctxt (thm,refl_thms,i), anet, ats, cs) | TRUE => try_true(res1 ctxt (thm,refl_thms,i),ss,anet,ats,cs) | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) | POP_ARTR => (ss,thm,hd ats,tl ats,cs) | POP_CS => (ss,thm,anet,ats,tl cs) | IF => if_exp(thm,ss,anet,ats,cs); fun exec(state as (s::ss, thm, _, _, _)) = if s=STOP then thm else exec(step(state)); in exec(ss, thm, Net.empty, [], []) end; fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = let val cong_tac = net_tac ctxt cong_net in fn i => (fn thm => if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm))) THEN TRY(auto_tac ctxt i) end; fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false); fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = let val cong_tac = net_tac ctxt cong_net in fn thm => let val state = thm RSN (2,red1) in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end end; fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); (* Compute Congruence rules for individual constants using the substition rules *) val subst_thms = map Drule.export_without_context subst_thms; fun exp_app(0,t) = t | exp_app(i,t) = exp_app(i-1,t $ Bound (i-1)); -fun exp_abs(Type("fun",[T1,T2]),t,i) = +fun exp_abs(\<^Type>\fun T1 T2\,t,i) = Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) | exp_abs(T,t,i) = exp_app(i,t); fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = let fun xn_list(x,n) = let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1); in ListPair.map eta_Var (ixs, take (n+1) Ts) end val lhs = list_comb(f,xn_list("X",k-1)) val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; fun find_subst ctxt T = let fun find (thm::thms) = let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm)); val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, [])); val eqT::_ = binder_types cT in if Sign.typ_instance (Proof_Context.theory_of ctxt) (T,eqT) then SOME(thm,va,vb,P) else find thms end | find [] = NONE in find subst_thms end; fun mk_cong ctxt (f,aTs,rT) (refl,eq) = let val k = length aTs; fun ri((subst,va as Var(a,Ta),vb as Var(b,Tb), Var (P, _)),i,si,T,yik) = let val cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T)) val cb = Thm.cterm_of ctxt vb val cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T)) val cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs)) in infer_instantiate ctxt [(a,cx),(b,cy),(P,cp)] subst end; fun mk(c,T::Ts,i,yik) = let val si = radixstring(26,"a",i) in case find_subst ctxt T of NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end end | mk(c,[],_,_) = c; in mk(refl,rev aTs,k-1,[]) end; fun mk_cong_type ctxt (f,T) = let val (aTs,rT) = strip_type T; fun find_refl(r::rs) = let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r) in if Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, hd(binder_types eqT)) then SOME(r,(eq,body_type eqT)) else find_refl rs end | find_refl([]) = NONE; in case find_refl refl_thms of NONE => [] | SOME(refl) => [mk_cong ctxt (f,aTs,rT) refl] end; fun mk_congs' ctxt f = let val T = case Sign.const_type (Proof_Context.theory_of ctxt) f of NONE => error(f^" not declared") | SOME(T) => T; val T' = Logic.incr_tvar 9 T; in mk_cong_type ctxt (Const(f,T'),T') end; val mk_congs = maps o mk_congs'; fun mk_typed_congs ctxt = let fun readfT(f,s) = let val T = Logic.incr_tvar 9 (Syntax.read_typ ctxt s); val t = case Sign.const_type (Proof_Context.theory_of ctxt) f of SOME(_) => Const(f,T) | NONE => Free(f,T) in (t,T) end in maps (mk_cong_type ctxt o readfT) end; end; end; diff --git a/src/FOLP/simpdata.ML b/src/FOLP/simpdata.ML --- a/src/FOLP/simpdata.ML +++ b/src/FOLP/simpdata.ML @@ -1,86 +1,86 @@ (* Title: FOLP/simpdata.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Simplification data for FOLP. *) fun make_iff_T th = th RS @{thm P_Imp_P_iff_T}; val refl_iff_T = make_iff_T @{thm refl}; val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}), (@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})]; (* Conversion into rewrite rules *) fun mk_eq th = case Thm.concl_of th of - _ $ (Const (\<^const_name>\iff\, _) $ _ $ _) $ _ => th - | _ $ (Const (\<^const_name>\eq\, _) $ _ $ _) $ _ => th - | _ $ (Const (\<^const_name>\Not\, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F} + _ $ \<^Const_>\iff for _ _\ $ _ => th + | _ $ \<^Const_>\eq _ for _ _\ $ _ => th + | _ $ \<^Const_>\Not for _\ $ _ => th RS @{thm not_P_imp_P_iff_F} | _ => make_iff_T th; val mksimps_pairs = [(\<^const_name>\imp\, [@{thm mp}]), (\<^const_name>\conj\, [@{thm conjunct1}, @{thm conjunct2}]), (\<^const_name>\All\, [@{thm spec}]), (\<^const_name>\True\, []), (\<^const_name>\False\, [])]; fun mk_atomize pairs = let fun atoms th = (case Thm.concl_of th of - Const ("Trueprop", _) $ p => + Const ("Trueprop", _) $ p => (* FIXME formal const name!? *) (case head_of p of Const(a,_) => (case AList.lookup (op =) pairs a of SOME(rls) => maps atoms ([th] RL rls) | NONE => [th]) | _ => [th]) | _ => [th]) in atoms end; fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th); (*destruct function for analysing equations*) fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs) | dest_red t = raise TERM("dest_red", [t]); structure FOLP_SimpData : SIMP_DATA = struct val refl_thms = [@{thm refl}, @{thm iff_refl}] val trans_thms = [@{thm trans}, @{thm iff_trans}] val red1 = @{thm iffD1} val red2 = @{thm iffD2} val mk_rew_rules = mk_rew_rules val case_splits = [] (*NO IF'S!*) val norm_thms = norm_thms val subst_thms = [@{thm subst}]; val dest_red = dest_red end; structure FOLP_Simp = SimpFun(FOLP_SimpData); (*not a component of SIMP_DATA, but an argument of SIMP_TAC *) val FOLP_congs = [@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong}, @{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong}, @{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs}; val IFOLP_rews = [refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @ @{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews}; open FOLP_Simp; val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI}); val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew \<^context>) IFOLP_rews; val FOLP_rews = IFOLP_rews @ @{thms cla_rews}; val FOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew \<^context>) FOLP_rews;