Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
authorballarin
Mon Feb 15 01:34:08 2010 +0100 (2010-02-15)
changeset 360930880493627ca
parent 36092 8f1e60d9f7cc
child 36094 eb1cc37bc8db
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
NEWS
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
     1.1 --- a/NEWS	Mon Feb 15 01:27:06 2010 +0100
     1.2 +++ b/NEWS	Mon Feb 15 01:34:08 2010 +0100
     1.3 @@ -9,6 +9,8 @@
     1.4  * Code generator: details of internal data cache have no impact on
     1.5  the user space functionality any longer.
     1.6  
     1.7 +* Methods unfold_locales and intro_locales ignore non-locale subgoals.  This
     1.8 +is more appropriate for interpretations with 'where'.  INCOMPATIBILITY.
     1.9  
    1.10  *** HOL ***
    1.11  
     2.1 --- a/src/Pure/Isar/locale.ML	Mon Feb 15 01:27:06 2010 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Mon Feb 15 01:34:08 2010 +0100
     2.3 @@ -566,15 +566,22 @@
     2.4  
     2.5  
     2.6  (* Tactic *)
     2.7 +fun intros_tac intros facts =
     2.8 +  (TRYALL (Method.insert_tac facts THEN'
     2.9 +      REPEAT_ALL_NEW (resolve_tac intros)) |> CHANGED)
    2.10 +    THEN Tactic.distinct_subgoals_tac;
    2.11  
    2.12 -fun intro_locales_tac eager ctxt =
    2.13 -  Method.intros_tac
    2.14 +fun gen_intro_locales_tac intros_tac eager ctxt =
    2.15 +  intros_tac
    2.16      (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
    2.17  
    2.18 +val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
    2.19 +val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
    2.20 +
    2.21  val _ = Context.>> (Context.map_theory
    2.22 - (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
    2.23 + (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
    2.24      "back-chain introduction rules of locales without unfolding predicates" #>
    2.25 -  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
    2.26 +  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
    2.27      "back-chain all introduction rules of locales"));
    2.28  
    2.29  end;
     3.1 --- a/src/Pure/Isar/method.ML	Mon Feb 15 01:27:06 2010 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Mon Feb 15 01:34:08 2010 +0100
     3.3 @@ -46,6 +46,7 @@
     3.4    val rule_tac: thm list -> thm list -> int -> tactic
     3.5    val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
     3.6    val intros_tac: thm list -> thm list -> tactic
     3.7 +  val try_intros_tac: thm list -> thm list -> tactic
     3.8    val rule: thm list -> method
     3.9    val erule: int -> thm list -> method
    3.10    val drule: int -> thm list -> method
    3.11 @@ -262,11 +263,13 @@
    3.12  
    3.13  (* intros_tac -- pervasive search spanned by intro rules *)
    3.14  
    3.15 -fun intros_tac intros facts =
    3.16 -  ALLGOALS (insert_tac facts THEN'
    3.17 +fun gen_intros_tac goals intros facts =
    3.18 +  goals (insert_tac facts THEN'
    3.19        REPEAT_ALL_NEW (resolve_tac intros))
    3.20      THEN Tactic.distinct_subgoals_tac;
    3.21  
    3.22 +val intros_tac = gen_intros_tac ALLGOALS;
    3.23 +val try_intros_tac = gen_intros_tac TRYALL;
    3.24  
    3.25  (* ML tactics *)
    3.26