equal
deleted
inserted
replaced
63 |
63 |
64 val depth_limit = ref 2000; |
64 val depth_limit = ref 2000; |
65 |
65 |
66 (**** Operators for forward proof ****) |
66 (**** Operators for forward proof ****) |
67 |
67 |
|
68 (*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*) |
|
69 fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb); |
|
70 |
68 (*raises exception if no rules apply -- unlike RL*) |
71 (*raises exception if no rules apply -- unlike RL*) |
69 fun tryres (th, rls) = |
72 fun tryres (th, rls) = |
70 let fun tryall [] = raise THM("tryres", 0, th::rls) |
73 let fun tryall [] = raise THM("tryres", 0, th::rls) |
71 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) |
74 | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls) |
72 in tryall rls end; |
75 in tryall rls end; |
73 |
76 |
74 (*Permits forward proof from rules that discharge assumptions*) |
77 (*Permits forward proof from rules that discharge assumptions*) |
75 fun forward_res nf st = |
78 fun forward_res nf st = |
76 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |
79 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |