1(* Title: HOL/Tools/Function/function_elims.ML 2 Author: Manuel Eberl, TU Muenchen 3 4Generate the pelims rules for a function. These are of the shape 5[|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P 6and are derived from the cases rule. There is at least one pelim rule for 7each function (cf. mutually recursive functions) 8There may be more than one pelim rule for a function in case of functions 9that return a boolean. For such a function, e.g. P x, not only the normal 10elim rule with the premise P x = z is generated, but also two additional 11elim rules with P x resp. \<not>P x as premises. 12*) 13 14signature FUNCTION_ELIMS = 15sig 16 val dest_funprop : term -> (term * term list) * term 17 val mk_partial_elim_rules : Proof.context -> 18 Function_Common.function_result -> thm list list 19end; 20 21structure Function_Elims : FUNCTION_ELIMS = 22struct 23 24(* Extract a function and its arguments from a proposition that is 25 either of the form "f x y z = ..." or, in case of function that 26 returns a boolean, "f x y z" *) 27fun dest_funprop (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (strip_comb lhs, rhs) 28 | dest_funprop (Const (\<^const_name>\<open>Not\<close>, _) $ t) = (strip_comb t, \<^term>\<open>False\<close>) 29 | dest_funprop t = (strip_comb t, \<^term>\<open>True\<close>); 30 31local 32 33fun propagate_tac ctxt i = 34 let 35 fun inspect eq = 36 (case eq of 37 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free x $ t) => 38 if Logic.occs (Free x, t) then raise Match else true 39 | Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ Free x) => 40 if Logic.occs (Free x, t) then raise Match else false 41 | _ => raise Match); 42 fun mk_eq thm = 43 (if inspect (Thm.prop_of thm) then [thm RS eq_reflection] 44 else [Thm.symmetric (thm RS eq_reflection)]) 45 handle Match => []; 46 val simpset = 47 empty_simpset ctxt 48 |> Simplifier.set_mksimps (K mk_eq); 49 in 50 asm_lr_simp_tac simpset i 51 end; 52 53val eq_boolI = @{lemma "\<And>P. P \<Longrightarrow> P = True" "\<And>P. \<not> P \<Longrightarrow> P = False" by iprover+}; 54val boolE = @{thms HOL.TrueE HOL.FalseE}; 55val boolD = @{lemma "\<And>P. True = P \<Longrightarrow> P" "\<And>P. False = P \<Longrightarrow> \<not> P" by iprover+}; 56val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}; 57 58fun bool_subst_tac ctxt = 59 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool) 60 THEN_ALL_NEW TRY o REPEAT_ALL_NEW (dresolve_tac ctxt boolD) 61 THEN_ALL_NEW TRY o REPEAT_ALL_NEW (eresolve_tac ctxt boolE); 62 63fun mk_bool_elims ctxt elim = 64 let 65 fun mk_bool_elim b = 66 elim 67 |> Thm.forall_elim b 68 |> Tactic.rule_by_tactic ctxt (distinct_subgoals_tac THEN TRY (resolve_tac ctxt eq_boolI 1)) 69 |> Tactic.rule_by_tactic ctxt (distinct_subgoals_tac THEN ALLGOALS (bool_subst_tac ctxt)); 70 in 71 map mk_bool_elim [\<^cterm>\<open>True\<close>, \<^cterm>\<open>False\<close>] 72 end; 73 74in 75 76fun mk_partial_elim_rules ctxt result = 77 let 78 val Function_Common.FunctionResult {fs, R, dom, psimps, cases, ...} = result; 79 val n_fs = length fs; 80 81 fun variant_free used_term v = 82 Free (singleton (Variable.variant_frees ctxt [used_term]) v); 83 84 fun mk_partial_elim_rule (idx, f) = 85 let 86 fun mk_funeq 0 T (acc_args, acc_lhs) = 87 let val y = variant_free acc_lhs ("y", T) 88 in (y, rev acc_args, HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))) end 89 | mk_funeq n (Type (\<^type_name>\<open>fun\<close>, [S, T])) (acc_args, acc_lhs) = 90 let val x = variant_free acc_lhs ("x", S) 91 in mk_funeq (n - 1) T (x :: acc_args, acc_lhs $ x) end 92 | mk_funeq _ _ _ = raise TERM ("Not a function", [f]); 93 94 val f_simps = 95 filter (fn r => 96 (Thm.prop_of r 97 |> Logic.strip_assums_concl 98 |> HOLogic.dest_Trueprop 99 |> dest_funprop |> fst |> fst) = f) 100 psimps; 101 102 val arity = 103 hd f_simps 104 |> Thm.prop_of 105 |> Logic.strip_assums_concl 106 |> HOLogic.dest_Trueprop 107 |> snd o fst o dest_funprop 108 |> length; 109 110 val (rhs_var, arg_vars, prop) = mk_funeq arity (fastype_of f) ([], f); 111 val args = HOLogic.mk_tuple arg_vars; 112 val domT = R |> dest_Free |> snd |> hd o snd o dest_Type; 113 114 val P = Thm.cterm_of ctxt (variant_free prop ("P", \<^typ>\<open>bool\<close>)); 115 val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args; 116 117 val cprop = Thm.cterm_of ctxt prop; 118 119 val asms = [cprop, Thm.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; 120 val asms_thms = map Thm.assume asms; 121 122 val prep_subgoal_tac = 123 TRY o REPEAT_ALL_NEW (eresolve_tac ctxt @{thms Pair_inject}) 124 THEN' Method.insert_tac ctxt 125 (case asms_thms of thm :: thms => (thm RS sym) :: thms) 126 THEN' propagate_tac ctxt 127 THEN_ALL_NEW 128 ((TRY o (EqSubst.eqsubst_asm_tac ctxt [1] psimps THEN' assume_tac ctxt))) 129 THEN_ALL_NEW bool_subst_tac ctxt; 130 131 val elim_stripped = 132 nth cases idx 133 |> Thm.forall_elim P 134 |> Thm.forall_elim (Thm.cterm_of ctxt args) 135 |> Tactic.rule_by_tactic ctxt (distinct_subgoals_tac THEN ALLGOALS prep_subgoal_tac) 136 |> fold_rev Thm.implies_intr asms 137 |> Thm.forall_intr (Thm.cterm_of ctxt rhs_var); 138 139 val bool_elims = 140 if fastype_of rhs_var = \<^typ>\<open>bool\<close> 141 then mk_bool_elims ctxt elim_stripped 142 else []; 143 144 fun unstrip rl = 145 rl 146 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars 147 |> Thm.forall_intr P 148 in 149 map unstrip (elim_stripped :: bool_elims) 150 end; 151 in 152 map_index mk_partial_elim_rule fs 153 end; 154 155end; 156 157end; 158