author  blanchet 
Mon, 20 Dec 2010 14:17:49 +0100  
changeset 41317  fc48faccd77b 
parent 38500  d5477ee35820 
child 42795  66fcc9882784 
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 = 
51 
Drule.export_without_context (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 

27149  61 
fun unsafe_solver prems = 
62 
FIRST' [resolve_tac (triv_rls @ prems), assume_tac]; 

63 

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

64 
(*No premature instantiation of variables during simplification*) 
27149  65 
fun safe_solver prems = 
66 
FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) 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 
17892  71 
setsubgoaler asm_simp_tac 
9713  72 
setSSolver (mk_solver "safe" safe_solver) 
73 
setSolver (mk_solver "unsafe" unsafe_solver) 

36543
0e7fc5bf38de
proper context for mksimps etc.  via simpset of the running Simplifier;
wenzelm
parents:
35762
diff
changeset

74 
setmksimps (K (map mk_meta_eq o atomize o gen_all)) 
9713  75 
setmkcong 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 = 
7123  78 
[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 

27149  88 
addeqcongs [@{thm left_cong}] 
89 
addcongs [@{thm imp_cong}]; 

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

90 

17876  91 
change_simpset (fn _ => LK_ss); 