# HG changeset patch # User Christian Urban # Date 1271233796 -7200 # Node ID ac8cb569a17bcaf70cff48f8ee7a362c42df13d0 # Parent f374ffd50c7c5fabe9de95a37df3422be77bb6b9# Parent faa7e6033f2e5fef09df5a9b5d511f0eadf4b900 merged diff -r faa7e6033f2e -r ac8cb569a17b Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 08:42:38 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 10:29:56 2010 +0200 @@ -371,144 +371,4 @@ (* apply(perm_strict_simp) *) oops -atom_decl var - -ML {* -val inductive_atomize = @{thms induct_atomize}; - -val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps inductive_atomize); -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); -fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); - -fun map_term f t u = (case f t u of - NONE => map_term' f t u | x => x) -and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of - (NONE, NONE) => NONE - | (SOME t'', NONE) => SOME (t'' $ u) - | (NONE, SOME u'') => SOME (t $ u'') - | (SOME t'', SOME u'') => SOME (t'' $ u'')) - | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of - NONE => NONE - | SOME t'' => SOME (Abs (s, T, t''))) - | map_term' _ _ _ = NONE; - - -fun map_thm ctxt f tac monos opt th = - let - val prop = prop_of th; - fun prove t = - Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) - in Option.map prove (map_term f prop (the_default prop opt)) end; - -fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of - Const (name, _) => - if name mem names then SOME (f p q) else NONE - | _ => NONE) - | split_conj _ _ _ _ = NONE; -*} - -ML {* -val perm_bool = @{thm "permute_bool_def"}; -val perm_boolI = @{thm "permute_boolI"}; -val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb - (Drule.strip_imp_concl (cprop_of perm_boolI)))); - -fun mk_perm_bool pi th = th RS Drule.cterm_instantiate - [(perm_boolI_pi, pi)] perm_boolI; - -*} - -ML {* -fun transp ([] :: _) = [] - | transp xs = map hd xs :: transp (map tl xs); - -fun prove_eqvt s xatoms ctxt = - let - val thy = ProofContext.theory_of ctxt; - val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy s); - val raw_induct = atomize_induct ctxt raw_induct; - val elims = map (atomize_induct ctxt) elims; - val intrs = map atomize_intr intrs; - val monos = Inductive.get_monos ctxt; - val intrs' = Inductive.unpartition_rules intrs - (map (fn (((s, ths), (_, k)), th) => - (s, ths ~~ Inductive.infer_intro_vars th k ths)) - (Inductive.partition_rules raw_induct intrs ~~ - Inductive.arities_of raw_induct ~~ elims)); - val k = length (Inductive.params_of raw_induct); - val atoms' = ["var"]; - val atoms = - if null xatoms then atoms' else - let val atoms = map (Sign.intern_type thy) xatoms - in - (case duplicates op = atoms of - [] => () - | xs => error ("Duplicate atoms: " ^ commas xs); - case subtract (op =) atoms' atoms of - [] => () - | xs => error ("No such atoms: " ^ commas xs); - atoms) - end; - val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; - val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps - (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp); - val (([t], [pi]), ctxt') = ctxt |> - Variable.import_terms false [concl_of raw_induct] ||>> - Variable.variant_fixes ["pi"]; - val ps = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); - fun eqvt_tac ctxt'' pi (intr, vs) st = - let - fun eqvt_err s = - let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt - in error ("Could not prove equivariance for introduction rule\n" ^ - Syntax.string_of_term ctxt''' t ^ "\n" ^ s) - end; - val res = SUBPROOF (fn {prems, params, ...} => - let - val prems' = map (fn th => the_default th (map_thm ctxt' - (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; - val prems'' = map (fn th => Simplifier.simplify eqvt_ss - (mk_perm_bool (cterm_of thy pi) th)) prems'; - val intr' = intr - in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 - end) ctxt' 1 st - in - case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of - NONE => eqvt_err ("Rule does not match goal\n" ^ - Syntax.string_of_term ctxt'' (hd (prems_of st))) - | SOME (th, _) => Seq.single th - end; - val thss = map (fn atom => - let val pi' = Free (pi, @{typ perm}) - in map (fn th => zero_var_indexes (th RS mp)) - (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => - let - val (h, ts) = strip_comb p; - val (ts1, ts2) = chop k ts - in - HOLogic.mk_imp (p, list_comb (h, ts1)) - end) ps))) - (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => - full_simp_tac eqvt_ss 1 THEN - eqvt_tac context pi' intr_vs) intrs')) |> - singleton (ProofContext.export ctxt' ctxt))) - end) atoms - in - ctxt |> - Local_Theory.notes (map (fn (name, ths) => - ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), - [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])])) - (names ~~ transp thss)) |> snd - end; -*} - end diff -r faa7e6033f2e -r ac8cb569a17b Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Apr 14 08:42:38 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Wed Apr 14 10:29:56 2010 +0200 @@ -120,63 +120,132 @@ "valid []" | "\atom x \ Gamma; valid Gamma\ \ valid ((x, T)#Gamma)" +inductive + typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) +where + t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" + | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" + | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" + + ML {* -fun my_tac ctxt intros = - Nominal_Permeq.eqvt_strict_tac ctxt [] [] - THEN' resolve_tac intros - THEN_ALL_NEW - (atac ORELSE' - EVERY' - [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), - Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], - atac ]) +fun map_term f t = + (case f t of + NONE => map_term' f t + | x => x) +and map_term' f (t $ u) = + (case (map_term f t, map_term f u) of + (NONE, NONE) => NONE + | (SOME t'', NONE) => SOME (t'' $ u) + | (NONE, SOME u'') => SOME (t $ u'') + | (SOME t'', SOME u'') => SOME (t'' $ u'')) + | map_term' f (Abs (s, T, t)) = + (case map_term f t of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ = NONE; + +fun map_thm_tac ctxt tac thm = +let + val monos = Inductive.get_monos ctxt +in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] +end + +(* + proves F[f t] from F[t] where F[t] is the given theorem + + - F needs to be monotone + - f returns either SOME for a term it fires + and NONE elsewhere +*) +fun map_thm ctxt f tac thm = +let + val opt_goal_trm = map_term f (prop_of thm) + fun prove goal = + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) +in + case opt_goal_trm of + NONE => thm + | SOME goal => prove goal +end + +fun transform_prem ctxt names thm = +let + fun split_conj names (Const ("op &", _) $ p $ q) = + (case head_of p of + Const (name, _) => if name mem names then SOME q else NONE + | _ => NONE) + | split_conj _ _ = NONE; +in + map_thm ctxt (split_conj names) (etac conjunct2 1) thm +end *} +ML {* +open Nominal_Permeq +*} + +ML {* +fun single_case_tac ctxt pred_names pi intro = +let + val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE} +in + eqvt_strict_tac ctxt [] [] THEN' + SUBPROOF (fn {prems, context as ctxt, ...} => + let + val prems' = map (transform_prem ctxt pred_names) prems + val side_cond_tac = EVERY' + [ rtac rule, + eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], + resolve_tac prems' ] + in + HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) + end) ctxt +end +*} + +ML {* +fun eqvt_rel_tac pred_name = +let + val thy = ProofContext.theory_of ctxt + val ({names, ...}, {raw_induct, intrs, ...}) = + Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + val param_no = length (Inductive.params_of raw_induct) + val (([raw_concl], [pi]), ctxt') = + ctxt |> Variable.import_terms false [concl_of raw_induct] + ||>> Variable.variant_fixes ["pi"]; + val preds = map (fst o HOLogic.dest_imp) + (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); +in + +end +*} + + + lemma [eqvt]: assumes a: "valid Gamma" shows "valid (p \ Gamma)" using a apply(induct) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -done - -lemma - shows "valid Gamma \ valid (p \ Gamma)" -ML_prf {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid") -*} -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *}) +apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *}) done - -thm eqvts -thm eqvts_raw - -inductive - typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) -where - t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" - - -ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} - lemma shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" ML_prf {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = +val ({names, ...}, {raw_induct, ...}) = Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *} apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -oops +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *}) +apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *}) +done lemma uu[eqvt]: assumes a: "Gamma \ t : T"