Quot/Nominal/nominal_thmdecls.ML
changeset 1037 2845e736dc1a
parent 947 fa810f01f7b5
child 1039 0d832c36b1bb
equal deleted inserted replaced
1032:135bf399c036 1037:2845e736dc1a
     1 (*  Title:      HOL/Nominal/nominal_thmdecls.ML
     1 (*  Title:      nominal_thmdecls.ML
     2     Author:     Julien Narboux, TU Muenchen
     2     Author:     Christian Urban
     3     Author:     Christian Urban, TU Muenchen
       
     4 
     3 
     5 Infrastructure for the lemma collection "eqvts".
     4   Infrastructure for the lemma collection "eqvts".
     6 
     5 
     7 By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in
     6   Provides the attributes [eqvt] and [eqvt_force], and the theorem
     8 a data-slot in the context. Possible modifiers are [... add] and
     7   list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be 
     9 [... del] for adding and deleting, respectively, the lemma from the
     8   stored are expected to be of the form
    10 data-slot.
     9 
       
    10     p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
       
    11 
       
    12   and are transformed into the form
       
    13 
       
    14     p o c == c
       
    15 
       
    16   TODO
       
    17 
       
    18    - deal with eqvt-lemmas of the for 
       
    19 
       
    20        c x1 x2 ... ==> c (p o x1) (p o x2) ..
    11 *)
    21 *)
    12 
    22 
    13 signature NOMINAL_THMDECLS =
    23 signature NOMINAL_THMDECLS =
    14 sig
    24 sig
    15   val eqvt_add: attribute
    25   val eqvt_add: attribute
    19   val setup: theory -> theory
    29   val setup: theory -> theory
    20   val get_eqvt_thms: Proof.context -> thm list
    30   val get_eqvt_thms: Proof.context -> thm list
    21 
    31 
    22 end;
    32 end;
    23 
    33 
    24 structure NominalThmDecls: NOMINAL_THMDECLS =
    34 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
    25 struct
    35 struct
    26 
    36 
    27 structure Data = Generic_Data
    37 structure EqvtData = Generic_Data
    28 (
    38 (
    29   type T = thm list
    39   type T = thm Item_Net.T;
    30   val empty = []
    40   val empty = Thm.full_rules;
    31   val extend = I
    41   val extend = I;
    32   val merge = Thm.merge_thms
    42   val merge = Item_Net.merge;
    33 )
    43 );
    34 
    44 
    35 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
    45 val content = Item_Net.content o EqvtData.get;
    36 (* There are two forms: one is an implication (for relations) and the other is an    *)
    46 val get_eqvt_thms = content o Context.Proof; 
    37 (* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
       
    38 (* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
       
    39 (* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
       
    40 (* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
       
    41 (* the implicational case it is also checked that the variables and permutation fit  *)
       
    42 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
       
    43 (* equality-lemma can be derived. *)
       
    44 exception EQVT_FORM of string
       
    45 
    47 
    46 val perm_boolE =
    48 val add_thm = EqvtData.map o Item_Net.update;
    47   @{lemma "pi \<bullet> P ==> P" by (simp add: permute_bool_def)};
    49 val del_thm = EqvtData.map o Item_Net.remove;
    48 
    50 
    49 val perm_boolI =
    51 val add_force_thm = EqvtData.map o Item_Net.update;
    50   @{lemma "P ==> pi \<bullet> P" by (simp add: permute_bool_def)};
    52 val del_force_thm = EqvtData.map o Item_Net.remove;
    51 
    53 
    52 fun prove_eqvt_tac ctxt orig_thm pi pi' =
    54 
       
    55 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
       
    56   | dest_perm t = raise TERM("dest_perm", [t])
       
    57 
       
    58 fun mk_perm p trm =
    53 let
    59 let
    54   val mypi = Thm.cterm_of ctxt pi
    60   val ty = fastype_of trm
    55   val T = fastype_of pi'
       
    56   val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi')
       
    57   val perm_pi_simp = @{thms permute_minus_cancel}
       
    58 in
    61 in
    59   EVERY1 [rtac @{thm iffI},
    62   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
    60           dtac perm_boolE,
       
    61           etac orig_thm,
       
    62           dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm),
       
    63           rtac perm_boolI,
       
    64           full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)]
       
    65 end;
       
    66 
       
    67 fun get_derived_thm ctxt hyp concl orig_thm pi =
       
    68   let
       
    69     val thy = ProofContext.theory_of ctxt;
       
    70     val pi' = Var (pi, @{typ "perm"});
       
    71     val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
       
    72     val ([goal_term, pi''], ctxt') = Variable.import_terms false
       
    73       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
       
    74   in
       
    75     Goal.prove ctxt' [] [] goal_term
       
    76       (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
       
    77     singleton (ProofContext.export ctxt' ctxt)
       
    78   end
       
    79 
       
    80 (* replaces in t every variable, say x, with pi o x *)
       
    81 fun apply_pi trm pi =
       
    82 let
       
    83   fun replace n ty =
       
    84   let 
       
    85     val c  = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) 
       
    86     val v1 = Var (pi, @{typ "perm"})
       
    87     val v2 = Var (n, ty)
       
    88   in
       
    89     c $ v1 $ v2 
       
    90   end
       
    91 in
       
    92   map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
       
    93 end
    63 end
    94 
    64 
    95 (* returns *the* pi which is in front of all variables, provided there *)
    65 fun eqvt_transform_tac thm = REPEAT o FIRST' 
    96 (* exists such a pi; otherwise raises EQVT_FORM                        *)
    66   [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
    97 fun get_pi t thy =
    67    rtac (thm RS @{thm trans}),
    98   let fun get_pi_aux s =
    68    rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
    99         (case s of
       
   100           (Const (@{const_name "permute"} ,typrm) $
       
   101              (Var (pi,_)) $
       
   102                (Var (n,ty))) =>
       
   103                 if (Sign.of_sort thy (ty, @{sort pt}))
       
   104                 then [pi]
       
   105                 else raise
       
   106                 EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt")
       
   107         | Abs (_,_,t1) => get_pi_aux t1
       
   108         | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
       
   109         | _ => [])
       
   110   in
       
   111     (* collect first all pi's in front of variables in t and then use distinct *)
       
   112     (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
       
   113     (* a singleton-list  *)
       
   114     (case (distinct (op =) (get_pi_aux t)) of
       
   115       [pi] => pi
       
   116     | [] => raise EQVT_FORM "No permutations found"
       
   117     | _ => raise EQVT_FORM "All permutation should be the same")
       
   118   end;
       
   119 
    69 
   120 (* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
    70 (* transform equations into the required form *)
   121 (* lemma list depending on flag. To be added the lemma has to satisfy a     *)
    71 fun transform_eq ctxt thm lhs rhs = 
   122 (* certain form. *)
    72 let
       
    73   val (p, t) = dest_perm lhs
       
    74   val (c, args) = strip_comb t
       
    75   val (c', args') = strip_comb rhs 
       
    76   val eargs = map Envir.eta_contract args 
       
    77   val eargs' = map Envir.eta_contract args'
       
    78   val p_str = fst (fst (dest_Var p))
       
    79   val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
       
    80 in
       
    81   if c <> c' 
       
    82     then error "eqvt lemma is not of the right form (constants do not agree)"
       
    83   else if eargs' <> map (mk_perm p) eargs 
       
    84     then error "eqvt lemma is not of the right form (arguments do not agree)"
       
    85   else if args = [] 
       
    86     then thm
       
    87   else Goal.prove ctxt [p_str] [] goal
       
    88     (fn _ => eqvt_transform_tac thm 1)
       
    89 end
   123 
    90 
   124 fun eqvt_add_del_aux flag orig_thm context = 
    91 fun transform addel_fn thm context = 
   125   let
    92 let
   126     val thy = Context.theory_of context
    93   val ctxt = Context.proof_of context
   127     val thms_to_be_added = (case (prop_of orig_thm) of
    94   val trm = HOLogic.dest_Trueprop (prop_of thm)
   128         (* case: eqvt-lemma is of the implicational form *)
    95 in
   129         (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
    96   case trm of
   130           let
    97     Const (@{const_name "op ="}, _) $ lhs $ rhs => 
   131             val pi = get_pi concl thy
    98       addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context
   132           in
    99   | _ => raise (error "no other cases yet implemented")
   133              if (apply_pi hyp pi = concl)
   100 end 
   134              then
       
   135                (warning ("equivariance lemma of the relational form");
       
   136                 [orig_thm,
       
   137                  get_derived_thm (Context.proof_of context) hyp concl orig_thm pi])
       
   138              else raise EQVT_FORM "Type Implication"
       
   139           end
       
   140        (* case: eqvt-lemma is of the equational form *)
       
   141       | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
       
   142             (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) =>
       
   143            (if (apply_pi lhs pi) = rhs
       
   144                then [orig_thm]
       
   145                else raise EQVT_FORM "Type Equality")
       
   146       | _ => raise EQVT_FORM "Type unknown")
       
   147   in
       
   148       fold (fn thm => Data.map (flag thm)) thms_to_be_added context
       
   149   end
       
   150   handle EQVT_FORM s =>
       
   151       error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
       
   152                " does not comply with the form of an equivariance lemma (" ^ s ^").")
       
   153 
   101 
   154 
   102 
   155 val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
   103 val eqvt_add = Thm.declaration_attribute (transform add_thm);
   156 val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
   104 val eqvt_del = Thm.declaration_attribute (transform del_thm);
   157 
   105 
   158 val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
   106 val eqvt_force_add = Thm.declaration_attribute add_force_thm;
   159 val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
   107 val eqvt_force_del = Thm.declaration_attribute del_force_thm;
   160 
       
   161 val get_eqvt_thms = Context.Proof #> Data.get;
       
   162 
   108 
   163 val setup =
   109 val setup =
   164     Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
   110   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
   165      "equivariance theorem declaration" 
   111     (cat_lines ["declaration of equivariance lemmas - they will automtically be",  
   166  #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
   112                 "brought into the form p o c = c"]) #>
   167      "equivariance theorem declaration (without checking the form of the lemma)" 
   113   Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
   168  #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
   114     (cat_lines ["declaration of equivariance lemmas - they will will be", 
       
   115                 "added/deleted directly to the eqvt thm-list"]) #>
       
   116   PureThy.add_thms_dynamic (@{binding "eqvt"}, content);
   169 
   117 
   170 
   118 
   171 end;
   119 end;