author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46186  9ae331a1d8c5 
child 51717  9e7d1c139569 
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 = 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

15 
case concl_of r of 
38500  16 
Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

17 
(case (forms_of_seq a, 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.*) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

31 
fun mk_meta_eq th = case concl_of th of 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

32 
Const("==",_)$_$_ => th 
38500  33 
 Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => 
9713  34 
(case (forms_of_seq a, forms_of_seq c) of 
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}) 
9713  41 
 _ => error ("addsimps: unable to use theorem\n" ^ 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
27149
diff
changeset

42 
Display.string_of_thm_without_context th)); 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

43 

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

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

9713  49 
(*Congruence rules for = or <> (instead of ==)*) 
36546  50 
fun mk_meta_cong ss rl = 
45659
09539cdffcd7
avoid stepping outside of context  plain zero_var_indexes should be sufficient;
wenzelm
parents:
45625
diff
changeset

51 
Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) 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

52 
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

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

55 

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

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

57 

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

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

60 

43596  61 
fun unsafe_solver ss = 
43597  62 
FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac]; 
27149  63 

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

64 
(*No premature instantiation of variables during simplification*) 
43596  65 
fun safe_solver ss = 
43597  66 
FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), 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 = 
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
35021
diff
changeset

70 
Simplifier.global_context @{theory} empty_ss 
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 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

74 
> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all)) 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

75 
> Simplifier.set_mkcong mk_meta_cong; 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

76 

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

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

81 
@{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @ 

82 
@{thms all_simps} @ @{thms ex_simps} @ 

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

84 
@{thms LK_extra_simps}; 

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

85 

9713  86 
val LK_ss = 
87 
LK_basic_ss 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

88 
> Simplifier.add_eqcong @{thm left_cong} 
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_cong @{thm imp_cong}; 
7098
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

90 