author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 52467  24c6ddb48cb8 
child 59582  0fbed69ff081 
permissions  rwrr 
23175  1 
(* Title: Tools/IsaPlanner/isand.ML 
23171  2 
Author: Lucas Dixon, University of Edinburgh 
23175  3 

52244  4 
Natural Deduction tools (obsolete). 
23171  5 

23175  6 
For working with Isabelle theorems in a natural detuction style. 
7 
ie, not having to deal with meta level quantified varaibles, 

8 
instead, we work with newly introduced frees, and hide the 

9 
"all"'s, exporting results from theorems proved with the frees, to 

10 
solve the all cases of the previous goal. This allows resolution 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

11 
to do proof search normally. 
23171  12 

23175  13 
Note: A nice idea: allow exporting to solve any subgoal, thus 
14 
allowing the interleaving of proof, or provide a structure for the 

15 
ordering of proof, thus allowing proof attempts in parrell, but 

16 
recording the order to apply things in. 

23171  17 

23175  18 
THINK: are we really ok with our varify name w.r.t the prop  do 
19 
we also need to avoid names in the hidden hyps? What about 

20 
unification contraints in flexflex pairs  might they also have 

21 
extra free vars? 

23171  22 
*) 
23 

24 
signature ISA_ND = 

25 
sig 

52244  26 
val variant_names: Proof.context > term list > string list > string list 
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

27 

23171  28 
(* meta level fixed params (i.e. !! vars) *) 
52244  29 
val fix_alls_term: Proof.context > int > term > term * term list 
23171  30 

31 
(* assumptions/subgoals *) 

52244  32 
val fixed_subgoal_thms: Proof.context > thm > thm list * (thm list > thm) 
23171  33 
end 
34 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

35 
structure IsaND : ISA_ND = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

36 
struct 
23171  37 

38 
(* datatype to capture an exported result, ie a fix or assume. *) 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

39 
datatype export = 
52244  40 
Export of 
41 
{fixes : Thm.cterm list, (* fixed vars *) 

42 
assumes : Thm.cterm list, (* hidden hyps/assumed prems *) 

43 
sgid : int, 

44 
gth : Thm.thm}; (* subgoal/goalthm *) 

23171  45 

46 
(* exporting function that takes a solution to the fixed/assumed goal, 

47 
and uses this to solve the subgoal in the main theorem *) 

52244  48 
fun export_solution (Export {fixes = cfvs, assumes = hcprems, sgid = i, gth = gth}) solth = 
49 
let 

50 
val solth' = solth 

51 
> Drule.implies_intr_list hcprems 

52 
> Drule.forall_intr_list cfvs; 

52467  53 
in Drule.compose (solth', i, gth) end; 
23171  54 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

55 
fun variant_names ctxt ts xs = 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

56 
let 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

57 
val names = 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

58 
Variable.names_of ctxt 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

59 
> (fold o fold_aterms) 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

60 
(fn Var ((a, _), _) => Name.declare a 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

61 
 Free (a, _) => Name.declare a 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

62 
 _ => I) ts; 
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

63 
in fst (fold_map Name.variant xs names) end; 
23171  64 

65 
(* fix parameters of a subgoal "i", as free variables, and create an 

66 
exporting function that will use the result of this proved goal to 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

67 
show the goal in the original theorem. 
23171  68 

69 
Note, an advantage of this over Isar is that it supports instantiation 

70 
of unkowns in the earlier theorem, ie we can do instantiation of meta 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

71 
vars! 
23171  72 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

73 
avoids constant, free and vars names. 
23171  74 

75 
loosely corresponds to: 

76 
Given "[ SG0; ... !! x. As ==> SGi x; ... SGm ] ==> G" : thm 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

77 
Result: 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

78 
("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

79 
expf : 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

80 
("As ==> SGi x'" : thm) > 
23171  81 
("[ SG0; ... SGi1; SGi+1; ... SGm ] ==> G") : thm) 
82 
*) 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

83 
fun fix_alls_term ctxt i t = 
52244  84 
let 
85 
val gt = Logic.get_goal t i; 

86 
val body = Term.strip_all_body gt; 

87 
val alls = rev (Term.strip_all_vars gt); 

88 
val xs = variant_names ctxt [t] (map fst alls); 

89 
val fvs = map Free (xs ~~ map snd alls); 

90 
in ((subst_bounds (fvs,body)), fvs) end; 

23171  91 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

92 
fun fix_alls_cterm ctxt i th = 
52244  93 
let 
94 
val cert = Thm.cterm_of (Thm.theory_of_thm th); 

95 
val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th); 

