src/HOL/Nominal/nominal_thmdecls.ML
author wenzelm
Sat, 17 Oct 2009 14:43:18 +0200
changeset 32960 69916a850301
parent 32740 9dd0a2f83429
child 33519 e31a85f92ce9
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
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
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32429
diff changeset
    22
  val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    23
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    24
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    25
structure NominalThmDecls: NOMINAL_THMDECLS =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    26
struct
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    27
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    28
structure Data = GenericDataFun
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    29
(
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
  type T = thm list
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
    31
  val empty = []:T
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
  val extend = I
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
    33
  fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
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
    34
)
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    35
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    36
(* 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
    37
(* 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
    38
(* 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
    39
(* 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
    40
(* 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
    41
(* 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
    42
(* 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
    43
(* 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
    44
(* 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
    45
exception EQVT_FORM of string
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    46
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32429
diff changeset
    47
val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    48
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
fun tactic (msg, tac) =
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
  if !NOMINAL_EQVT_DEBUG
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
    51
  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
    52
  else tac
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    53
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    54
fun prove_eqvt_tac ctxt orig_thm pi pi' =
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
    55
let
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    56
  val mypi = Thm.cterm_of ctxt pi
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
    57
  val T = fastype_of pi'
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    58
  val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    59
  val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
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
    60
in
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    61
  EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    62
          tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
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
    63
          tactic ("solve with orig_thm", etac orig_thm),
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
    64
          tactic ("applies orig_thm instantiated with rev pi",
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
    65
                     dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    66
          tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
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
    67
          tactic ("getting rid of all remaining perms",
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
    68
                     full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
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
    69
end;
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    70
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    71
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
    72
  let
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    73
    val thy = ProofContext.theory_of ctxt;
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    74
    val pi' = Var (pi, typi);
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    75
    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
    76
    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
    77
      [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32091
diff changeset
    78
    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
    79
  in
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    80
    Goal.prove ctxt' [] [] goal_term
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    81
      (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
30088
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    82
    singleton (ProofContext.export ctxt' ctxt)
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
    83
  end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    84
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    85
(* 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
    86
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
    87
let
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    88
  fun replace n ty =
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    89
  let 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    90
    val c  = Const (@{const_name "perm"}, typi --> ty --> ty) 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    91
    val v1 = Var (pi, typi)
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    92
    val v2 = Var (n, ty)
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    93
  in
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    94
    c $ v1 $ v2 
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    95
  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
    96
in
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    97
  map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
    98
end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    99
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   100
(* 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
   101
(* exists such a pi; otherwise raises EQVT_FORM                        *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   102
fun get_pi t thy =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   103
  let fun get_pi_aux s =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   104
        (case s of
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   105
          (Const (@{const_name "perm"} ,typrm) $
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   106
             (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   107
               (Var (n,ty))) =>
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   108
             let
24039
273698405054 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents: 22846
diff changeset
   109
                (* 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
   110
                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
   111
             in
24271
499608101177 avoid low-level tsig;
wenzelm
parents: 24265
diff changeset
   112
                if (Sign.of_sort thy (ty,[class_name]))
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   113
                then [(pi,typi)]
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   114
                else raise
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   115
                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
   116
             end
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   117
        | Abs (_,_,t1) => get_pi_aux t1
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   118
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   119
        | _ => [])
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   120
  in
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   121
    (* 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
   122
    (* 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
   123
    (* a singleton-list  *)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   124
    (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
   125
      [(pi,typi)] => (pi, typi)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   126
    | _ => 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
   127
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   128
26652
43310f3721a5 proper dynamic facts for eqvts, freshs, bijs;
wenzelm
parents: 26400
diff changeset
   129
(* 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
   130
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   131
(* 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
   132
4d5917cc60c4 fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents: 24039
diff changeset
   133
fun eqvt_add_del_aux flag orig_thm context = 
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   134
  let
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   135
    val thy = Context.theory_of context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   136
    val thms_to_be_added = (case (prop_of orig_thm) of
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   137
        (* case: eqvt-lemma is of the implicational form *)
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   138
        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   139
          let
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   140
            val (pi,typi) = get_pi concl thy
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   141
          in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   142
             if (apply_pi hyp (pi,typi) = concl)
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   143
             then
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   144
               (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
   145
                [orig_thm,
fe6eac03b816 Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents: 29585
diff changeset
   146
                 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
   147
             else raise EQVT_FORM "Type Implication"
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   148
          end
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   149
       (* case: eqvt-lemma is of the equational form *)
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
   150
      | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   151
            (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
   152
           (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
   153
               then [orig_thm]
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   154
               else raise EQVT_FORM "Type Equality")
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22286
diff changeset
   155
      | _ => raise EQVT_FORM "Type unknown")
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   156
  in
26652
43310f3721a5 proper dynamic facts for eqvts, freshs, bijs;
wenzelm
parents: 26400
diff changeset
   157
      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
   158
  end
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22715
diff changeset
   159
  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
   160
      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
   161
               " 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
   162
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   163
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   164
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   165
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
   166
30991
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   167
val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
Christian Urban <urbanc@in.tum.de>
parents: 30986
diff changeset
   168
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
   169
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
   170
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
   171
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   172
val setup =
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
   173
    Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
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
   174
     "equivariance theorem declaration" 
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
   175
 #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
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
   176
     "equivariance theorem declaration (without checking the form of the lemma)" 
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
 #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
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
   178
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   179
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   180
end;