Structure match_goal
signature match_goal =
sig
include Abbrev
datatype name =
Assumption of string option
| Conclusion
| Anything
type pattern = term quotation
type matcher = name * pattern * bool (* whole term? *)
(*
semantics of names:
Assumption (SOME s)
- must be an assumption
- must be the same as any other assumptions called s
- must be different from any other assumptions not called s
Assumption NONE
- must be an assumption
Conclusion
- must be the conclusion
Anything
(no constraints)
*)
(*
semantics of whole term boolean:
- if true then the match must be of the whole assumption/conclusion
- otherwise, match any subterm (i.e., like Coq's context patterns)
*)
(*
semantics of pattern variables:
2 kinds of variable:
- free variable in goal
- unification variable
- by convention, must end, and not start, with an underscore
assume all free variables cannot be mistaken for unification variables
(if attempting to bind a non-unification variable, the match will fail)
*)
(*
semantics of matcher list with a tactic (match_case):
Iterate over matchers, all must match:
1. Parse quotation in context of goal (and check no free vars ending with _)
2. Attempt to match the appropriate part of the goal with the pattern (keep track which match)
- if failed, backtrack within current matcher;
- if no assumptions match, backtrack to previous matcher
3. Go to the next matcher
4. When all matchers are done:
- Introduce abbreviations for all unification variables
- Try running the tactic
- if it fails: undo abbreviations, backtrack
- if it succeeds: undo abbreviations, done
semantics of (matcher list * thms_tactic) list:
Iterate over list, taking first thing that works.
*)
type mg_tactic = (string -> thm) * (string -> term) -> tactic
val match1_tac : matcher * mg_tactic -> tactic
val match_tac : matcher list * mg_tactic -> tactic
val first_match_tac : (matcher list * mg_tactic) list -> tactic
(* TODO: maybe these should be elsewhere *)
val kill_asm : thm -> tactic
val drule_thm : thm -> thm -> tactic
(* -- *)
structure mg : sig
(* name and match whole assumption *)
val a : string -> pattern -> matcher
(* match whole assumption *)
val ua : pattern -> matcher
val au : pattern -> matcher
(* name and match assumption subterm *)
val ab : string -> pattern -> matcher
val ba : string -> pattern -> matcher
(* match assumption subterm *)
val uab : pattern -> matcher
val uba : pattern -> matcher
val aub : pattern -> matcher
val abu : pattern -> matcher
val bau : pattern -> matcher
val bua : pattern -> matcher
(* match whole conclusion *)
val c : pattern -> matcher
(* match conclusion subterm *)
val cb : pattern -> matcher
val bc : pattern -> matcher
(* match whole assumption or conclusion *)
val ac : pattern -> matcher
val ca : pattern -> matcher
(* match assumption or conclusion subterm *)
val acb : pattern -> matcher
val abc : pattern -> matcher
val bca : pattern -> matcher
val cba : pattern -> matcher
val cab : pattern -> matcher
val bac : pattern -> matcher
end
end
HOL 4, Kananaskis-13