summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 26 Sep 1996 11:10:46 +0200 | |

changeset 2029 | 2fa4c4b1a7fe |

parent 2028 | 738bb98d65ec |

child 2030 | 474b3f208789 |

Generalized freeze to freeze_thaw in order to
implement defer_tac

--- a/src/Pure/tactic.ML Thu Sep 26 10:34:19 1996 +0200 +++ b/src/Pure/tactic.ML Thu Sep 26 11:10:46 1996 +0200 @@ -26,6 +26,7 @@ val compose_tac: (bool * thm * int) -> int -> tactic val cut_facts_tac: thm list -> int -> tactic val cut_inst_tac: (string*string)list -> thm -> int -> tactic + val defer_tac : int -> tactic val dmatch_tac: thm list -> int -> tactic val dresolve_tac: thm list -> int -> tactic val dres_inst_tac: (string*string)list -> thm -> int -> tactic @@ -42,7 +43,7 @@ val fold_tac: thm list -> tactic val forward_tac: thm list -> int -> tactic val forw_inst_tac: (string*string)list -> thm -> int -> tactic - val freeze: thm -> thm + val freeze_thaw: thm -> thm * (thm -> thm) val insert_tagged_brl: ('a*(bool*thm)) * (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net @@ -95,22 +96,45 @@ | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); Sequence.seqof(fn()=> seqcell)); -fun string_of (a,0) = a - | string_of (a,i) = a ^ "_" ^ string_of_int i; -(*convert all Vars in a theorem to Frees*) -fun freeze th = - let val fth = freezeT th - val {prop,sign,...} = rep_thm fth - fun mk_inst (Var(v,T)) = - (cterm_of sign (Var(v,T)), - cterm_of sign (Free(string_of v, T))) - val insts = map mk_inst (term_vars prop) - in instantiate ([],insts) fth end; +(*Convert all Vars in a theorem to Frees. Also return a function for + reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) +local + fun string_of (a,0) = a + | string_of (a,i) = a ^ "_" ^ string_of_int i; +in + fun freeze_thaw th = + let val fth = freezeT th + val {prop,sign,...} = rep_thm fth + fun mk_inst (Var(v,T)) = + (cterm_of sign (Var(v,T)), + cterm_of sign (Free(string_of v, T))) + val insts = map mk_inst (term_vars prop) + fun thaw th' = + th' |> forall_intr_list (map #2 insts) + |> forall_elim_list (map #1 insts) + in (instantiate ([],insts) fth, thaw) end; +end; + + +(*Rotates the given subgoal to be the last. Useful when re-playing + an old proof script, when the proof of an early subgoal fails. + DOES NOT WORK FOR TYPE VARIABLES.*) +fun defer_tac i state = + let val (state',thaw) = freeze_thaw state + val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) + val hyp::hyps' = drop(i-1,hyps) + in implies_intr hyp (implies_elim_list state' (map assume hyps)) + |> implies_intr_list (take(i-1,hyps) @ hyps') + |> thaw + |> Sequence.single + end + handle _ => Sequence.null; + (*Makes a rule by applying a tactic to an existing rule*) fun rule_by_tactic tac rl = - case Sequence.pull(tac (freeze (standard rl))) of + case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of None => raise THM("rule_by_tactic", 0, [rl]) | Some(rl',_) => standard rl'; @@ -234,7 +258,7 @@ terms that are substituted contain (term or type) unknowns from the goal, because it is unable to instantiate goal unknowns at the same time. - The type checker is instructed not to freezes flexible type vars that + The type checker is instructed not to freeze flexible type vars that were introduced during type inference and still remain in the term at the end. This increases flexibility but can introduce schematic type vars in goals.