96 
val cfvs = rev (map cert fvs); 

97 
val ct_body = cert fixedbody; 

98 
in (ct_body, cfvs) end; 

23171  99 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

100 
fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i; 
23171  101 

102 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

103 
(* hide other goals *) 
23171  104 
(* note the export goal is rotated by (i  1) and will have to be 
105 
unrotated to get backto the originial position(s) *) 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

106 
fun hide_other_goals th = 
52244  107 
let 
108 
(* tl beacuse fst sg is the goal we are interested in *) 

109 
val cprems = tl (Drule.cprems_of th); 

110 
val aprems = map Thm.assume cprems; 

111 
in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end; 

23171  112 

113 
(* a nicer version of the above that leaves only a single subgoal (the 

114 
other subgoals are hidden hyps, that the exporter suffles about) 

115 
namely the subgoal that we were trying to solve. *) 

116 
(* loosely corresponds to: 

117 
Given "[ SG0; ... !! x. As ==> SGi x; ... SGm ] ==> G" : thm 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

118 
Result: 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

119 
("(As ==> SGi x') ==> SGi x'" : thm, 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

120 
expf : 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

121 
("SGi x'" : thm) > 
23171  122 
("[ SG0; ... SGi1; SGi+1; ... SGm ] ==> G") : thm) 
123 
*) 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

124 
fun fix_alls ctxt i th = 
52244  125 
let 
126 
val (fixed_gth, fixedvars) = fix_alls' ctxt i th 

127 
val (sml_gth, othergoals) = hide_other_goals fixed_gth 

128 
in (sml_gth, Export {fixes = fixedvars, assumes = othergoals, sgid = i, gth = th}) end; 

23171  129 

130 

131 
(* Fixme: allow different order of subgoals given to expf *) 

132 
(* make each subgoal into a separate thm that needs to be proved *) 

133 
(* loosely corresponds to: 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

134 
Given 
23171  135 
"[ SG0; ... SGm ] ==> G" : thm 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

136 
Result: 
23171  137 
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list,  goals 
138 
["SG0", ..., "SGm"] : thm list >  export function 

139 
"G" : thm) 

140 
*) 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

141 
fun subgoal_thms th = 
52244  142 
let 
143 
val cert = Thm.cterm_of (Thm.theory_of_thm th); 

23171  144 

52244  145 
val t = prop_of th; 
23171  146 

52244  147 
val prems = Logic.strip_imp_prems t; 
148 
val aprems = map (Thm.trivial o cert) prems; 

23171  149 

52244  150 
fun explortf premths = Drule.implies_elim_list th premths; 
151 
in (aprems, explortf) end; 

23171  152 

153 

154 
(* Fixme: allow different order of subgoals in exportf *) 

155 
(* as above, but also fix all parameters in all subgoals, and uses 

156 
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent 

157 
subgoals. *) 

158 
(* loosely corresponds to: 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

159 
Given 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

160 
"[ !! x0s. A0s x0s ==> SG0 x0s; 
23171  161 
...; !! xms. Ams xms ==> SGm xms] ==> G" : thm 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

162 
Result: 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
46777
diff
changeset

163 
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
23171  164 
... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list,  goals 
165 
["SG0 x0s'", ..., "SGm xms'"] : thm list >  export function 

166 
"G" : thm) 

167 
*) 

168 
(* requires being given solutions! *) 

49340
25fc6e0da459
observe context more carefully when producing "fresh" variables  for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset

169 
fun fixed_subgoal_thms ctxt th = 
52244  170 
let 
171 
val (subgoals, expf) = subgoal_thms th; 

172 
(* fun export_sg (th, exp) = exp th; *) 

173 
fun export_sgs expfs solthms = 

174 
expf (map2 (curry (op >)) solthms expfs); 

175 
(* expf (map export_sg (ths ~~ expfs)); *) 

176 
in 

177 
apsnd export_sgs 

178 
(Library.split_list (map (apsnd export_solution o fix_alls ctxt 1) subgoals)) 

179 
end; 

23171  180 

181 
end; 