src/HOL/Nominal/nominal_thmdecls.ML
author urbanc
Thu, 08 Feb 2007 17:22:22 +0100
changeset 22286 85b065601f45
parent 22250 0d7ea7d2bc28
child 22418 49e2d9744ae1
permissions -rw-r--r--
added get-functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     1
(* ID: "$Id$"
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     2
   Authors: Julien Narboux and Christian Urban
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     3
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     4
   This file introduces the infrastructure for the lemma 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     5
   declaration "eqvt" "bij" and "fresh".
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     6
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     7
   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     8
   in a data-slot in the theory context. Possible modifiers
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
     9
   are [attribute add] and [attribute del] for adding and deleting,
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    10
   respectively the lemma from the data-slot.  
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
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    15
  val print_data: Proof.context -> unit
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    16
  val eqvt_add: attribute
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    17
  val eqvt_del: attribute
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    18
  val setup: theory -> theory
22286
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    19
  val get_eqvt_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    20
  val get_fresh_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    21
  val get_bij_thms: theory -> thm list
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    22
  
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    23
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    24
  val NOMINAL_EQVT_DEBUG : bool ref
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    25
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    26
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    27
structure NominalThmDecls: NOMINAL_THMDECLS =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    28
struct
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    29
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    30
structure Data = GenericDataFun
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    31
(
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    32
  val name = "HOL/Nominal/eqvt";
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    33
  type T = {eqvt:thm list, fresh:thm list, bij:thm list};
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    34
  val empty = ({eqvt=[], fresh=[], bij=[]}:T);
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    35
  val extend = I;
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    36
  fun merge _ (r1:T,r2:T) = {eqvt  = Drule.merge_rules (#eqvt r1, #eqvt r2), 
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    37
                             fresh = Drule.merge_rules (#fresh r1, #fresh r2), 
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    38
                             bij   = Drule.merge_rules (#bij r1, #bij r2)}
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    39
  fun print context (data:T) =
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    40
    let 
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    41
       fun print_aux msg thms =
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    42
         Pretty.writeln (Pretty.big_list msg
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    43
           (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    44
    in
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    45
      (print_aux "Equivariance lemmas: " (#eqvt data);
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    46
       print_aux "Freshness lemmas: " (#fresh data);
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    47
       print_aux "Bijection lemmas: " (#bij data))
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    48
    end;
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    49
 
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    50
);
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    51
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    52
(* 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
    53
(* 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
    54
(* 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
    55
(* 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
    56
(* 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
    57
(* 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
    58
(* 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
    59
(* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    60
(* eqality-lemma can be derived. *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    61
exception EQVT_FORM;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    62
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
    63
val print_data = Data.print o Context.Proof;
22286
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    64
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvt;
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    65
val get_fresh_thms = Context.Theory #> Data.get #> #fresh;
85b065601f45 added get-functions
urbanc
parents: 22250
diff changeset
    66
val get_bij_thms = Context.Theory #> Data.get #> #bij;
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    67
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    68
(* FIXME: should be a function in a library *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    69
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    70
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    71
val perm_bool = thm "perm_bool";
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    72
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    73
val NOMINAL_EQVT_DEBUG = ref false;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    74
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    75
fun tactic (msg,tac) = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    76
    if !NOMINAL_EQVT_DEBUG 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    77
    then (EVERY [tac, print_tac ("after "^msg)])
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    78
    else tac 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    79
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    80
fun tactic_eqvt ctx orig_thm pi typi = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    81
    let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    82
        val mypi = Thm.cterm_of ctx (Var (pi,typi))
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    83
        val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    84
        val perm_pi_simp = PureThy.get_thms ctx (Name "perm_pi_simp")
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    85
    in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    86
        EVERY [tactic ("iffI applied",rtac iffI 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    87
               tactic ("simplifies with orig_thm and perm_bool", 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    88
                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    89
               tactic ("applies orig_thm instantiated with rev pi",
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    90
                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    91
               tactic ("getting rid of all remaining perms",
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    92
                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    93
    end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    94
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    95
fun get_derived_thm thy hyp concl orig_thm pi typi =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    96
   let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    97
       val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    98
       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
    99
       val _ = Display.print_cterm (cterm_of thy goal_term) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   100
   in	
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   101
     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   102
   end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   103
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   104
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   105
(* the eqvt_thm_list to the user, we have to manually update the context and the      *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   106
(* thm-list eqvt *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   107
fun update_context flag thms context =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   108
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   109
     val context' = fold (fn thm => Data.map (flag thm)) thms context 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   110
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   111
    Context.mapping (snd o PureThy.add_thmss [(("eqvt",(#eqvt (Data.get context'))),[])]) I context'
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   112
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   113
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   114
(* replaces every variable x in t with pi o x *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   115
fun apply_pi trm (pi,typi) =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   116
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   117
    fun only_vars t =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   118
       (case t of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   119
          Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   120
        | _ => t)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   121
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   122
     map_aterms only_vars trm 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   123
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   124
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   125
(* 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
   126
(* exists such a pi; otherwise raises EQVT_FORM                        *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   127
fun get_pi t thy =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   128
  let fun get_pi_aux s =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   129
        (case s of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   130
          (Const ("Nominal.perm",typrm) $ 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   131
             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   132
               (Var (n,ty))) => 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   133
             let
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   134
		(* FIXME: this should be an operation the library *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   135
                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   136
	     in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   137
		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   138
                then [(pi,typi)] 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   139
                else raise EQVT_FORM 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   140
             end 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   141
        | Abs (_,_,t1) => get_pi_aux t1
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   142
        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   143
        | _ => [])  
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   144
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   145
    (* 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
   146
    (* 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
   147
    (* a singleton-list  *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   148
    (case (distinct (op =) (get_pi_aux t)) of 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   149
      [(pi,typi)] => (pi,typi)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   150
    | _ => raise EQVT_FORM)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   151
  end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   152
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   153
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   154
(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   155
(* certain form. *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   156
fun eqvt_add_del_aux flag orig_thm context =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   157
  let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   158
    val thy = Context.theory_of context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   159
    val thms_to_be_added = (case (prop_of orig_thm) of
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   160
        (* case: eqvt-lemma is of the implicational form *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   161
        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   162
          let  
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   163
            val (pi,typi) = get_pi concl thy
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   164
          in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   165
             if (apply_pi hyp (pi,typi) = concl)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   166
             then 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   167
               (warning ("equivariance lemma of the relational form");
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   168
                [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   169
             else raise EQVT_FORM
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   170
          end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   171
        (* case: eqvt-lemma is of the equational form *)  
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   172
      | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   173
            (Const ("Nominal.perm",_) $ Var (pi,typi) $ lhs) $ rhs)) =>
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   174
	      (if (apply_pi lhs (pi,typi)) = rhs 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   175
               then [orig_thm] 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   176
               else raise EQVT_FORM)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   177
      | _ => raise EQVT_FORM)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   178
  in 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   179
      update_context flag thms_to_be_added context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   180
  end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   181
  handle EQVT_FORM => 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   182
      error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma.")
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   183
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   184
(* in cases of bij- and freshness, we just add the lemmas to the *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   185
(* data-slot *) 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   186
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   187
fun simple_add_del_aux record_access name flag th context = 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   188
   let 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   189
     val context' = Data.map (flag th) context
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   190
   in
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   191
     Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   192
   end
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   193
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
   194
fun bij_add_del_aux f   = simple_add_del_aux #bij "bij" f
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
   195
fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   196
22250
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
   197
fun eqvt_map f th (r:Data.T)  = {eqvt = (f th (#eqvt r)), fresh = #fresh r, bij = #bij r};
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
   198
fun fresh_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = (f th (#fresh r)), bij = #bij r};
0d7ea7d2bc28 fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents: 22245
diff changeset
   199
fun bij_map f th (r:Data.T)   = {eqvt = #eqvt r, fresh = #fresh r, bij = (f th (#bij r))};
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   200
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   201
val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   202
val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   203
val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   204
val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   205
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   206
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   207
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   208
val setup =
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   209
  Data.init #>
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   210
  Attrib.add_attributes 
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   211
     [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   212
      ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   213
      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   214
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   215
end;
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   216
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   217
(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   218
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   219
(* Drule.add_rule has type thm -> thm list -> thm list *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   220
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   221
(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   222
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff changeset
   223
(* add_del_args is of type attribute -> attribute -> src -> attribute *)