src/HOL/Nominal/nominal_thmdecls.ML
author wenzelm
Thu, 18 Apr 2013 17:07:01 +0200
changeset 51717 9e7d1c139569
parent 42616 92715b528e78
child 54990 8dc8d427b313
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     1
(*  Title:      HOL/Nominal/nominal_thmdecls.ML
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     2
    Author:     Julien Narboux, TU Muenchen
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     3
    Author:     Christian Urban, TU Muenchen
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     5
Infrastructure for the lemma collection "eqvts".
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     6
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     7
By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     8
a data-slot in the context. Possible modifiers are [... add] and
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
     9
[... del] for adding and deleting, respectively, the lemma from the
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    10
data-slot.
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    11
*)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    12
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    13
signature NOMINAL_THMDECLS =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    14
sig
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    15
  val eqvt_add: attribute
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    16
  val eqvt_del: attribute
22715
381e6c45f13b improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents: 22562
diff changeset
    17
  val eqvt_force_add: attribute
381e6c45f13b improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents: 22562
diff changeset
    18
  val eqvt_force_del: attribute
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    19
  val setup: theory -> theory
24571
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24271
diff changeset
    20
  val get_eqvt_thms: Proof.context -> thm list
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    21
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    22
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    23
structure NominalThmDecls: NOMINAL_THMDECLS =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    24
struct
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    25
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 32960
diff changeset
    26
structure Data = Generic_Data
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    27
(
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    28
  type T = thm list
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 32960
diff changeset
    29
  val empty = []
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    30
  val extend = I
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 32960
diff changeset
    31
  val merge = Thm.merge_thms
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    32
)
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    33
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    34
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    35
(* There are two forms: one is an implication (for relations) and the other is an    *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    36
(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    37
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    38
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    39
(* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    40
(* the implicational case it is also checked that the variables and permutation fit  *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    41
(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
24265
4d5917cc60c4 fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents: 24039
diff changeset
    42
(* equality-lemma can be derived. *)
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    43
exception EQVT_FORM of string
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    44
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42361
diff changeset
    45
val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    46
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    47
fun tactic ctxt (msg, tac) =
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    48
  if Config.get ctxt nominal_eqvt_debug
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    49
  then tac THEN' (K (print_tac ("after " ^ msg)))
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    50
  else tac
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    51
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    52
fun prove_eqvt_tac ctxt orig_thm pi pi' =
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    53
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    54
    val thy = Proof_Context.theory_of ctxt
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    55
    val mypi = Thm.cterm_of thy pi
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    56
    val T = fastype_of pi'
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    57
    val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38864
diff changeset
    58
    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    59
  in
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    60
    EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    61
            tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    62
            tactic ctxt ("solve with orig_thm", etac orig_thm),
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    63
            tactic ctxt ("applies orig_thm instantiated with rev pi",
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    64
                       dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    65
            tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    66
            tactic ctxt ("getting rid of all remaining perms",
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42616
diff changeset
    67
                       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    68
  end;
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    69
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    70
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    71
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    72
    val thy = Proof_Context.theory_of ctxt;
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    73
    val pi' = Var (pi, typi);
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    74
    val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    75
    val ([goal_term, pi''], ctxt') = Variable.import_terms false
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    76
      [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
    77
    val _ = writeln (Syntax.string_of_term ctxt' goal_term);
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    78
  in
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    79
    Goal.prove ctxt' [] [] goal_term
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
    80
      (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
    81
    singleton (Proof_Context.export ctxt' ctxt)
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    82
  end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    83
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    84
(* replaces in t every variable, say x, with pi o x *)
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    85
fun apply_pi trm (pi, typi) =
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    86
let
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    87
  fun replace n ty =
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    88
  let 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    89
    val c  = Const (@{const_name "perm"}, typi --> ty --> ty) 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    90
    val v1 = Var (pi, typi)
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    91
    val v2 = Var (n, ty)
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    92
  in
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    93
    c $ v1 $ v2 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    94
  end
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
    95
in
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    96
  map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    97
end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    98
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    99
(* returns *the* pi which is in front of all variables, provided there *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   100
(* exists such a pi; otherwise raises EQVT_FORM                        *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   101
fun get_pi t thy =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   102
  let fun get_pi_aux s =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   103
        (case s of
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   104
          (Const (@{const_name "perm"} ,typrm) $
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   105
             (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   106
               (Var (n,ty))) =>
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   107
             let
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
   108
                (* FIXME: this should be an operation the library *)
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   109
                val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
   110
             in
24271
499608101177 avoid low-level tsig;
wenzelm
parents: 24265
diff changeset
   111
                if (Sign.of_sort thy (ty,[class_name]))
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   112
                then [(pi,typi)]
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   113
                else raise
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   114
                EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   115
             end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   116
        | Abs (_,_,t1) => get_pi_aux t1
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   117
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   118
        | _ => [])
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   119
  in
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   120
    (* collect first all pi's in front of variables in t and then use distinct *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   121
    (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   122
    (* a singleton-list  *)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   123
    (case (distinct (op =) (get_pi_aux t)) of
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
   124
      [(pi,typi)] => (pi, typi)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   125
    | _ => raise EQVT_FORM "All permutation should be the same")
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   126
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   127
26652
43310f3721a5 proper dynamic facts for eqvts, freshs, bijs;
wenzelm
parents: 26400
diff changeset
   128
(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   129
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   130
(* certain form. *)
24265
4d5917cc60c4 fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents: 24039
diff changeset
   131
4d5917cc60c4 fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents: 24039
diff changeset
   132
fun eqvt_add_del_aux flag orig_thm context = 
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   133
  let
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   134
    val thy = Context.theory_of context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   135
    val thms_to_be_added = (case (prop_of orig_thm) of
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   136
        (* case: eqvt-lemma is of the implicational form *)
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   137
        (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   138
          let
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   139
            val (pi,typi) = get_pi concl thy
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   140
          in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   141
             if (apply_pi hyp (pi,typi) = concl)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   142
             then
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   143
               (warning ("equivariance lemma of the relational form");
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
   144
                [orig_thm,
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
   145
                 get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi])
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   146
             else raise EQVT_FORM "Type Implication"
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   147
          end
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   148
       (* case: eqvt-lemma is of the equational form *)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38808
diff changeset
   149
      | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   150
            (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
   151
           (if (apply_pi lhs (pi,typi)) = rhs
22437
b3526cd2a336 removes some unused code that used to try to derive a simpler version of the eqvt lemmas
narboux
parents: 22418
diff changeset
   152
               then [orig_thm]
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   153
               else raise EQVT_FORM "Type Equality")
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   154
      | _ => raise EQVT_FORM "Type unknown")
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   155
  in
26652
43310f3721a5 proper dynamic facts for eqvts, freshs, bijs;
wenzelm
parents: 26400
diff changeset
   156
      fold (fn thm => Data.map (flag thm)) thms_to_be_added context
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   157
  end
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   158
  handle EQVT_FORM s =>
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 30991
diff changeset
   159
      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
   160
               " does not comply with the form of an equivariance lemma (" ^ s ^").")
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   161
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   162
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   163
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   164
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   165
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   166
val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   167
val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   168
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
   169
val get_eqvt_thms = Context.Proof #> Data.get;
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   170
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   171
val setup =
38807
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
   172
  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
   173
   "equivariance theorem declaration" #>
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
   174
  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
378ffc903bed eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents: 38558
diff changeset
   175
    "equivariance theorem declaration (without checking the form of the lemma)" #>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38864
diff changeset
   176
  Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);
30986
047fa04a9fe8 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents: 30528
diff changeset
   177
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   178
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   179
end;