summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Tools/meson.ML

changeset 19875 | 7405ce9d4f25 |

parent 19728 | 6c47d9295dca |

child 19894 | 7c7e15b27145 |

equal
deleted
inserted
replaced

19874:cc4b2b882e4c | 19875:7405ce9d4f25 |
---|---|

70 fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb); |
70 fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb); |

71 |
71 |

72 (*raises exception if no rules apply -- unlike RL*) |
72 (*raises exception if no rules apply -- unlike RL*) |

73 fun tryres (th, rls) = |
73 fun tryres (th, rls) = |

74 let fun tryall [] = raise THM("tryres", 0, th::rls) |
74 let fun tryall [] = raise THM("tryres", 0, th::rls) |

75 | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls) |
75 | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls) |

76 in tryall rls end; |
76 in tryall rls end; |

77 |
77 |

78 (*Permits forward proof from rules that discharge assumptions*) |
78 (*Permits forward proof from rules that discharge assumptions*) |

79 fun forward_res nf st = |
79 fun forward_res nf st = |

80 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |
80 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |

82 | NONE => raise THM("forward_res", 0, [st]); |
82 | NONE => raise THM("forward_res", 0, [st]); |

83 |
83 |

84 |
84 |

85 (*Are any of the constants in "bs" present in the term?*) |
85 (*Are any of the constants in "bs" present in the term?*) |

86 fun has_consts bs = |
86 fun has_consts bs = |

87 let fun has (Const(a,_)) = a mem bs |
87 let fun has (Const(a,_)) = member (op =) bs a |

88 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false |
88 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false |

89 (*ignore constants within @-terms*) |
89 (*ignore constants within @-terms*) |

90 | has (f$u) = has f orelse has u |
90 | has (f$u) = has f orelse has u |

91 | has (Abs(_,_,t)) = has t |
91 | has (Abs(_,_,t)) = has t |

92 | has _ = false |
92 | has _ = false |

264 | has_bool _ = false; |
264 | has_bool _ = false; |

265 |
265 |

266 (*Is the string the name of a connective? It doesn't matter if this list is |
266 (*Is the string the name of a connective? It doesn't matter if this list is |

267 incomplete, since when actually called, the only connectives likely to |
267 incomplete, since when actually called, the only connectives likely to |

268 remain are & | Not.*) |
268 remain are & | Not.*) |

269 fun is_conn c = c mem_string |
269 val is_conn = member (op =) |

270 ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", |
270 ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", |

271 "All", "Ex", "Ball", "Bex"]; |
271 "All", "Ex", "Ball", "Bex"]; |

272 |
272 |

273 (*True if the term contains a function where the type of any argument contains |
273 (*True if the term contains a function where the type of any argument contains |

274 bool.*) |
274 bool.*) |

334 (*detects repetitions in a list of terms*) |
334 (*detects repetitions in a list of terms*) |

335 fun has_reps [] = false |
335 fun has_reps [] = false |

336 | has_reps [_] = false |
336 | has_reps [_] = false |

337 | has_reps [t,u] = (t aconv u) |
337 | has_reps [t,u] = (t aconv u) |

338 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) |
338 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) |

339 handle INSERT => true; |
339 handle Net.INSERT => true; |

340 |
340 |

341 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
341 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |

342 fun TRYING_eq_assume_tac 0 st = Seq.single st |
342 fun TRYING_eq_assume_tac 0 st = Seq.single st |

343 | TRYING_eq_assume_tac i st = |
343 | TRYING_eq_assume_tac i st = |

344 TRYING_eq_assume_tac (i-1) (eq_assumption i st) |
344 TRYING_eq_assume_tac (i-1) (eq_assumption i st) |