krauss@26582: (* Title: Tools/atomize_elim.ML krauss@26582: Author: Alexander Krauss, TU Muenchen krauss@26582: krauss@26582: Turn elimination rules into atomic expressions in the object logic. krauss@26582: *) krauss@26582: krauss@26582: signature ATOMIZE_ELIM = krauss@26582: sig krauss@27571: val atomize_elim_conv : Proof.context -> conv krauss@27571: val full_atomize_elim_conv : Proof.context -> conv krauss@26582: val atomize_elim_tac : Proof.context -> int -> tactic krauss@26582: end krauss@26582: wenzelm@57948: structure Atomize_Elim : ATOMIZE_ELIM = krauss@26582: struct krauss@26582: wenzelm@57949: (* atomize_elim rules *) wenzelm@31902: wenzelm@57949: val named_theorems = wenzelm@57949: Context.>>> (Context.map_theory_result wenzelm@57949: (Named_Target.theory_init #> wenzelm@67149: Named_Theorems.declare \<^binding>\atomize_elim\ "atomize_elim rewrite rule" ##> wenzelm@57949: Local_Theory.exit_global)); krauss@26582: krauss@26582: krauss@26582: (* More conversions: *) krauss@26582: local open Conv in krauss@26582: krauss@26582: (* Compute inverse permutation *) krauss@26582: fun invert_perm pi = haftmann@33040: (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0))) krauss@26582: |> map_index I wenzelm@59058: |> sort (int_ord o apply2 snd) krauss@26582: |> map fst krauss@26582: krauss@26582: (* rearrange_prems as a conversion *) krauss@26582: fun rearrange_prems_conv pi ct = krauss@26582: let wenzelm@33002: val pi' = 0 :: map (Integer.add 1) pi krauss@27571: val fwd = Thm.trivial ct krauss@26582: |> Drule.rearrange_prems pi' wenzelm@59582: val back = Thm.trivial (snd (Thm.dest_implies (Thm.cprop_of fwd))) krauss@26582: |> Drule.rearrange_prems (invert_perm pi') krauss@27571: in Thm.equal_intr fwd back end krauss@26582: krauss@26582: wenzelm@57948: (* convert !!thesis. (!!x y z. ... => thesis) ==> ... krauss@26582: ==> (!!a b c. ... => thesis) krauss@26582: ==> thesis krauss@26582: krauss@26582: to krauss@26582: krauss@26582: (EX x y z. ...) | ... | (EX a b c. ...) krauss@26582: *) krauss@27571: fun atomize_elim_conv ctxt ct = wenzelm@54742: (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt wenzelm@57949: then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems) wenzelm@59970: then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct' krauss@26582: then all_conv ct' krauss@26582: else raise CTERM ("atomize_elim", [ct', ct]))) krauss@26582: ct krauss@26582: krauss@26582: krauss@26582: (* Move the thesis-quantifier inside over other quantifiers and unrelated prems *) krauss@26582: fun thesis_miniscope_conv inner_cv ctxt = krauss@26582: let krauss@26582: (* check if the outermost quantifier binds the conclusion *) wenzelm@57948: fun is_forall_thesis t = krauss@27571: case Logic.strip_assums_concl t of krauss@27571: (_ $ Bound i) => i = length (Logic.strip_params t) - 1 krauss@27571: | _ => false krauss@26582: krauss@26582: (* move unrelated assumptions out of the quantification *) krauss@26582: fun movea_conv ctxt ct = krauss@26582: let wenzelm@59582: val _ $ Abs (_, _, b) = Thm.term_of ct wenzelm@42083: val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i) krauss@26582: (Logic.strip_imp_prems b) [] krauss@26582: |> rev krauss@26582: krauss@26582: fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq) krauss@26582: then_conv (implies_concl_conv cv) krauss@26582: in krauss@26582: (forall_conv (K (rearrange_prems_conv idxs)) ctxt krauss@26582: then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt))) krauss@26582: ct krauss@26582: end krauss@26582: krauss@26582: (* move current quantifier to the right *) wenzelm@57948: fun moveq_conv ctxt = krauss@27571: (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt)) krauss@26582: else_conv (movea_conv ctxt) krauss@26582: wenzelm@57948: fun ms_conv ctxt ct = wenzelm@59582: if is_forall_thesis (Thm.term_of ct) krauss@26582: then moveq_conv ctxt ct krauss@26582: else (implies_concl_conv (ms_conv ctxt) krauss@26582: else_conv krauss@27571: (forall_conv (ms_conv o snd) ctxt)) krauss@26582: ct krauss@26582: in wenzelm@57948: ms_conv ctxt krauss@26582: end krauss@26582: krauss@27571: val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv krauss@26582: krauss@26582: end krauss@26582: krauss@26582: krauss@27571: fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => krauss@26582: let wenzelm@42361: val thy = Proof_Context.theory_of ctxt krauss@27571: val _ $ thesis = Logic.strip_assums_concl subg wenzelm@57948: krauss@26582: (* Introduce a quantifier first if the thesis is not bound *) wenzelm@57948: val quantify_thesis = krauss@26582: if is_Bound thesis then all_tac krauss@26582: else let wenzelm@59621: val cthesis = Thm.global_cterm_of thy thesis wenzelm@60801: val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis] krauss@26582: @{thm meta_spec} krauss@26582: in wenzelm@58956: compose_tac ctxt (false, rule, 1) i krauss@26582: end krauss@26582: in krauss@26582: quantify_thesis krauss@27571: THEN (CONVERSION (full_atomize_elim_conv ctxt) i) krauss@26582: end) krauss@26582: wenzelm@57948: val _ = wenzelm@57948: Theory.setup wenzelm@67149: (Method.setup \<^binding>\atomize_elim\ (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) wenzelm@57948: "convert obtains statement to atomic object logic goal") krauss@26582: krauss@26582: end