src/Pure/Isar/object_logic.ML
author wenzelm
Tue, 06 Aug 2019 16:15:22 +0200
changeset 70657 1004333b76aa
parent 70572 35dd9212bf29
child 74694 e098fa45bfe0
permissions -rw-r--r--
clarified context: proper transfer;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/object_logic.ML
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     3
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     4
Specifics about common object-logics.
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     5
*)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     6
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     7
signature OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     8
sig
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
     9
  val get_base_sort: Proof.context -> sort option
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    10
  val add_base_sort: sort -> theory -> theory
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    11
  val add_judgment: binding * typ * mixfix -> theory -> theory
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    12
  val add_judgment_cmd: binding * string * mixfix -> theory -> theory
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    13
  val judgment_name: Proof.context -> string
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    14
  val is_judgment: Proof.context -> term -> bool
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    15
  val drop_judgment: Proof.context -> term -> term
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    16
  val fixed_judgment: Proof.context -> string -> term
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    17
  val ensure_propT: Proof.context -> term -> term
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    18
  val dest_judgment: Proof.context -> cterm -> cterm
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    19
  val judgment_conv: Proof.context -> conv -> conv
70170
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
    20
  val is_propositional: Proof.context -> typ -> bool
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    21
  val elim_concl: Proof.context -> thm -> term option
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    22
  val declare_atomize: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    23
  val declare_rulify: attribute
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    24
  val atomize_term: Proof.context -> term -> term
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    25
  val atomize: Proof.context -> conv
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    26
  val atomize_prems: Proof.context -> conv
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    27
  val atomize_prems_tac: Proof.context -> int -> tactic
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    28
  val full_atomize_tac: Proof.context -> int -> tactic
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    29
  val rulify_term: Proof.context -> term -> term
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    30
  val rulify_tac: Proof.context -> int -> tactic
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    31
  val rulify: Proof.context -> thm -> thm
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    32
  val rulify_no_asm: Proof.context -> thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    33
  val rule_format: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    34
  val rule_format_no_asm: attribute
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    35
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    36
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35129
diff changeset
    37
structure Object_Logic: OBJECT_LOGIC =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    38
struct
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    39
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    40
(** context data **)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    41
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    42
datatype data = Data of
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    43
 {base_sort: sort option,
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    44
  judgment: string option,
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    45
  atomize_rulify: thm list * thm list};
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    46
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    47
fun make_data (base_sort, judgment, atomize_rulify) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    48
  Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    49
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    50
structure Data = Generic_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
    51
(
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    52
  type T = data;
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    53
  val empty = make_data (NONE, NONE, ([], []));
16449
d0dc9a301e37 accomodate change of TheoryDataFun;
wenzelm
parents: 15973
diff changeset
    54
  val extend = I;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    55
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    56
  fun merge_opt eq (SOME x, SOME y) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    57
        if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
41493
f05976d69141 added merge_options convenience;
wenzelm
parents: 41228
diff changeset
    58
    | merge_opt _ data = merge_options data;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    59
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33090
diff changeset
    60
  fun merge
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    61
     (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    62
      Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    63
    make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 23602
diff changeset
    64
      (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
    65
);
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
    66
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36610
diff changeset
    67
fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    68
  make_data (f (base_sort, judgment, atomize_rulify)));
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    69
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    70
fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args);
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    71
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    72
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    73
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    74
(** generic treatment of judgments -- with a single argument only **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    75
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    76
(* base_sort *)
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    77
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    78
val get_base_sort = #base_sort o get_data;
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    79
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    80
fun add_base_sort S =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    81
  (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    82
    if is_some base_sort then error "Attempt to redeclare object-logic base sort"
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    83
    else (SOME S, judgment, atomize_rulify));
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    84
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    85
18825
c13136d648e2 removed unatomize;
wenzelm
parents: 18807
diff changeset
    86
(* add judgment *)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    87
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    88
local
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    89
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 29606
diff changeset
    90
fun gen_add_judgment add_consts (b, T, mx) thy =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    91
  let
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    92
    val c = Sign.full_name thy b;
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    93
    val thy' = thy |> add_consts [(b, T, mx)];
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    94
    val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    95
  in
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    96
    thy'
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61246
diff changeset
    97
    |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
    98
    |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
    99
        if is_some judgment then error "Attempt to redeclare object-logic judgment"
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   100
        else (base_sort, SOME c, atomize_rulify))
14226
7afe0e5bcc83 Made judgments automatically declared final.
skalberg
parents: 13376
diff changeset
   101
  end;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   102
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   103
in
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   104
56239
17df7145a871 tuned signature;
wenzelm
parents: 54742
diff changeset
   105
val add_judgment = gen_add_judgment Sign.add_consts;
17df7145a871 tuned signature;
wenzelm
parents: 54742
diff changeset
   106
val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   107
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   108
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   109
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   110
23566
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   111
(* judgments *)
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   112
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   113
fun judgment_name ctxt =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   114
  (case #judgment (get_data ctxt) of
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   115
    SOME name => name
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   116
  | _ => raise TERM ("Unknown object-logic judgment", []));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   117
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   118
fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   119
  | is_judgment _ _ = false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   120
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   121
fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   122
  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   123
      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   124
  | drop_judgment _ tm = tm;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   125
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   126
fun fixed_judgment ctxt x =
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   127
  let  (*be robust wrt. low-level errors*)
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   128
    val c = judgment_name ctxt;
