diff -r 135bf399c036 -r 2845e736dc1a Quot/Nominal/nominal_thmdecls.ML --- a/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 09:25:21 2010 +0100 +++ b/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:06:10 2010 +0100 @@ -1,13 +1,23 @@ -(* Title: HOL/Nominal/nominal_thmdecls.ML - Author: Julien Narboux, TU Muenchen - Author: Christian Urban, TU Muenchen +(* Title: nominal_thmdecls.ML + Author: Christian Urban + + Infrastructure for the lemma collection "eqvts". + + Provides the attributes [eqvt] and [eqvt_force], and the theorem + list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be + stored are expected to be of the form -Infrastructure for the lemma collection "eqvts". + p o (c x1 x2 ...) = c (p o x1) (p o x2) ... + + and are transformed into the form + + p o c == c -By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in -a data-slot in the context. Possible modifiers are [... add] and -[... del] for adding and deleting, respectively, the lemma from the -data-slot. + TODO + + - deal with eqvt-lemmas of the for + + c x1 x2 ... ==> c (p o x1) (p o x2) .. *) signature NOMINAL_THMDECLS = @@ -21,151 +31,89 @@ end; -structure NominalThmDecls: NOMINAL_THMDECLS = +structure Nominal_ThmDecls: NOMINAL_THMDECLS = struct -structure Data = Generic_Data +structure EqvtData = Generic_Data ( - type T = thm list - val empty = [] - val extend = I - val merge = Thm.merge_thms -) + type T = thm Item_Net.T; + val empty = Thm.full_rules; + val extend = I; + val merge = Item_Net.merge; +); + +val content = Item_Net.content o EqvtData.get; +val get_eqvt_thms = content o Context.Proof; -(* Exception for when a theorem does not conform with form of an equivariance lemma. *) -(* There are two forms: one is an implication (for relations) and the other is an *) -(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *) -(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) -(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) -(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) -(* the implicational case it is also checked that the variables and permutation fit *) -(* together, i.e. are of the right "pt_class", so that a stronger version of the *) -(* equality-lemma can be derived. *) -exception EQVT_FORM of string +val add_thm = EqvtData.map o Item_Net.update; +val del_thm = EqvtData.map o Item_Net.remove; + +val add_force_thm = EqvtData.map o Item_Net.update; +val del_force_thm = EqvtData.map o Item_Net.remove; + -val perm_boolE = - @{lemma "pi \ P ==> P" by (simp add: permute_bool_def)}; - -val perm_boolI = - @{lemma "P ==> pi \ P" by (simp add: permute_bool_def)}; +fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) + | dest_perm t = raise TERM("dest_perm", [t]) -fun prove_eqvt_tac ctxt orig_thm pi pi' = +fun mk_perm p trm = let - val mypi = Thm.cterm_of ctxt pi - val T = fastype_of pi' - val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi') - val perm_pi_simp = @{thms permute_minus_cancel} + val ty = fastype_of trm in - EVERY1 [rtac @{thm iffI}, - dtac perm_boolE, - etac orig_thm, - dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm), - rtac perm_boolI, - full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)] -end; - -fun get_derived_thm ctxt hyp concl orig_thm pi = - let - val thy = ProofContext.theory_of ctxt; - val pi' = Var (pi, @{typ "perm"}); - val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; - val ([goal_term, pi''], ctxt') = Variable.import_terms false - [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt - in - Goal.prove ctxt' [] [] goal_term - (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |> - singleton (ProofContext.export ctxt' ctxt) - end - -(* replaces in t every variable, say x, with pi o x *) -fun apply_pi trm pi = -let - fun replace n ty = - let - val c = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) - val v1 = Var (pi, @{typ "perm"}) - val v2 = Var (n, ty) - in - c $ v1 $ v2 - end -in - map_aterms (fn Var (n, ty) => replace n ty | t => t) trm + Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm end -(* returns *the* pi which is in front of all variables, provided there *) -(* exists such a pi; otherwise raises EQVT_FORM *) -fun get_pi t thy = - let fun get_pi_aux s = - (case s of - (Const (@{const_name "permute"} ,typrm) $ - (Var (pi,_)) $ - (Var (n,ty))) => - if (Sign.of_sort thy (ty, @{sort pt})) - then [pi] - else raise - EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt") - | Abs (_,_,t1) => get_pi_aux t1 - | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 - | _ => []) - in - (* collect first all pi's in front of variables in t and then use distinct *) - (* to ensure that all pi's must have been the same, i.e. distinct returns *) - (* a singleton-list *) - (case (distinct (op =) (get_pi_aux t)) of - [pi] => pi - | [] => raise EQVT_FORM "No permutations found" - | _ => raise EQVT_FORM "All permutation should be the same") - end; - -(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *) -(* lemma list depending on flag. To be added the lemma has to satisfy a *) -(* certain form. *) +fun eqvt_transform_tac thm = REPEAT o FIRST' + [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), + rtac (thm RS @{thm trans}), + rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] -fun eqvt_add_del_aux flag orig_thm context = - let - val thy = Context.theory_of context - val thms_to_be_added = (case (prop_of orig_thm) of - (* case: eqvt-lemma is of the implicational form *) - (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => - let - val pi = get_pi concl thy - in - if (apply_pi hyp pi = concl) - then - (warning ("equivariance lemma of the relational form"); - [orig_thm, - get_derived_thm (Context.proof_of context) hyp concl orig_thm pi]) - else raise EQVT_FORM "Type Implication" - end - (* case: eqvt-lemma is of the equational form *) - | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ - (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) => - (if (apply_pi lhs pi) = rhs - then [orig_thm] - else raise EQVT_FORM "Type Equality") - | _ => raise EQVT_FORM "Type unknown") - in - fold (fn thm => Data.map (flag thm)) thms_to_be_added context - end - handle EQVT_FORM s => - error (Display.string_of_thm (Context.proof_of context) orig_thm ^ - " does not comply with the form of an equivariance lemma (" ^ s ^").") +(* transform equations into the required form *) +fun transform_eq ctxt thm lhs rhs = +let + val (p, t) = dest_perm lhs + val (c, args) = strip_comb t + val (c', args') = strip_comb rhs + val eargs = map Envir.eta_contract args + val eargs' = map Envir.eta_contract args' + val p_str = fst (fst (dest_Var p)) + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) +in + if c <> c' + then error "eqvt lemma is not of the right form (constants do not agree)" + else if eargs' <> map (mk_perm p) eargs + then error "eqvt lemma is not of the right form (arguments do not agree)" + else if args = [] + then thm + else Goal.prove ctxt [p_str] [] goal + (fn _ => eqvt_transform_tac thm 1) +end + +fun transform addel_fn thm context = +let + val ctxt = Context.proof_of context + val trm = HOLogic.dest_Trueprop (prop_of thm) +in + case trm of + Const (@{const_name "op ="}, _) $ lhs $ rhs => + addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context + | _ => raise (error "no other cases yet implemented") +end -val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm)); -val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm)); +val eqvt_add = Thm.declaration_attribute (transform add_thm); +val eqvt_del = Thm.declaration_attribute (transform del_thm); -val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm); -val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm); - -val get_eqvt_thms = Context.Proof #> Data.get; +val eqvt_force_add = Thm.declaration_attribute add_force_thm; +val eqvt_force_del = Thm.declaration_attribute del_force_thm; val setup = - Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) - "equivariance theorem declaration" - #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) - "equivariance theorem declaration (without checking the form of the lemma)" - #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) + Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + (cat_lines ["declaration of equivariance lemmas - they will automtically be", + "brought into the form p o c = c"]) #> + Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) + (cat_lines ["declaration of equivariance lemmas - they will will be", + "added/deleted directly to the eqvt thm-list"]) #> + PureThy.add_thms_dynamic (@{binding "eqvt"}, content); end;