summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Tools/IsaPlanner/isand.ML

author | wenzelm |

Thu Jun 27 17:06:22 2013 +0200 (2013-06-27) | |

changeset 52467 | 24c6ddb48cb8 |

parent 52246 | 54c0d4128b30 |

child 59582 | 0fbed69ff081 |

permissions | -rw-r--r-- |

tuned signature;

1 (* Title: Tools/IsaPlanner/isand.ML

2 Author: Lucas Dixon, University of Edinburgh

4 Natural Deduction tools (obsolete).

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

11 to do proof search normally.

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.

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 flex-flex pairs - might they also have

21 extra free vars?

22 *)

24 signature ISA_ND =

25 sig

26 val variant_names: Proof.context -> term list -> string list -> string list

28 (* meta level fixed params (i.e. !! vars) *)

29 val fix_alls_term: Proof.context -> int -> term -> term * term list

31 (* assumptions/subgoals *)

32 val fixed_subgoal_thms: Proof.context -> thm -> thm list * (thm list -> thm)

33 end

35 structure IsaND : ISA_ND =

36 struct

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

39 datatype export =

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 *)

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

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

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;

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

55 fun variant_names ctxt ts xs =

56 let

57 val names =

58 Variable.names_of ctxt

59 |> (fold o fold_aterms)

60 (fn Var ((a, _), _) => Name.declare a

61 | Free (a, _) => Name.declare a

62 | _ => I) ts;

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

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

67 show the goal in the original theorem.

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

71 vars!

73 avoids constant, free and vars names.

75 loosely corresponds to:

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

77 Result:

78 ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,

79 expf :

80 ("As ==> SGi x'" : thm) ->

81 ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)

82 *)

83 fun fix_alls_term ctxt i t =

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;

92 fun fix_alls_cterm ctxt i th =

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;

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

103 (* hide other goals *)

104 (* note the export goal is rotated by (i - 1) and will have to be

105 unrotated to get backto the originial position(s) *)

106 fun hide_other_goals th =

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;

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

118 Result:

119 ("(As ==> SGi x') ==> SGi x'" : thm,

120 expf :

121 ("SGi x'" : thm) ->

122 ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)

123 *)

124 fun fix_alls ctxt i th =

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;

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:

134 Given

135 "[| SG0; ... SGm |] ==> G" : thm

136 Result:

137 (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals

138 ["SG0", ..., "SGm"] : thm list -> -- export function

139 "G" : thm)

140 *)

141 fun subgoal_thms th =

142 let

143 val cert = Thm.cterm_of (Thm.theory_of_thm th);

145 val t = prop_of th;

147 val prems = Logic.strip_imp_prems t;

148 val aprems = map (Thm.trivial o cert) prems;

150 fun explortf premths = Drule.implies_elim_list th premths;

151 in (aprems, explortf) end;

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:

159 Given

160 "[| !! x0s. A0s x0s ==> SG0 x0s;

161 ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm

162 Result:

163 (["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",

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! *)

169 fun fixed_subgoal_thms ctxt th =

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;

181 end;