1(* Title: HOL/Tools/split_rule.ML 2 Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen 3 4Some tools for managing tupled arguments and abstractions in rules. 5*) 6 7signature SPLIT_RULE = 8sig 9 val split_rule_var: Proof.context -> term -> thm -> thm 10 val split_rule: Proof.context -> thm -> thm 11 val complete_split_rule: Proof.context -> thm -> thm 12end; 13 14structure Split_Rule: SPLIT_RULE = 15struct 16 17(** split rules **) 18 19fun internal_case_prod_const (Ta, Tb, Tc) = 20 Const (\<^const_name>\<open>Product_Type.internal_case_prod\<close>, 21 [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); 22 23fun eval_internal_split ctxt = 24 hol_simplify ctxt @{thms internal_case_prod_def} o 25 hol_simplify ctxt @{thms internal_case_prod_conv}; 26 27fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt; 28 29 30(*In ap_split S T u, term u expects separate arguments for the factors of S, 31 with result type T. The call creates a new term expecting one argument 32 of type S.*) 33fun ap_split (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) T3 u = 34 internal_case_prod_const (T1, T2, T3) $ 35 Abs ("v", T1, 36 ap_split T2 T3 37 ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $ 38 Bound 0)) 39 | ap_split _ T3 u = u; 40 41(*Curries any Var of function type in the rule*) 42fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl = 43 let val T' = HOLogic.flatten_tupleT T1 ---> T2; 44 val newt = ap_split T1 T2 (Var (v, T')); 45 in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end 46 | split_rule_var' _ _ rl = rl; 47 48 49(* complete splitting of partially split rules *) 50 51fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U 52 (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U) 53 (incr_boundvars 1 u) $ Bound 0)) 54 | ap_split' _ _ u = u; 55 56fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) = 57 let 58 val (Us', U') = strip_type T; 59 val Us = take (length ts) Us'; 60 val U = drop (length ts) Us' ---> U'; 61 val T' = maps HOLogic.flatten_tupleT Us ---> U; 62 fun mk_tuple (v as Var ((a, _), T)) (xs, insts) = 63 let 64 val Ts = HOLogic.flatten_tupleT T; 65 val ys = Name.variant_list xs (replicate (length Ts) a); 66 in 67 (xs @ ys, 68 (dest_Var v, 69 Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T 70 (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts) 71 end 72 | mk_tuple _ x = x; 73 val newt = ap_split' Us U (Var (v, T')); 74 val (vs', insts) = fold mk_tuple ts (vs, []); 75 in 76 (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs') 77 end 78 | complete_split_rule_var _ _ x = x; 79 80fun collect_vars (Abs (_, _, t)) = collect_vars t 81 | collect_vars t = 82 (case strip_comb t of 83 (v as Var _, ts) => cons (v, ts) 84 | (_, ts) => fold collect_vars ts); 85 86 87fun split_rule_var ctxt = 88 (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt; 89 90(*curries ALL function variables occurring in a rule's conclusion*) 91fun split_rule ctxt rl = 92 fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl 93 |> remove_internal_split ctxt 94 |> Drule.export_without_context; 95 96(*curries ALL function variables*) 97fun complete_split_rule ctxt rl = 98 let 99 val prop = Thm.prop_of rl; 100 val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop []; 101 val vars = collect_vars prop []; 102 in 103 fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs)) 104 |> remove_internal_split ctxt 105 |> Drule.export_without_context 106 |> Rule_Cases.save rl 107 end; 108 109 110(* attribute syntax *) 111 112val _ = 113 Theory.setup 114 (Attrib.setup \<^binding>\<open>split_format\<close> 115 (Scan.lift (Args.parens (Args.$$$ "complete") 116 >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of)))) 117 "split pair-typed subterms in premises, or function arguments" #> 118 Attrib.setup \<^binding>\<open>split_rule\<close> 119 (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of))) 120 "curries ALL function variables occurring in a rule's conclusion"); 121 122end; 123 124