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/lib/cases.ML | |
parent | 8885f9c96d950655250292ee03b54aafeb2f727f (diff) |
reorganize
Diffstat (limited to 'spartan/core/lib/cases.ML')
-rw-r--r-- | spartan/core/lib/cases.ML | 42 |
1 files changed, 0 insertions, 42 deletions
diff --git a/spartan/core/lib/cases.ML b/spartan/core/lib/cases.ML deleted file mode 100644 index 560a9f1..0000000 --- a/spartan/core/lib/cases.ML +++ /dev/null @@ -1,42 +0,0 @@ -(* Title: cases.ML - Author: Joshua Chen - -Case reasoning. -*) - -structure Case: sig - -val rules: Proof.context -> thm list -val lookup_rule: Proof.context -> Termtab.key -> thm option -val register_rule: thm -> Context.generic -> Context.generic - -end = struct - -(* Context 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 Termtab.table - val empty = Termtab.empty - val extend = I - val merge = Termtab.merge Thm.eq_thm_prop -) - -val rules = map #2 o Termtab.dest o Rules.get o Context.Proof -fun lookup_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt)) -fun register_rule rl = - let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl)) - in Rules.map (Termtab.update (hd, rl)) end - - -(* [cases] attribute *) -val _ = Theory.setup ( - Attrib.setup \<^binding>\<open>cases\<close> - (Scan.succeed (Thm.declaration_attribute register_rule)) - "" - #> Global_Theory.add_thms_dynamic (\<^binding>\<open>cases\<close>, rules o Context.proof_of) -) - - -end |