diff options
author | Josh Chen | 2020-06-19 12:41:54 +0200 |
---|---|---|
committer | Josh Chen | 2020-06-19 12:41:54 +0200 |
commit | 4f147cba894baa9e372e2b67211140b1a6f7b16c (patch) | |
tree | 68cf6b9e9e73955b1831f4529834bdaf04ac1ceb /spartan/core/elimination.ML | |
parent | 8885f9c96d950655250292ee03b54aafeb2f727f (diff) |
reorganize
Diffstat (limited to 'spartan/core/elimination.ML')
-rw-r--r-- | spartan/core/elimination.ML | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML new file mode 100644 index 0000000..11b3af9 --- /dev/null +++ b/spartan/core/elimination.ML @@ -0,0 +1,48 @@ +(* Title: elimination.ML + Author: Joshua Chen + +Type elimination setup. +*) + +structure Elim: sig + +val Rules: Proof.context -> (thm * indexname list) Termtab.table +val rules: Proof.context -> (thm * indexname list) list +val lookup_rule: Proof.context -> Termtab.key -> (thm * indexname list) option +val register_rule: term list -> thm -> Context.generic -> Context.generic + +end = struct + +(** Context data **) + +(* Elimination rule data *) + +(*Stores elimination rules together with a list of the indexnames of the + variables each rule eliminates. Keyed by head of the type being eliminated.*) +structure Rules = Generic_Data ( + type T = (thm * indexname list) Termtab.table + val empty = Termtab.empty + val extend = I + val merge = Termtab.merge (eq_fst Thm.eq_thm_prop) +) + +val Rules = Rules.get o Context.Proof +fun rules ctxt = map (op #2) (Termtab.dest (Rules ctxt)) +fun lookup_rule ctxt = Termtab.lookup (Rules ctxt) +fun register_rule tms rl = + let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl)) + in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end + + +(* [elims] attribute *) +val _ = Theory.setup ( + Attrib.setup \<^binding>\<open>elims\<close> + (Scan.repeat Args.term_pattern >> + (Thm.declaration_attribute o register_rule)) + "" + #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>, + fn context => (map #1 (rules (Context.proof_of context)))) +) + + +end |