moved rulify to ObjectLogic;
authorwenzelm
Sun Oct 14 22:08:29 2001 +0200 (2001-10-14 ago)
changeset 11770b6bb7a853dd2
parent 11769 1fcf1eb51608
child 11771 b7b100a2de1d
moved rulify to ObjectLogic;
src/HOL/Finite.ML
src/HOL/HOL.thy
src/HOL/Integ/IntArith.ML
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/ROOT.ML
src/HOL/Set.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Typedef.thy
src/Pure/Isar/attrib.ML
src/Pure/object_logic.ML
src/ZF/ZF.ML
src/ZF/upair.thy
     1.1 --- a/src/HOL/Finite.ML	Sun Oct 14 22:07:01 2001 +0200
     1.2 +++ b/src/HOL/Finite.ML	Sun Oct 14 22:08:29 2001 +0200
     1.3 @@ -598,7 +598,7 @@
     1.4  
     1.5  
     1.6  Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
     1.7 -by (blast_tac (claset() addIs [rulify lemma]) 1);
     1.8 +by (blast_tac (claset() addIs [ObjectLogic.rulify lemma]) 1);
     1.9  qed "foldSet_determ";
    1.10  
    1.11  Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
     2.1 --- a/src/HOL/HOL.thy	Sun Oct 14 22:07:01 2001 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Oct 14 22:08:29 2001 +0200
     2.3 @@ -237,6 +237,7 @@
     2.4  
     2.5  use "cladata.ML"
     2.6  setup hypsubst_setup
     2.7 +declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
     2.8  setup Classical.setup
     2.9  setup clasetup
    2.10  
     3.1 --- a/src/HOL/Integ/IntArith.ML	Sun Oct 14 22:07:01 2001 +0200
     3.2 +++ b/src/HOL/Integ/IntArith.ML	Sun Oct 14 22:08:29 2001 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  by(blast_tac (claset() addIs [le_SucI]) 1);
     3.5  val lemma = result();
     3.6  
     3.7 -bind_thm("nat0_intermed_int_val", rulify_no_asm lemma);
     3.8 +bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
     3.9  
    3.10  Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= Numeral1; m < n; \
    3.11  \        f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
     4.1 --- a/src/HOL/IsaMakefile	Sun Oct 14 22:07:01 2001 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Sun Oct 14 22:08:29 2001 +0200
     4.3 @@ -73,9 +73,9 @@
     4.4    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
     4.5    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     4.6    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
     4.7 -  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/rulify.ML \
     4.8 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML \
     4.9 -  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
    4.10 +  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
    4.11 +  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
    4.12 +  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
    4.13    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    4.14    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
    4.15    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
     5.1 --- a/src/HOL/List.ML	Sun Oct 14 22:07:01 2001 +0200
     5.2 +++ b/src/HOL/List.ML	Sun Oct 14 22:08:29 2001 +0200
     5.3 @@ -413,7 +413,7 @@
     5.4  by Auto_tac;
     5.5  qed "rev_exhaust_aux";
     5.6  
     5.7 -bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
     5.8 +bind_thm ("rev_exhaust", ObjectLogic.rulify rev_exhaust_aux);
     5.9  
    5.10  
    5.11  (** set **)
     6.1 --- a/src/HOL/ROOT.ML	Sun Oct 14 22:07:01 2001 +0200
     6.2 +++ b/src/HOL/ROOT.ML	Sun Oct 14 22:08:29 2001 +0200
     6.3 @@ -20,7 +20,6 @@
     6.4  use "~~/src/Provers/split_paired_all.ML";
     6.5  use "~~/src/Provers/splitter.ML";
     6.6  use "~~/src/Provers/hypsubst.ML";
     6.7 -use "~~/src/Provers/rulify.ML";
     6.8  use "~~/src/Provers/induct_method.ML";
     6.9  use "~~/src/Provers/make_elim.ML";
    6.10  use "~~/src/Provers/classical.ML";
     7.1 --- a/src/HOL/Set.ML	Sun Oct 14 22:07:01 2001 +0200
     7.2 +++ b/src/HOL/Set.ML	Sun Oct 14 22:08:29 2001 +0200
     7.3 @@ -840,23 +840,6 @@
     7.4  by (Blast_tac 1);
     7.5  qed "psubset_imp_ex_mem";
     7.6  
     7.7 -
     7.8 -(* rulify setup *)
     7.9 -
    7.10  Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
    7.11  by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
    7.12  qed "atomize_ball";
    7.13 -
    7.14 -local
    7.15 -  val ss = HOL_basic_ss addsimps
    7.16 -    [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
    7.17 -in
    7.18 -
    7.19 -structure Rulify = RulifyFun
    7.20 - (val make_meta = Simplifier.simplify ss
    7.21 -  val full_make_meta = Simplifier.full_simplify ss);
    7.22 -
    7.23 -structure BasicRulify: BASIC_RULIFY = Rulify;
    7.24 -open BasicRulify;
    7.25 -
    7.26 -end;
     8.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Oct 14 22:07:01 2001 +0200
     8.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Oct 14 22:08:29 2001 +0200
     8.3 @@ -295,7 +295,7 @@
     8.4  val all_not_allowed = 
     8.5      "Introduction rule must not have a leading \"!!\" quantifier";
     8.6  
     8.7 -val atomize_cterm = full_rewrite_cterm inductive_atomize;
     8.8 +val atomize_cterm = rewrite_cterm true inductive_atomize;
     8.9  
    8.10  in
    8.11  
     9.1 --- a/src/HOL/Typedef.thy	Sun Oct 14 22:07:01 2001 +0200
     9.2 +++ b/src/HOL/Typedef.thy	Sun Oct 14 22:08:29 2001 +0200
     9.3 @@ -8,6 +8,9 @@
     9.4  theory Typedef = Set
     9.5  files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
     9.6  
     9.7 +(*belongs to theory Set*)
     9.8 +declare atomize_ball [symmetric, rulify]
     9.9 +
    9.10  (* Courtesy of Stephan Merz *)
    9.11  lemma Least_mono: 
    9.12    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    9.13 @@ -20,10 +23,6 @@
    9.14    done
    9.15  
    9.16  
    9.17 -(*belongs to theory Set*)
    9.18 -setup Rulify.setup
    9.19 -
    9.20 -
    9.21  subsection {* HOL type definitions *}
    9.22  
    9.23  constdefs
    10.1 --- a/src/Pure/Isar/attrib.ML	Sun Oct 14 22:07:01 2001 +0200
    10.2 +++ b/src/Pure/Isar/attrib.ML	Sun Oct 14 22:08:29 2001 +0200
    10.3 @@ -278,6 +278,13 @@
    10.4  fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
    10.5  
    10.6  
    10.7 +(* rule_format *)
    10.8 +
    10.9 +fun rule_format_att x = syntax
   10.10 +  (Scan.lift (Args.parens (Args.$$$ "no_asm")
   10.11 +  >> K ObjectLogic.rule_format_no_asm || Scan.succeed ObjectLogic.rule_format)) x;
   10.12 +
   10.13 +
   10.14  (* misc rules *)
   10.15  
   10.16  fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
   10.17 @@ -288,6 +295,7 @@
   10.18  fun exported_local x = no_args (Drule.rule_attribute Proof.export_thm) x;
   10.19  
   10.20  
   10.21 +
   10.22  (** theory setup **)
   10.23  
   10.24  (* pure_attributes *)
   10.25 @@ -309,8 +317,11 @@
   10.26    ("case_names", (case_names, case_names), "named rule cases"),
   10.27    ("params", (params, params), "named rule parameters"),
   10.28    ("exported", (exported_global, exported_local), "theorem exported from context"),
   10.29 -  ("atomize", (no_args ObjectLogic.atomize, no_args undef_local_attribute),
   10.30 -    "declaration of atomize rule")];
   10.31 +  ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
   10.32 +    "declaration of atomize rule"),
   10.33 +  ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
   10.34 +    "declaration of rulify rule"),
   10.35 +  ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")];
   10.36  
   10.37  
   10.38  (* setup *)
    11.1 --- a/src/Pure/object_logic.ML	Sun Oct 14 22:07:01 2001 +0200
    11.2 +++ b/src/Pure/object_logic.ML	Sun Oct 14 22:08:29 2001 +0200
    11.3 @@ -14,9 +14,14 @@
    11.4    val is_judgment: Sign.sg -> term -> bool
    11.5    val drop_judgment: Sign.sg -> term -> term
    11.6    val fixed_judgment: Sign.sg -> string -> term
    11.7 -  val atomize: theory attribute
    11.8 +  val declare_atomize: theory attribute
    11.9 +  val declare_rulify: theory attribute
   11.10    val atomize_tac: int -> tactic
   11.11    val atomize_goal: int -> thm -> thm
   11.12 +  val rulify: thm -> thm
   11.13 +  val rulify_no_asm: thm -> thm
   11.14 +  val rule_format: 'a attribute
   11.15 +  val rule_format_no_asm: 'a attribute
   11.16    val setup: (theory -> theory) list
   11.17  end;
   11.18  
   11.19 @@ -31,9 +36,9 @@
   11.20  structure ObjectLogicDataArgs =
   11.21  struct
   11.22    val name = "Pure/object-logic";
   11.23 -  type T = string option * thm list;
   11.24 +  type T = string option * (thm list * thm list);
   11.25  
   11.26 -  val empty = (None, []);
   11.27 +  val empty = (None, ([], [Drule.norm_hhf_eq]));
   11.28    val copy = I;
   11.29    val prep_ext = I;
   11.30  
   11.31 @@ -41,8 +46,9 @@
   11.32          if x = y then Some x else error "Attempt to merge different object-logics"
   11.33      | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
   11.34  
   11.35 -  fun merge ((judgment1, atomize1), (judgment2, atomize2)) =
   11.36 -    (merge_judgment (judgment1, judgment2), Drule.merge_rules (atomize1, atomize2));
   11.37 +  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
   11.38 +    (merge_judgment (judgment1, judgment2),
   11.39 +      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
   11.40  
   11.41    fun print _ _ = ();
   11.42  end;
   11.43 @@ -72,7 +78,6 @@
   11.44  end;
   11.45  
   11.46  
   11.47 -
   11.48  (* term operations *)
   11.49  
   11.50  fun judgment_name sg =
   11.51 @@ -99,32 +104,49 @@
   11.52  
   11.53  
   11.54  
   11.55 -(** atomize meta-level connectives **)
   11.56 +(** treatment of meta-level connectives **)
   11.57  
   11.58  (* maintain rules *)
   11.59  
   11.60 -val get_atomize_sg = #2 o ObjectLogicData.get_sg;
   11.61 +val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
   11.62 +val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
   11.63  
   11.64 -val add_atomize = ObjectLogicData.map o Library.apsnd o Drule.add_rules;
   11.65 -fun atomize (thy, th) = (add_atomize [th] thy, th);
   11.66 +val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
   11.67 +val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
   11.68 +
   11.69 +fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
   11.70 +fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
   11.71  
   11.72  
   11.73 -(* tactics *)
   11.74 +(* atomize *)
   11.75  
   11.76  fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
   11.77    (MetaSimplifier.goals_conv (Library.equal i)
   11.78      (MetaSimplifier.forall_conv
   11.79 -      (MetaSimplifier.goals_conv (K true) (Tactic.full_rewrite rews)))));
   11.80 +      (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
   11.81  
   11.82  fun atomize_tac i st =
   11.83    if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
   11.84 -    (rewrite_prems_tac (get_atomize_sg (Thm.sign_of_thm st)) i) st
   11.85 +    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   11.86    else all_tac st;
   11.87  
   11.88  fun atomize_goal i st =
   11.89    (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
   11.90  
   11.91  
   11.92 +(* rulify *)
   11.93 +
   11.94 +fun gen_rulify full thm =
   11.95 +  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
   11.96 +  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
   11.97 +
   11.98 +val rulify = gen_rulify true;
   11.99 +val rulify_no_asm = gen_rulify false;
  11.100 +
  11.101 +fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
  11.102 +fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
  11.103 +
  11.104 +
  11.105  
  11.106  (** theory setup **)
  11.107  
    12.1 --- a/src/ZF/ZF.ML	Sun Oct 14 22:07:01 2001 +0200
    12.2 +++ b/src/ZF/ZF.ML	Sun Oct 14 22:08:29 2001 +0200
    12.3 @@ -510,23 +510,6 @@
    12.4  by (Blast_tac 1);
    12.5  qed "Union_in_Pow";
    12.6  
    12.7 -
    12.8 -(* update rulify setup -- include bounded All *)
    12.9 -
   12.10  Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
   12.11  by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
   12.12  qed "atomize_ball";
   12.13 -
   12.14 -local
   12.15 -  val ss = FOL_basic_ss addsimps
   12.16 -    [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
   12.17 -in
   12.18 -
   12.19 -structure Rulify = RulifyFun
   12.20 - (val make_meta = Simplifier.simplify ss
   12.21 -  val full_make_meta = Simplifier.full_simplify ss);
   12.22 -
   12.23 -structure BasicRulify: BASIC_RULIFY = Rulify;
   12.24 -open BasicRulify;
   12.25 -
   12.26 -end;
    13.1 --- a/src/ZF/upair.thy	Sun Oct 14 22:07:01 2001 +0200
    13.2 +++ b/src/ZF/upair.thy	Sun Oct 14 22:08:29 2001 +0200
    13.3 @@ -8,6 +8,6 @@
    13.4  files "Tools/typechk":
    13.5  
    13.6  setup TypeCheck.setup
    13.7 -setup Rulify.setup
    13.8 +declare atomize_ball [symmetric, rulify]
    13.9  
   13.10  end