author  wenzelm 
Sun, 30 Jul 2006 21:28:52 +0200  
changeset 20260  990dbc007ca6 
parent 20250  c3f209752749 
child 20290  3f886c176c9b 
permissions  rwrr 
17980  1 
(* Title: Pure/goal.ML 
2 
ID: $Id$ 

3 
Author: Makarius and Lawrence C Paulson 

4 

18139  5 
Goals in tactical theorem proving. 
17980  6 
*) 
7 

8 
signature BASIC_GOAL = 

9 
sig 

10 
val SELECT_GOAL: tactic > int > tactic 

11 
end; 

12 

13 
signature GOAL = 

14 
sig 

15 
include BASIC_GOAL 

16 
val init: cterm > thm 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

17 
val protect: thm > thm 
17980  18 
val conclude: thm > thm 
19 
val finish: thm > thm 

18119  20 
val compose_hhf: thm > int > thm > thm Seq.seq 
21 
val compose_hhf_tac: thm > int > tactic 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

22 
val comp_hhf: thm > thm > thm 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

23 
val prove_raw: cterm list > cterm > (thm list > tactic) > thm 
20056  24 
val prove_multi: Context.proof > string list > term list > term list > 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

25 
({prems: thm list, context: Context.proof} > tactic) > thm list 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

26 
val prove: Context.proof > string list > term list > term > 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

27 
({prems: thm list, context: Context.proof} > tactic) > thm 
20056  28 
val prove_global: theory > string list > term list > term > (thm list > tactic) > thm 
19184  29 
val extract: int > int > thm > thm Seq.seq 
30 
val retrofit: int > int > thm > thm > thm Seq.seq 

17980  31 
end; 
32 

33 
structure Goal: GOAL = 

34 
struct 

35 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

36 
(** goals **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

37 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

38 
(* 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

39 
 (init) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

40 
C ==> #C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

41 
*) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

42 
fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI; 
17980  43 

44 
(* 

18119  45 
C 
46 
 (protect) 

47 
#C 

17980  48 
*) 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

49 
fun protect th = th COMP Drule.incr_indexes th Drule.protectI; 
17980  50 

51 
(* 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

52 
A ==> ... ==> #C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

53 
 (conclude) 
17980  54 
A ==> ... ==> C 
55 
*) 

56 
fun conclude th = 

18497  57 
(case SINGLE (Thm.compose_no_flatten false (th, Thm.nprems_of th) 1) 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

58 
(Drule.incr_indexes th Drule.protectD) of 
17980  59 
SOME th' => th' 
60 
 NONE => raise THM ("Failed to conclude goal", 0, [th])); 

61 

62 
(* 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

63 
#C 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

64 
 (finish) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

65 
C 
17983  66 
*) 
17980  67 
fun finish th = 
68 
(case Thm.nprems_of th of 

69 
0 => conclude th 

70 
 n => raise THM ("Proof failed.\n" ^ 

71 
Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^ 

72 
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); 

73 

74 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

75 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

76 
(** results **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

77 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

78 
(* composition of normal results *) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

79 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

80 
fun compose_hhf tha i thb = 
18145  81 
Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb; 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

82 

18119  83 
fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i); 
84 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

85 
fun comp_hhf tha thb = 
19862  86 
(case Seq.chop 2 (compose_hhf tha 1 thb) of 
18119  87 
([th], _) => th 
88 
 ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb]) 

89 
 _ => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb])); 

17986  90 

91 

18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

92 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

93 
(** tactical theorem proving **) 
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

94 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

95 
(* prove_raw  no checks, no normalization of result! *) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

96 

c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

97 
fun prove_raw casms cprop tac = 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

98 
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

99 
SOME th => Drule.implies_intr_list casms (finish th) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

100 
 NONE => error "Tactic failed."); 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

101 

c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

102 

18119  103 
(* prove_multi *) 
17986  104 

20056  105 
fun prove_multi ctxt xs asms props tac = 
17980  106 
let 
20056  107 
val thy = Context.theory_of_proof ctxt; 
108 
val string_of_term = Sign.string_of_term thy; 

109 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

110 
fun err msg = cat_error msg 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

111 
("The error(s) above occurred for the goal statement:\n" ^ 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

112 
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props))); 
17980  113 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

114 
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) 
17980  115 
handle TERM (msg, _) => err msg  TYPE (msg, _, _) => err msg; 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

116 
val casms = map cert_safe asms; 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

117 
val cprops = map cert_safe props; 
17980  118 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

119 
val (prems, ctxt') = ctxt 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

120 
> Variable.add_fixes_direct xs 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

121 
> fold Variable.declare_internal (asms @ props) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

122 
> Assumption.add_assumes casms; 
17980  123 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

124 
val goal = init (Conjunction.mk_conjunction_list cprops); 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

125 
val res = 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

126 
(case SINGLE (tac {prems = prems, context = ctxt'}) goal of 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

127 
NONE => err "Tactic failed." 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19619
diff
changeset

128 
 SOME res => res); 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

129 
val [results] = Conjunction.elim_precise [length props] (finish res) 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

130 
handle THM (msg, _, _) => err msg; 
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

131 
val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results) 
20056  132 
orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res)); 
17980  133 
in 
20056  134 
results 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

135 
> (Seq.hd o Assumption.exports false ctxt' ctxt) 
20056  136 
> Variable.export ctxt' ctxt 
20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

137 
> map Drule.zero_var_indexes 
17980  138 
end; 
139 

140 

18119  141 
(* prove *) 
17980  142 

20056  143 
fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac); 
144 

145 
fun prove_global thy xs asms prop tac = 

20250
c3f209752749
prove: proper assumption context, more tactic arguments;
wenzelm
parents:
20228
diff
changeset

146 
Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems)); 
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

147 

09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset

148 

17980  149 

19184  150 
(** local goal states **) 
18207  151 

19184  152 
fun extract i n st = 
153 
(if i < 1 orelse n < 1 orelse i + n  1 > Thm.nprems_of st then Seq.empty 

154 
else if n = 1 then Seq.single (Thm.cprem_of st i) 

19423  155 
else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n  1)))) 
20260  156 
> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init); 
17980  157 

19221  158 
fun retrofit i n st' st = 
159 
(if n = 1 then st 

19423  160 
else st > Drule.rotate_prems (i  1) > Conjunction.uncurry n > Drule.rotate_prems (1  i)) 
19221  161 
> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i; 
18207  162 

17980  163 
fun SELECT_GOAL tac i st = 
19191  164 
if Thm.nprems_of st = 1 andalso i = 1 then tac st 
19184  165 
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; 
17980  166 

18207  167 
end; 
168 

17980  169 
structure BasicGoal: BASIC_GOAL = Goal; 
170 
open BasicGoal; 