author  wenzelm 
Fri, 19 Feb 2010 16:11:45 +0100  
changeset 35232  f588e1169c8b 
parent 35021  c839a4c670c6 
child 35762  af3ff2ba4c54 
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 
ID: $Id$ 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

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

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

5 

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

7 

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

8 
Borrows from the DC simplifier of Soren Heilmann. 
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 

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

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

13 

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

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

15 
fun atomize r = 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

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

17 
Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

18 
(case (forms_of_seq a, forms_of_seq c) of 
9713  19 
([], [p]) => 
20 
(case p of 

22896  21 
Const("imp",_)$_$_ => atomize(r RS @{thm mp_R}) 
22 
 Const("conj",_)$_$_ => atomize(r RS @{thm conjunct1}) @ 

23 
atomize(r RS @{thm conjunct2}) 

24 
 Const("All",_)$_ => atomize(r RS @{thm spec}) 

9713  25 
 Const("True",_) => [] (*True is DELETED*) 
26 
 Const("False",_) => [] (*should False do something?*) 

27 
 _ => [r]) 

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

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

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

30 

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

31 
(*Make metaequalities.*) 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

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

33 
Const("==",_)$_$_ => th 
86583034aacf
installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff
changeset

34 
 Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) => 
9713  35 
(case (forms_of_seq a, forms_of_seq c) of 
36 
([], [p]) => 

37 
(case p of 

22896  38 
(Const("equal",_)$_$_) => th RS @{thm eq_reflection} 
39 
 (Const("iff",_)$_$_) => th RS @{thm iff_reflection} 

27149  40 
 (Const("Not",_)$_) => th RS @{thm iff_reflection_F} 
41 
 _ => th RS @{thm iff_reflection_T}) 

9713  42 
 _ => 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

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

44 

7123  45 
(*Replace premises x=y, X<>Y by X==Y*) 
9713  46 
val mk_meta_prems = 
47 
rule_by_tactic 

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

9713  50 
(*Congruence rules for = or <> (instead of ==)*) 
7123  51 
fun mk_meta_cong 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 
Drule.export_without_context(mk_meta_eq (mk_meta_prems rl)) 
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 
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

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

56 

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

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

58 

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

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

61 

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

64 

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

65 
(*No premature instantiation of variables during simplification*) 
27149  66 
fun safe_solver prems = 
67 
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

68 

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

69 
(*No simprules, but basic infrastructure for simplification*) 
9713  70 
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

71 
Simplifier.global_context @{theory} empty_ss 
17892  72 
setsubgoaler asm_simp_tac 
9713  73 
setSSolver (mk_solver "safe" safe_solver) 
74 
setSolver (mk_solver "unsafe" unsafe_solver) 

12725  75 
setmksimps (map mk_meta_eq o atomize o gen_all) 
9713  76 
setmkcong mk_meta_cong; 
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 = 
7123  79 
[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 = 
88 
LK_basic_ss addsimps LK_simps 

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

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

91 

17876  92 
change_simpset (fn _ => LK_ss); 