# HG changeset patch # User noschinl # Date 1378457800 -7200 # Node ID 92db671e0ac6d4393a25137ae20244e3735b9fe8 # Parent a1a78a2716822cd62edad2adef818f3f286e276a added simps_of_case and case_of_simps to convert between simps and case rules diff -r a1a78a271682 -r 92db671e0ac6 src/HOL/Library/Simps_Case_Conv.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Simps_Case_Conv.thy Fri Sep 06 10:56:40 2013 +0200 @@ -0,0 +1,12 @@ +(* Title: HOL/Library/Simps_Case_Conv.thy + Author: Lars Noschinski +*) + +theory Simps_Case_Conv + imports Main + keywords "simps_of_case" "case_of_simps" :: thy_decl +begin + +ML_file "simps_case_conv.ML" + +end diff -r a1a78a271682 -r 92db671e0ac6 src/HOL/Library/simps_case_conv.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/simps_case_conv.ML Fri Sep 06 10:56:40 2013 +0200 @@ -0,0 +1,202 @@ +(* Title: HOL/Library/simps_case_conv.ML + Author: Lars Noschinski, TU Muenchen + Gerwin Klein, NICTA + + Converts function specifications between the representation as + a list of equations (with patterns on the lhs) and a single + equation (with a nested case expression on the rhs). +*) + +signature SIMPS_CASE_CONV = +sig + val to_case: Proof.context -> thm list -> thm + val gen_to_simps: Proof.context -> thm list -> thm -> thm list + val to_simps: Proof.context -> thm -> thm list +end + +structure Simps_Case_Conv: SIMPS_CASE_CONV = +struct + +(* Collects all type constructors in a type *) +fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts + | collect_Tcons (TFree _) = [] + | collect_Tcons (TVar _) = [] + +fun get_split_ths thy = collect_Tcons + #> distinct (op =) + #> map_filter (Datatype_Data.get_info thy) + #> map #split + +val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq + + +local + +(*Creates free variables for a list of types*) +fun mk_Frees Ts ctxt = + let + val (names,ctxt') = Variable.variant_fixes (replicate (length Ts) "x") ctxt + val ts = map Free (names ~~ Ts) + in (ts, ctxt') end + +fun tac ctxt {splits, intros, defs} = + let val ctxt' = Classical.addSIs (ctxt, intros) in + REPEAT_DETERM1 (FIRSTGOAL (split_tac splits)) + THEN Local_Defs.unfold_tac ctxt defs + THEN safe_tac ctxt' + end + +fun import [] ctxt = ([], ctxt) + | import (thm :: thms) ctxt = + let + val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term + #> Thm.cterm_of (Proof_Context.theory_of ctxt) + val ct = fun_ct thm + val cts = map fun_ct thms + val pairs = map (fn s => (s,ct)) cts + val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs) + in Variable.import true (thm :: thms') ctxt |> apfst snd end + +in + +(* + For a list + f p_11 ... p_1n = t1 + f p_21 ... p_2n = t2 + ... + f p_mn ... p_mn = tm + of theorems, prove a single theorem + f x1 ... xn = t + where t is a (nested) case expression. The terms p_11, ..., p_mn must + be exhaustive, non-overlapping datatype patterns. f must not be a function + application. +*) +fun to_case ctxt ths = + let + val (iths, ctxt') = import ths ctxt + val (fun_t, arg_ts) = hd iths |> strip_eq |> fst |> strip_comb + val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths + val (arg_Frees, ctxt'') = mk_Frees (map fastype_of arg_ts) ctxt' + + fun hide_rhs ((pat, rhs), name) lthy = let + val frees = fold Term.add_frees pat [] + val abs_rhs = fold absfree frees rhs + val ((f,def), lthy') = Local_Defs.add_def + ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy + in ((list_comb (f, map Free (rev frees)), def), lthy') end + + val ((def_ts, def_thms), ctxt3) = let + val nctxt = Variable.names_of ctxt'' + val names = Name.invent nctxt "rhs" (length eqs) + in fold_map hide_rhs (eqs ~~ names) ctxt'' |> apfst split_list end + + val (cases, split_thms) = + let + val pattern = map (fst #> HOLogic.mk_tuple) eqs + val case_arg = HOLogic.mk_tuple arg_Frees + val cases = Case_Translation.make_case ctxt Case_Translation.Warning Name.context + case_arg (pattern ~~ def_ts) + val split_thms = get_split_ths (Proof_Context.theory_of ctxt3) (fastype_of case_arg) + in (cases, split_thms) end + + val t = (list_comb (fun_t, arg_Frees), cases) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} => + tac ctxt {splits=split_thms, intros=ths, defs=def_thms}) + in th + |> singleton (Proof_Context.export ctxt3 ctxt) + |> Goal.norm_result + end + +end + +local + +fun was_split t = + let + val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq + o fst o HOLogic.dest_imp + val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop + fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t + | dest_alls t = t + in forall (is_free_eq_imp o dest_alls) (get_conjs t) end + handle TERM _ => false + +fun apply_split ctxt split thm = Seq.of_list + let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in + (Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split])) + end + +fun forward_tac rules t = Seq.of_list ([t] RL rules) + +val refl_imp = refl RSN (2, mp) + +val get_rules_once_split = + REPEAT (forward_tac [conjunct1, conjunct2]) + THEN REPEAT (forward_tac [spec]) + THEN (forward_tac [refl_imp]) + +fun do_split ctxt split = + let + val split' = split RS iffD1; + val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt)))) + in if was_split split_rhs + then DETERM (apply_split ctxt split') THEN get_rules_once_split + else raise TERM ("malformed split rule", [split_rhs]) + end + +val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq] + +in + +fun gen_to_simps ctxt splitthms thm = + Seq.list_of ((TRY atomize_meta_eq + THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm) + +fun to_simps ctxt thm = + let + val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of + val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T + in gen_to_simps ctxt splitthms thm end + + +end + +fun case_of_simps_cmd (bind, thms_ref) lthy = + let + val thy = Proof_Context.theory_of lthy + val bind' = apsnd (map (Attrib.intern_src thy)) bind + val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy + in + Local_Theory.note (bind', [thm]) lthy |> snd + end + +fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy = + let + val thy = Proof_Context.theory_of lthy + val bind' = apsnd (map (Attrib.intern_src thy)) bind + val thm = singleton (Attrib.eval_thms lthy) thm_ref + val simps = if null splits_ref + then to_simps lthy thm + else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm + in + Local_Theory.note (bind', simps) lthy |> snd + end + +val _ = + Outer_Syntax.local_theory @{command_spec "case_of_simps"} + "turns a list of equations into a case expression" + (Parse_Spec.opt_thm_name ":" -- Parse_Spec.xthms1 >> case_of_simps_cmd) + +val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |-- + Parse_Spec.xthms1 --| @{keyword ")"} + +val _ = + Outer_Syntax.local_theory @{command_spec "simps_of_case"} + "perform case split on rule" + (Parse_Spec.opt_thm_name ":" -- Parse_Spec.xthm -- + Scan.optional parse_splits [] >> simps_of_case_cmd) + +end +