# HG changeset patch # User Christian Urban # Date 1295978306 -3600 # Node ID 747ebf2f066dd4aa7efde0e452f6c97b7d6b8004 # Parent 8ae1c2e6369eeb08827eb78a4d14468c6fde0b7f made eqvt-proof explicit in the function definitions diff -r 8ae1c2e6369e -r 747ebf2f066d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Jan 25 02:51:44 2011 +0900 +++ b/Nominal/Ex/Lambda.thy Tue Jan 25 18:58:26 2011 +0100 @@ -17,6 +17,7 @@ "height (Var x) = 1" | "height (App t1 t2) = max (height t1) (height t2) + 1" | "height (Lam [x].t) = height t + 1" +defer apply(rule_tac y="x" in lam.exhaust) apply(auto simp add: lam.distinct lam.eq_iff) apply(simp add: Abs_eq_iff alphas) @@ -24,11 +25,39 @@ apply(subst (4) supp_perm_eq[where p="p", symmetric]) apply(simp add: pure_supp fresh_star_def) apply(simp add: eqvt_at_def) +apply(subgoal_tac "\p x r. height_graph x r \ height_graph (p \ x) (p \ r)") +unfolding eqvt_def +apply(rule allI) +apply(simp add: permute_fun_def) +apply(rule ext) +apply(rule ext) +apply(simp add: permute_bool_def) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \ x" in meta_spec) +apply(drule_tac x="- p \ xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +apply(erule height_graph.induct) +apply(perm_simp) +apply(rule height_graph.intros) +apply(perm_simp) +apply(rule height_graph.intros) +apply(assumption) +apply(assumption) +apply(perm_simp) +apply(rule height_graph.intros) +apply(assumption) done termination by (relation "measure size") (simp_all add: lam.size) +thm height.simps + text {* free name function - returns atom lists *} @@ -38,6 +67,7 @@ "frees_lst (Var x) = [atom x]" | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" +defer apply(rule_tac y="x" in lam.exhaust) apply(simp_all)[3] apply(simp_all only: lam.distinct) @@ -57,6 +87,32 @@ apply(auto simp add: fresh_star_def)[1] unfolding eqvt_at_def apply(simp only: removeAll_eqvt atom_eqvt) +apply(subgoal_tac "\p x r. frees_lst_graph x r \ frees_lst_graph (p \ x) (p \ r)") +unfolding eqvt_def +apply(rule allI) +apply(simp add: permute_fun_def) +apply(rule ext) +apply(rule ext) +apply(simp add: permute_bool_def) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \ x" in meta_spec) +apply(drule_tac x="- p \ xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +apply(erule frees_lst_graph.induct) +apply(perm_simp) +apply(rule frees_lst_graph.intros) +apply(perm_simp) +apply(rule frees_lst_graph.intros) +apply(assumption) +apply(assumption) +apply(perm_simp) +apply(rule frees_lst_graph.intros) +apply(assumption) done termination @@ -79,6 +135,7 @@ "(Var x)[y ::= s] = (if x = y then s else (Var x))" | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" | "atom x \ (y, s) \ (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" +defer apply(auto simp add: lam.distinct lam.eq_iff) apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) apply(blast)+ @@ -115,6 +172,33 @@ apply(simp add: Abs_fresh_iff) apply(drule sym) apply(simp add: Abs_fresh_iff) +apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") +unfolding eqvt_def +apply(rule allI) +apply(simp add: permute_fun_def) +apply(rule ext) +apply(rule ext) +apply(simp add: permute_bool_def) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \ x" in meta_spec) +apply(drule_tac x="- p \ xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +apply(erule subst_graph.induct) +apply(perm_simp) +apply(rule subst_graph.intros) +apply(perm_simp) +apply(rule subst_graph.intros) +apply(assumption) +apply(assumption) +apply(perm_simp) +apply(rule subst_graph.intros) +apply(simp add: fresh_Pair) +apply(assumption) done termination @@ -249,6 +333,7 @@ "trans (Var x) xs = lookup xs 0 x" | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" | "atom x \ xs \ trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" +defer apply(case_tac x) apply(simp) apply(rule_tac y="a" and c="b" in lam.strong_exhaust) @@ -335,53 +420,13 @@ apply(simp_all add: permute_pure) done -ML {* -Nominal_Function_Core.trace := true -*} - (* -inductive - trans_graph -where - "trans_graph (Var x, xs) (index xs 0 (atom x) \= (\v. Some (DBVar v)))" -| "\trans_graph (t1, xs) (trans_sum (t1, xs)); - \a. trans_sum (t1, xs) = Some a \ trans_graph (t2, xs) (trans_sum (t2, xs))\ - \ trans_graph (App t1 t2, xs) - (trans_sum (t1, xs) \= (\v. trans_sum (t2, xs) \= (\va. Some (DBApp v va))))" -| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \ - trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \= (\v. Some (DBLam v)))" - -lemma - assumes a: "trans_graph x t" - shows "trans_graph (p \ x) (p \ t)" -using a -apply(induct) -apply(perm_simp) -apply(rule trans_graph.intros) -apply(perm_simp) -apply(rule trans_graph.intros) -apply(simp) -apply(simp) -defer -apply(perm_simp) -apply(rule trans_graph.intros) -apply(simp) -apply(rotate_tac 3) -apply(drule_tac x="FOO" in meta_spec) -apply(drule meta_mp) -prefer 2 -apply(simp) - -equivariance trans_graph -*) - -(* equivariance fails at the moment nominal_primrec trans :: "lam \ atom list \ db option" where "trans (Var x) xs = (index xs 0 (atom x) \= (\n. Some (DBVar n)))" -| "trans (App t1 t2) xs = (trans t1 xs \= (\db1. trans t2 xs \= (\db2. Some (DBApp db1 db2))))" -| "trans (Lam x t) xs = (trans t (atom x # xs) \= (\db. Some (DBLam db)))" +| "trans (App t1 t2) xs = ((trans t1 xs) \= (\db1. (trans t2 xs) \= (\db2. Some (DBApp db1 db2))))" +| "trans (Lam [x].t) xs = (trans t (atom x # xs) \= (\db. Some (DBLam db)))" *) diff -r 8ae1c2e6369e -r 747ebf2f066d Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Jan 25 02:51:44 2011 +0900 +++ b/Nominal/Ex/TypeSchemes.thy Tue Jan 25 18:58:26 2011 +0100 @@ -28,6 +28,60 @@ thm ty_tys.supp thm ty_tys.fresh +fun + lookup :: "(name \ ty) list \ name \ ty" +where + "lookup [] Y = Var Y" +| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" + +lemma lookup_eqvt[eqvt]: + shows "(p \ lookup Ts T) = lookup (p \ Ts) (p \ T)" +apply(induct Ts T rule: lookup.induct) +apply(simp_all) +done + +nominal_primrec + subst :: "(name \ ty) list \ ty \ ty" +and substs :: "(name \ ty) list \ tys \ tys" +where + "subst \ (Var X) = lookup \ X" +| "subst \ (Fun T1 T2) = Fun (subst \ T1) (subst \ T2)" +| "fset (map_fset atom xs) \* \ \ substs \ (All xs T) = All xs (subst \ T)" +term subst_substs_sumC +term Inl +thm subst_substs_graph.induct +thm subst_substs_graph.intros +thm Projl.simps +apply(subgoal_tac "\p x r. subst_substs_graph x r \ subst_substs_graph (p \ x) (p \ r)") +apply(simp add: eqvt_def) +apply(rule allI) +apply(simp add: permute_fun_def permute_bool_def) +apply(rule ext) +apply(rule ext) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \ x" in meta_spec) +apply(drule_tac x="- p \ xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +thm subst_substs_graph.induct +thm subst_substs_graph.intros +thm Projl.simps +apply(erule subst_substs_graph.induct) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(simp only: eqvts) +thm Projl.simps +term Inl +term Inr +apply(perm_simp) +thm subst_substs_graph.intros +thm Projl.simps +oops + section {* defined as two separate nominal datatypes *} @@ -52,22 +106,23 @@ thm tys2.fresh fun - lookup :: "(name \ ty2) list \ name \ ty2" + lookup2 :: "(name \ ty2) list \ name \ ty2" where - "lookup [] Y = Var2 Y" -| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" + "lookup2 [] Y = Var2 Y" +| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)" -lemma lookup_eqvt[eqvt]: - shows "(p \ lookup Ts T) = lookup (p \ Ts) (p \ T)" -apply(induct Ts T rule: lookup.induct) +lemma lookup2_eqvt[eqvt]: + shows "(p \ lookup2 Ts T) = lookup2 (p \ Ts) (p \ T)" +apply(induct Ts T rule: lookup2.induct) apply(simp_all) done -function +nominal_primrec subst :: "(name \ ty2) list \ ty2 \ ty2" where - "subst \ (Var2 X) = lookup \ X" + "subst \ (Var2 X) = lookup2 \ X" | "subst \ (Fun2 T1 T2) = Fun2 (subst \ T1) (subst \ T2)" +defer apply(case_tac x) apply(simp) apply(rule_tac y="b" in ty2.exhaust) @@ -76,6 +131,28 @@ apply(simp_all add: ty2.distinct) apply(simp add: ty2.eq_iff) apply(simp add: ty2.eq_iff) +apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") +apply(simp add: eqvt_def) +apply(rule allI) +apply(simp add: permute_fun_def permute_bool_def) +apply(rule ext) +apply(rule ext) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \ x" in meta_spec) +apply(drule_tac x="- p \ xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +apply(erule subst_graph.induct) +apply(perm_simp) +apply(rule subst_graph.intros) +apply(perm_simp) +apply(rule subst_graph.intros) +apply(assumption) +apply(assumption) done termination @@ -86,14 +163,14 @@ lemma subst_eqvt[eqvt]: shows "(p \ subst \ T) = subst (p \ \) (p \ T)" apply(induct \ T rule: subst.induct) -apply(simp_all add: lookup_eqvt) +apply(simp_all add: lookup2_eqvt) done lemma j: assumes "a \ Ts" " a \ X" - shows "a \ lookup Ts X" + shows "a \ lookup2 Ts X" using assms -apply(induct Ts X rule: lookup.induct) +apply(induct Ts X rule: lookup2.induct) apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair) done diff -r 8ae1c2e6369e -r 747ebf2f066d Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Tue Jan 25 02:51:44 2011 +0900 +++ b/Nominal/nominal_function_core.ML Tue Jan 25 18:58:26 2011 +0100 @@ -115,6 +115,14 @@ |> HOLogic.mk_Trueprop end +fun mk_eqvt trm = + let + val ty = fastype_of trm + in + Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm + |> HOLogic.mk_Trueprop + end + (* nominal *) fun find_calls2 f t = let @@ -496,18 +504,19 @@ |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) - val goalstate = Conjunction.intr graph_is_function complete + val goalstate = + Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt |> Thm.close_derivation |> Goal.protect |> fold_rev (Thm.implies_intr o cprop_of) compat |> Thm.implies_intr (cprop_of complete) + |> Thm.implies_intr (cprop_of G_eqvt) in (goalstate, values) end -(* nominal *) (* wrapper -- restores quantifiers in rule specifications *) -fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy = +fun inductive_def (binding as ((R, T), _)) intrs lthy = let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = lthy @@ -527,16 +536,6 @@ [] (* no special monos *) ||> Local_Theory.restore_naming lthy - val eqvt_thm' = - if eqvt_flag = false then NONE - else - let - (* val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) *) - val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy - in - SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}) - end - val cert = cterm_of (ProofContext.theory_of lthy) fun requantify orig_intro thm = let @@ -550,7 +549,7 @@ forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm end in - ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy) + ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) end (* nominal *) @@ -574,7 +573,7 @@ val G_intros = map2 mk_GIntro clauses RCss in - inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy + inductive_def ((Binding.name n, T), NoSyn) G_intros lthy end fun define_function fdefname (fname, mixfix) domT ranT G default lthy = @@ -605,8 +604,8 @@ val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss - val ((R, RIntro_thms, R_elim, _, _), lthy) = - inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy + val ((R, RIntro_thms, R_elim, _), lthy) = + inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy in ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) end @@ -988,7 +987,7 @@ val trees = map build_tree clauses val RCss = map find_calls trees - val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) = + val ((G, GIntro_thms, G_elim, G_induct), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = @@ -1019,6 +1018,8 @@ mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> Thm.assume) + val G_eqvt = mk_eqvt G |> cert |> Thm.assume + val compat_store = store_compat_thms n compat val (goalstate, values) = PROFILE "prove_stuff" @@ -1032,10 +1033,11 @@ let val newthy = theory_of_thm provedgoal (*FIXME*) - val (graph_is_function, complete_thm) = + val ((graph_is_function, complete_thm), _) = provedgoal |> Conjunction.elim - |> apfst (Thm.forall_elim_vars 0) + |>> Conjunction.elim + |>> apfst (Thm.forall_elim_vars 0) val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)