46 val flexflex_tac : tactic |
46 val flexflex_tac : tactic |
47 val fold_goals_tac : thm list -> tactic |
47 val fold_goals_tac : thm list -> tactic |
48 val fold_tac : thm list -> tactic |
48 val fold_tac : thm list -> tactic |
49 val forward_tac : thm list -> int -> tactic |
49 val forward_tac : thm list -> int -> tactic |
50 val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
50 val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
51 val freeze_thaw : thm -> thm * (thm -> thm) |
|
52 val insert_tagged_brl : ('a*(bool*thm)) * |
51 val insert_tagged_brl : ('a*(bool*thm)) * |
53 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
52 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
54 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
53 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
55 val delete_tagged_brl : (bool*thm) * |
54 val delete_tagged_brl : (bool*thm) * |
56 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
55 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
103 None => Seq.empty |
102 None => Seq.empty |
104 | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); |
103 | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); |
105 Seq.make(fn()=> seqcell)); |
104 Seq.make(fn()=> seqcell)); |
106 |
105 |
107 |
106 |
108 (*Convert all Vars in a theorem to Frees. Also return a function for |
|
109 reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. |
|
110 Similar code in type/freeze_thaw*) |
|
111 fun freeze_thaw th = |
|
112 let val fth = freezeT th |
|
113 val {prop,sign,...} = rep_thm fth |
|
114 val used = add_term_names (prop, []) |
|
115 and vars = term_vars prop |
|
116 fun newName (Var(ix,_), (pairs,used)) = |
|
117 let val v = variant used (string_of_indexname ix) |
|
118 in ((ix,v)::pairs, v::used) end; |
|
119 val (alist, _) = foldr newName (vars, ([], used)) |
|
120 fun mk_inst (Var(v,T)) = |
|
121 (cterm_of sign (Var(v,T)), |
|
122 cterm_of sign (Free(the (assoc(alist,v)), T))) |
|
123 val insts = map mk_inst vars |
|
124 fun thaw th' = |
|
125 th' |> forall_intr_list (map #2 insts) |
|
126 |> forall_elim_list (map #1 insts) |
|
127 in (instantiate ([],insts) fth, thaw) end; |
|
128 |
|
129 |
|
130 (*Rotates the given subgoal to be the last. Useful when re-playing |
107 (*Rotates the given subgoal to be the last. Useful when re-playing |
131 an old proof script, when the proof of an early subgoal fails. |
108 an old proof script, when the proof of an early subgoal fails. |
132 DOES NOT WORK FOR TYPE VARIABLES.*) |
109 DOES NOT WORK FOR TYPE VARIABLES. |
|
110 Similar to drule/rotate_prems*) |
133 fun defer_tac i state = |
111 fun defer_tac i state = |
134 let val (state',thaw) = freeze_thaw state |
112 let val (state',thaw) = freeze_thaw state |
135 val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) |
113 val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) |
136 val hyp::hyps' = List.drop(hyps, i-1) |
114 val hyp::hyps' = List.drop(hyps, i-1) |
137 in implies_intr hyp (implies_elim_list state' (map assume hyps)) |
115 in implies_intr hyp (implies_elim_list state' (map assume hyps)) |