author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18947  de38ee3654d4 
permissions  rwrr 
6778  1 
(* Title: Pure/Isar/calculation.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

5 
Generic calculational proofs. 
6778  6 
*) 
7 

8 
signature CALCULATION = 

9 
sig 

18637  10 
val print_rules: Context.generic > unit 
16571  11 
val get_calculation: Proof.state > thm list option 
18728  12 
val trans_add: attribute 
13 
val trans_del: attribute 

14 
val sym_add: attribute 

15 
val sym_del: attribute 

16 
val symmetric: attribute 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

17 
val also: (thmref * Attrib.src list) list option > bool > Proof.state > Proof.state Seq.seq 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

18 
val also_i: thm list option > bool > Proof.state > Proof.state Seq.seq 
18637  19 
val finally: (thmref * Attrib.src list) list option > bool > Proof.state > Proof.state Seq.seq 
17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

20 
val finally_i: thm list option > bool > Proof.state > Proof.state Seq.seq 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

21 
val moreover: bool > Proof.state > Proof.state 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

22 
val ultimately: bool > Proof.state > Proof.state 
6778  23 
end; 
24 

25 
structure Calculation: CALCULATION = 

26 
struct 

27 

18637  28 
(** calculation data **) 
6778  29 

18637  30 
structure CalculationData = GenericDataFun 
31 
( 

6778  32 
val name = "Isar/calculation"; 
12379  33 
type T = (thm NetRules.T * thm list) * (thm list * int) option; 
18637  34 
val empty = ((NetRules.elim, []), NONE); 
35 
val extend = I; 

6778  36 

18637  37 
fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = 
38 
((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE); 

6778  39 

18637  40 
fun print generic ((trans, sym), _) = 
41 
let val ctxt = Context.proof_of generic in 

42 
[Pretty.big_list "transitivity rules:" 

43 
(map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), 

44 
Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] 

45 
> Pretty.chunks > Pretty.writeln 

46 
end; 

47 
); 

48 

18708  49 
val _ = Context.add_setup CalculationData.init; 
18637  50 
val print_rules = CalculationData.print; 
6778  51 

52 

53 
(* access calculation *) 

54 

55 
fun get_calculation state = 

18637  56 
(case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of 
15531  57 
NONE => NONE 
58 
 SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE); 

6778  59 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

60 
val calculationN = "calculation"; 
6778  61 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

62 
fun put_calculation calc = 
18728  63 
`Proof.level #> (fn lev => Proof.map_context (Context.proof_map 
64 
(CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

65 
#> Proof.put_thms (calculationN, calc); 
6778  66 

67 

18637  68 

6778  69 
(** attributes **) 
70 

12379  71 
(* add/del rules *) 
72 

18728  73 
val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); 
74 
val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); 

6778  75 

18637  76 
val sym_add = 
18728  77 
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule) 
18637  78 
#> ContextRules.elim_query NONE; 
79 
val sym_del = 

18728  80 
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule) 
18637  81 
#> ContextRules.rule_del; 
12379  82 

83 

18637  84 
(* symmetric *) 
12379  85 

18728  86 
val symmetric = Thm.rule_attribute (fn x => fn th => 
18637  87 
(case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of 
12379  88 
([th'], _) => th' 
89 
 ([], _) => raise THM ("symmetric: no unifiers", 1, [th]) 

90 
 _ => raise THM ("symmetric: multiple unifiers", 1, [th]))); 

91 

6778  92 

93 
(* concrete syntax *) 

94 

18637  95 
val trans_att = Attrib.add_del_args trans_add trans_del; 
96 
val sym_att = Attrib.add_del_args sym_add sym_del; 

12379  97 

15801  98 
val _ = Context.add_setup 
18708  99 
(Attrib.add_attributes 
18728  100 
[("trans", trans_att, "declaration of transitivity rule"), 
101 
("sym", sym_att, "declaration of symmetry rule"), 

102 
("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #> 

18708  103 
PureThy.add_thms 
18728  104 
[(("", transitive_thm), [trans_add]), 
105 
(("", symmetric_thm), [sym_add])] #> snd); 

15801  106 

6778  107 

6787  108 

6778  109 
(** proof commands **) 
110 

18678  111 
fun err_if b msg = if b then error msg else (); 
17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

112 

14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset

113 
fun assert_sane final = 
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset

114 
if final then Proof.assert_forward else Proof.assert_forward_or_chain; 
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset

115 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

116 
fun maintain_calculation false calc = put_calculation (SOME calc) 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

117 
 maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; 
6778  118 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

119 
fun print_calculation false _ _ = () 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

120 
 print_calculation true ctxt calc = 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

121 
Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc)); 
8562  122 

123 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

124 
(* also and finally *) 
8562  125 

18637  126 
val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; 
127 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

128 
fun calculate prep_rules final raw_rules int state = 
6778  129 
let 
12805  130 
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; 
9322  131 
val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl); 
11097  132 
fun projection ths th = Library.exists (Library.curry eq_prop th) ths; 
8300  133 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

134 
val opt_rules = Option.map (prep_rules state) raw_rules; 
11097  135 
fun combine ths = 
15531  136 
(case opt_rules of SOME rules => rules 
137 
 NONE => 

18637  138 
(case ths of [] => NetRules.rules (#1 (get_rules state)) 
139 
 th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th))) 

18223  140 
> Seq.of_list > Seq.maps (Drule.multi_resolve ths) 
11097  141 
> Seq.filter (not o projection ths); 
7414  142 

14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset

143 
val facts = Proof.the_facts (assert_sane final state); 
6903  144 
val (initial, calculations) = 
6778  145 
(case get_calculation state of 
15531  146 
NONE => (true, Seq.single facts) 
147 
 SOME calc => (false, Seq.map single (combine (calc @ facts)))); 

6778  148 
in 
18678  149 
err_if (initial andalso final) "No calculation yet"; 
150 
err_if (initial andalso is_some opt_rules) "Initial calculation  no rules to be given"; 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

151 
calculations > Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc; 
12055  152 
state > maintain_calculation final calc)) 
6778  153 
end; 
154 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

155 
val also = calculate Proof.get_thmss false; 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

156 
val also_i = calculate (K I) false; 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

157 
val finally = calculate Proof.get_thmss true; 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

158 
val finally_i = calculate (K I) true; 
6778  159 

160 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

161 
(* moreover and ultimately *) 
8562  162 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

163 
fun collect final int state = 
8588  164 
let 
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset

165 
val facts = Proof.the_facts (assert_sane final state); 
8588  166 
val (initial, thms) = 
167 
(case get_calculation state of 

15531  168 
NONE => (true, []) 
169 
 SOME thms => (false, thms)); 

8588  170 
val calc = thms @ facts; 
171 
in 

18678  172 
err_if (initial andalso final) "No calculation yet"; 
17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

173 
print_calculation int (Proof.context_of state) calc; 
8588  174 
state > maintain_calculation final calc 
175 
end; 

176 

17350
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

177 
val moreover = collect false; 
26cd3756377a
more selfcontained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset

178 
val ultimately = collect true; 
8562  179 

6778  180 
end; 