122 struct |
122 struct |
123 |
123 |
124 (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
124 (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
125 fun trace_goalno_tac tac i st = |
125 fun trace_goalno_tac tac i st = |
126 case Seq.pull(tac i st) of |
126 case Seq.pull(tac i st) of |
127 None => Seq.empty |
127 NONE => Seq.empty |
128 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
128 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
129 Seq.make(fn()=> seqcell)); |
129 Seq.make(fn()=> seqcell)); |
130 |
130 |
131 (*Makes a rule by applying a tactic to an existing rule*) |
131 (*Makes a rule by applying a tactic to an existing rule*) |
132 fun rule_by_tactic tac rl = |
132 fun rule_by_tactic tac rl = |
133 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
133 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
134 in case Seq.pull (tac st) of |
134 in case Seq.pull (tac st) of |
135 None => raise THM("rule_by_tactic", 0, [rl]) |
135 NONE => raise THM("rule_by_tactic", 0, [rl]) |
136 | Some(st',_) => Thm.varifyT (thaw st') |
136 | SOME(st',_) => Thm.varifyT (thaw st') |
137 end; |
137 end; |
138 |
138 |
139 (*** Basic tactics ***) |
139 (*** Basic tactics ***) |
140 |
140 |
141 (*** The following fail if the goal number is out of range: |
141 (*** The following fail if the goal number is out of range: |
225 (*read instantiations with respect to subgoal i of proof state st*) |
225 (*read instantiations with respect to subgoal i of proof state st*) |
226 fun read_insts_in_state (st, i, sinsts, rule) = |
226 fun read_insts_in_state (st, i, sinsts, rule) = |
227 let val {sign,...} = rep_thm st |
227 let val {sign,...} = rep_thm st |
228 and params = params_of_state st i |
228 and params = params_of_state st i |
229 and rts = types_sorts rule and (types,sorts) = types_sorts st |
229 and rts = types_sorts rule and (types,sorts) = types_sorts st |
230 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
230 fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm) |
231 | types'(ixn) = types ixn; |
231 | types'(ixn) = types ixn; |
232 val used = add_term_tvarnames |
232 val used = add_term_tvarnames |
233 (prop_of st $ prop_of rule,[]) |
233 (prop_of st $ prop_of rule,[]) |
234 in read_insts sign rts (types',sorts) used sinsts end; |
234 in read_insts sign rts (types',sorts) used sinsts end; |
235 |
235 |
418 |
418 |
419 (*insert one tagged brl into the pair of nets*) |
419 (*insert one tagged brl into the pair of nets*) |
420 fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) = |
420 fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) = |
421 if eres then |
421 if eres then |
422 (case try Thm.major_prem_of th of |
422 (case try Thm.major_prem_of th of |
423 Some prem => (inet, Net.insert_term ((prem, kbrl), enet, K false)) |
423 SOME prem => (inet, Net.insert_term ((prem, kbrl), enet, K false)) |
424 | None => error "insert_tagged_brl: elimination rule with no premises") |
424 | NONE => error "insert_tagged_brl: elimination rule with no premises") |
425 else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
425 else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
426 |
426 |
427 (*build a pair of nets for biresolution*) |
427 (*build a pair of nets for biresolution*) |
428 fun build_netpair netpair brls = |
428 fun build_netpair netpair brls = |
429 foldr insert_tagged_brl (taglist 1 brls, netpair); |
429 foldr insert_tagged_brl (taglist 1 brls, netpair); |
433 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') |
433 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') |
434 in |
434 in |
435 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) = |
435 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) = |
436 (if eres then |
436 (if eres then |
437 (case try Thm.major_prem_of th of |
437 (case try Thm.major_prem_of th of |
438 Some prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl)) |
438 SOME prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl)) |
439 | None => (inet, enet)) (*no major premise: ignore*) |
439 | NONE => (inet, enet)) (*no major premise: ignore*) |
440 else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet)) |
440 else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet)) |
441 handle Net.DELETE => (inet,enet); |
441 handle Net.DELETE => (inet,enet); |
442 end; |
442 end; |
443 |
443 |
444 |
444 |
573 |
573 |
574 (*Calling this will generate the warning "Same as previous level" since |
574 (*Calling this will generate the warning "Same as previous level" since |
575 it affects nothing but the names of bound variables!*) |
575 it affects nothing but the names of bound variables!*) |
576 fun rename_params_tac xs i = |
576 fun rename_params_tac xs i = |
577 case Library.find_first (not o Syntax.is_identifier) xs of |
577 case Library.find_first (not o Syntax.is_identifier) xs of |
578 Some x => error ("Not an identifier: " ^ x) |
578 SOME x => error ("Not an identifier: " ^ x) |
579 | None => |
579 | NONE => |
580 (if !Logic.auto_rename |
580 (if !Logic.auto_rename |
581 then (warning "Resetting Logic.auto_rename"; |
581 then (warning "Resetting Logic.auto_rename"; |
582 Logic.auto_rename := false) |
582 Logic.auto_rename := false) |
583 else (); PRIMITIVE (rename_params_rule (xs, i))); |
583 else (); PRIMITIVE (rename_params_rule (xs, i))); |
584 |
584 |
611 (*Rotates the given subgoal to be the last.*) |
611 (*Rotates the given subgoal to be the last.*) |
612 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1); |
612 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1); |
613 |
613 |
614 (* remove premises that do not satisfy p; fails if all prems satisfy p *) |
614 (* remove premises that do not satisfy p; fails if all prems satisfy p *) |
615 fun filter_prems_tac p = |
615 fun filter_prems_tac p = |
616 let fun Then None tac = Some tac |
616 let fun Then NONE tac = SOME tac |
617 | Then (Some tac) tac' = Some(tac THEN' tac'); |
617 | Then (SOME tac) tac' = SOME(tac THEN' tac'); |
618 fun thins ((tac,n),H) = |
618 fun thins ((tac,n),H) = |
619 if p H then (tac,n+1) |
619 if p H then (tac,n+1) |
620 else (Then tac (rotate_tac n THEN' etac thin_rl),0); |
620 else (Then tac (rotate_tac n THEN' etac thin_rl),0); |
621 in SUBGOAL(fn (subg,n) => |
621 in SUBGOAL(fn (subg,n) => |
622 let val Hs = Logic.strip_assums_hyp subg |
622 let val Hs = Logic.strip_assums_hyp subg |
623 in case fst(foldl thins ((None,0),Hs)) of |
623 in case fst(foldl thins ((NONE,0),Hs)) of |
624 None => no_tac | Some tac => tac n |
624 NONE => no_tac | SOME tac => tac n |
625 end) |
625 end) |
626 end; |
626 end; |
627 |
627 |
628 |
628 |
629 (*meta-level conjunction*) |
629 (*meta-level conjunction*) |
661 val casms = map cert_safe asms; |
661 val casms = map cert_safe asms; |
662 val prems = map (norm_hhf_rule o Thm.assume) casms; |
662 val prems = map (norm_hhf_rule o Thm.assume) casms; |
663 val goal = Drule.mk_triv_goal (cert_safe prop); |
663 val goal = Drule.mk_triv_goal (cert_safe prop); |
664 |
664 |
665 val goal' = |
665 val goal' = |
666 (case Seq.pull (tac prems goal) of Some (goal', _) => goal' | _ => err "Tactic failed."); |
666 (case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed."); |
667 val ngoals = Thm.nprems_of goal'; |
667 val ngoals = Thm.nprems_of goal'; |
668 val raw_result = goal' RS Drule.rev_triv_goal; |
668 val raw_result = goal' RS Drule.rev_triv_goal; |
669 val prop' = prop_of raw_result; |
669 val prop' = prop_of raw_result; |
670 in |
670 in |
671 if ngoals <> 0 then |
671 if ngoals <> 0 then |