author  hoelzl 
Mon, 08 Aug 2016 14:13:14 +0200  
changeset 63627  6ddb43c6b711 
parent 61268  abe08fb15a12 
child 69593  3dda49e08b9d 
permissions  rwrr 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

1 
(* Title: Sequents/simpdata.ML 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

3 
Copyright 1999 University of Cambridge 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

4 

27149  5 
Instantiation of the generic simplifier for LK. 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

6 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

7 
Borrows from the DC simplifier of Soren Heilmann. 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

8 
*) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

9 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

10 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

11 
(** Conversion into rewrite rules **) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

12 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

13 
(*Make atomic rewrite rules*) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

14 
fun atomize r = 
59582  15 
case Thm.concl_of r of 
38500  16 
Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => 
55228  17 
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of 
9713  18 
([], [p]) => 
19 
(case p of 

38500  20 
Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R}) 
21 
 Const(@{const_name conj},_)$_$_ => atomize(r RS @{thm conjunct1}) @ 

22896  22 
atomize(r RS @{thm conjunct2}) 
38500  23 
 Const(@{const_name All},_)$_ => atomize(r RS @{thm spec}) 
24 
 Const(@{const_name True},_) => [] (*True is DELETED*) 

25 
 Const(@{const_name False},_) => [] (*should False do something?*) 

9713  26 
 _ => [r]) 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

27 
 _ => []) (*ignore theorem unless it has precisely one conclusion*) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

28 
 _ => [r]; 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

29 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

30 
(*Make metaequalities.*) 
59582  31 
fun mk_meta_eq ctxt th = case Thm.concl_of th of 
56245  32 
Const(@{const_name Pure.eq},_)$_$_ => th 
38500  33 
 Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => 
55228  34 
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of 
9713  35 
([], [p]) => 
36 
(case p of 

38500  37 
(Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection} 
38 
 (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} 

39 
 (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} 

27149  40 
 _ => th RS @{thm iff_reflection_T}) 
61268  41 
 _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

42 

7123  43 
(*Replace premises x=y, X<>Y by X==Y*) 
36546  44 
fun mk_meta_prems ctxt = 
45 
rule_by_tactic ctxt 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

46 
(REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); 
7123  47 

9713  48 
(*Congruence rules for = or <> (instead of ==)*) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

49 
fun mk_meta_cong ctxt rl = 
55228  50 
Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl)) 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset

51 
handle THM _ => 
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset

52 
error("Premises and conclusion of congruence rules must use =equality or <>"); 
7123  53 

54 

7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

55 
(*** Standard simpsets ***) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

56 

27149  57 
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, 
58 
@{thm iff_refl}, reflexive_thm]; 

7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

59 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

60 
fun unsafe_solver ctxt = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

61 
FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt]; 
27149  62 

7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

63 
(*No premature instantiation of variables during simplification*) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

64 
fun safe_solver ctxt = 
58957  65 
FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i), 
66 
eq_assume_tac]; 

7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

67 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

68 
(*No simprules, but basic infrastructure for simplification*) 
9713  69 
val LK_basic_ss = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

70 
empty_simpset @{context} 
45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

71 
setSSolver (mk_solver "safe" safe_solver) 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

72 
setSolver (mk_solver "unsafe" unsafe_solver) 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

73 
> Simplifier.set_subgoaler asm_simp_tac 
60822  74 
> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

75 
> Simplifier.set_mkcong mk_meta_cong 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

76 
> simpset_of; 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

77 

86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

78 
val LK_simps = 
46186  79 
[@{thm triv_forall_equality}, (* prunes params *) 
27149  80 
@{thm refl} RS @{thm P_iff_T}] @ 
81 
@{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ 

82 
@{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @ 

83 
@{thms all_simps} @ @{thms ex_simps} @ 

84 
[@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ 

85 
@{thms LK_extra_simps}; 

7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

86 

9713  87 
val LK_ss = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

88 
put_simpset LK_basic_ss @{context} addsimps LK_simps 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
43597
diff
changeset

89 
> Simplifier.add_eqcong @{thm left_cong} 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

90 
> Simplifier.add_cong @{thm imp_cong} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46186
diff
changeset

91 
> simpset_of; 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

92 