70572
wenzelm
parents: 70170
diff changeset
   129
    val aT = Term.aT [];
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   130
    val T =
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   131
      the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
60443
wenzelm
parents: 59970
diff changeset
   132
      |> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   133
    val U = Term.domain_type T handle Match => aT;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   134
  in Const (c, T) $ Free (x, U) end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   135
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   136
fun ensure_propT ctxt t =
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   137
  let val T = Term.fastype_of t
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   138
  in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end;
13376
59975b8417e2 assert_propT;
wenzelm
parents: 13334
diff changeset
   139
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   140
fun dest_judgment ctxt ct =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   141
  if is_judgment ctxt (Thm.term_of ct)
23586
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   142
  then Thm.dest_arg ct
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   143
  else raise CTERM ("dest_judgment", [ct]);
7d6b1d800dc4 avoid polymorphic equality;
wenzelm
parents: 23566
diff changeset
   144
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   145
fun judgment_conv ctxt cv ct =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   146
  if is_judgment ctxt (Thm.term_of ct)
23566
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   147
  then Conv.arg_conv cv ct
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   148
  else raise CTERM ("judgment_conv", [ct]);
b65692d4adcd replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents: 23540
diff changeset
   149
70170
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
   150
fun is_propositional ctxt T =
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
   151
  T = propT orelse
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
   152
    let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T))
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
   153
    in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end;
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 61853
diff changeset
   154
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   155
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   156
(* elimination rules *)
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   157
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   158
fun elim_concl ctxt rule =
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   159
  let
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   160
    val concl = Thm.concl_of rule;
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   161
    val C = drop_judgment ctxt concl;
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   162
  in
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   163
    if Term.is_Var C andalso
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   164
      exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41493
diff changeset
   165
    then SOME C else NONE
19261
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   166
  end;
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   167
9f8e56d1dbf6 added is_elim (from Provers/classical.ML);
wenzelm
parents: 18939
diff changeset
   168
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   169
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   170
(** treatment of meta-level connectives **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   171
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   172
(* maintain rules *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   173
70657
1004333b76aa clarified context: proper transfer;
wenzelm
parents: 70572
diff changeset
   174
fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt)));
1004333b76aa clarified context: proper transfer;
wenzelm
parents: 70572
diff changeset
   175
val get_atomize = get_atomize_rulify #1;
1004333b76aa clarified context: proper transfer;
wenzelm
parents: 70572
diff changeset
   176
val get_rulify = get_atomize_rulify #2;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   177
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   178
fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
61092
d261ac466180 trim context for persistent storage;
wenzelm
parents: 60822
diff changeset
   179
  (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify)));
25497
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   180
1c9b3733f887 added base_sort;
wenzelm
parents: 25018
diff changeset
   181
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
61092
d261ac466180 trim context for persistent storage;
wenzelm
parents: 60822
diff changeset
   182
  (base_sort, judgment, (atomize, Thm.add_thm (Thm.trim_context th) rulify)));
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   183
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   184
val declare_atomize = Thm.declaration_attribute add_atomize;
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   185
val declare_rulify = Thm.declaration_attribute add_rulify;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22796
diff changeset
   186
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   187
val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   188
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   189
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   190
(* atomize *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   191
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   192
fun atomize_term ctxt =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   193
  drop_judgment ctxt o
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   194
    Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
12729
46808b5ec985 added atomize_cterm;
wenzelm
parents: 12725
diff changeset
   195
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   196
fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
14743
81001d6cb8c0 conversion of theorems to atomic form
paulson
parents: 14226
diff changeset
   197
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   198
fun atomize_prems ctxt ct =
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   199
  if Logic.has_meta_prems (Thm.term_of ct) then
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   200
    Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct
23602
361e9c3a5e3a tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents: 23586
diff changeset
   201
  else Conv.all_conv ct;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   202
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   203
val atomize_prems_tac = CONVERSION o atomize_prems;
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   204
val full_atomize_tac = CONVERSION o atomize;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   205
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   206
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   207
(* rulify *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   208
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   209
fun rulify_term ctxt =
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   210
  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) [];
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   211
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   212
fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
18807
80df0609d25f renamed reverse_atomize to unatomize;
wenzelm
parents: 18783
diff changeset
   213
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   214
fun gen_rulify full ctxt =
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59647
diff changeset
   215
  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
60822
4f58f3662e7d more explicit context;
wenzelm
parents: 60443
diff changeset
   216
  #> Variable.gen_all ctxt
59647
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 56239
diff changeset
   217
  #> Thm.strip_shyps
c6f413b660cf clarified Drule.gen_all: observe context more carefully;
wenzelm
parents: 56239
diff changeset
   218
  #> Drule.zero_var_indexes;
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   219
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   220
val rulify = gen_rulify true;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   221
val rulify_no_asm = gen_rulify false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   222
61853
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61255
diff changeset
   223
val rule_format = Thm.rule_attribute [] (rulify o Context.proof_of);
fb7756087101 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents: 61255
diff changeset
   224
val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of);
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   225
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   226
end;