full_atomize;
authorwenzelm
Mon Jan 21 16:15:16 2002 +0100 (2002-01-21)
changeset 12829c92128238f85
parent 12828 57fb9d1ee34a
child 12830 c037ff3e5ddf
full_atomize;
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jan 21 15:29:06 2002 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jan 21 16:15:16 2002 +0100
     1.3 @@ -182,6 +182,12 @@
     1.4  fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
     1.5  
     1.6  
     1.7 +(* atomize rule statements *)
     1.8 +
     1.9 +fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
    1.10 +  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
    1.11 +
    1.12 +
    1.13  (* unfold intro/elim rules *)
    1.14  
    1.15  fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
    1.16 @@ -640,7 +646,7 @@
    1.17    ("intro", thms_args intro, "repeatedly apply introduction rules"),
    1.18    ("elim", thms_args elim, "repeatedly apply elimination rules"),
    1.19    ("fold", thms_args fold, "fold definitions"),
    1.20 -  ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)),
    1.21 +  ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
    1.22      "present local premises as object-level statements"),
    1.23    ("rules", rules_args rules_meth, "apply many rules, including proof search"),
    1.24    ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
     2.1 --- a/src/Pure/Isar/object_logic.ML	Mon Jan 21 15:29:06 2002 +0100
     2.2 +++ b/src/Pure/Isar/object_logic.ML	Mon Jan 21 16:15:16 2002 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4    val declare_rulify: theory attribute
     2.5    val atomize_term: Sign.sg -> term -> term
     2.6    val atomize_tac: int -> tactic
     2.7 +  val full_atomize_tac: int -> tactic
     2.8    val atomize_goal: int -> thm -> thm
     2.9    val rulify: thm -> thm
    2.10    val rulify_no_asm: thm -> thm
    2.11 @@ -135,6 +136,9 @@
    2.12      (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
    2.13    else all_tac st;
    2.14  
    2.15 +fun full_atomize_tac i st =
    2.16 +  rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
    2.17 +
    2.18  fun atomize_goal i st =
    2.19    (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
    2.20