# HG changeset patch # User Christian Urban # Date 1294535864 0 # Node ID d0f774d06e6eaf637b58c58866de5743cb09eeb3 # Parent e9a2770660ef9b16e8f32e6b13aef0238069d4f5 added eqvt_at premises in function definition - however not proved at the moment diff -r e9a2770660ef -r d0f774d06e6e Nominal/Ex/LamTest.thy --- a/Nominal/Ex/LamTest.thy Fri Jan 07 05:40:31 2011 +0000 +++ b/Nominal/Ex/LamTest.thy Sun Jan 09 01:17:44 2011 +0000 @@ -10,15 +10,16 @@ | Lam x::"name" l::"lam" bind x in l definition - "eqvt x \ \p. p \ x = x" + "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" + +definition + "eqvt f \ \p. p \ f = f" lemma eqvtI: - "(\p. p \ x \ x) \ eqvt x" + "(\p. p \ f \ f) \ eqvt f" apply(auto simp add: eqvt_def) done -term THE_default - lemma the_default_eqvt: assumes unique: "\!x. P x" shows "(p \ (THE_default d P)) = (THE_default d (p \ P))" @@ -49,7 +50,6 @@ ML {* - val trace = Unsynchronized.ref false fun trace_msg msg = if ! trace then tracing (msg ()) else () @@ -134,15 +134,27 @@ *} ML {* -fun mk_eqvt trm = +fun mk_eqvt_at (f_trm, arg_trm) = let - val ty = fastype_of trm + val f_ty = fastype_of f_trm + val arg_ty = domain_type f_ty in - Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm + Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm |> HOLogic.mk_Trueprop end *} +ML {* +fun find_calls2 f t = + let + fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I) + | aux (Abs (_, _, t)) = aux t + | aux _ = I + in + aux t [] + end +*} + ML {* (** building proof obligations *) @@ -153,16 +165,21 @@ val _ = tracing ("ranT: " ^ @{make_string} ranT) val _ = tracing ("fvar: " ^ @{make_string} fvar) val _ = tracing ("f: " ^ @{make_string} f) - fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = + + fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) = let val shift = incr_boundvars (length qs') + + val RCs_rhs = find_calls2 fvar rhs + val RCs_rhs' = find_calls2 fvar rhs' in Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') - (*|> (curry Logic.mk_implies) (mk_eqvt fvar) *) - |> (curry Logic.mk_implies) @{term "Trueprop True"} (* HERE *) + |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) + |> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs') + (*|> (curry Logic.mk_implies) @{term "Trueprop True"}*) (* HERE *) |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |> curry abstract_over fvar |> curry subst_bound f @@ -276,6 +293,24 @@ end *} + +ML {* +fun eqvt_at_elim thm = + let + val _ = tracing ("term\n" ^ @{make_string} (prop_of thm)) + in + case (prop_of thm) of + Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => + let + val el_thm = Skip_Proof.make_thm @{theory} t + in + Thm.elim_implies el_thm thm + |> eqvt_at_elim + end + | _ => thm + end +*} + ML {* (* expects i <= j *) fun lookup_compat_thm i j cts = @@ -295,8 +330,10 @@ in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - (*|> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *) - |> Thm.elim_implies @{thm TrueI} + |> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th)) + (*|> Thm.elim_implies @{thm TrueI}*) (* THERE *) + |> eqvt_at_elim + |> tap (fn th => tracing ("AFTER " ^ @{make_string} th)) |> fold Thm.elim_implies agsj |> fold Thm.elim_implies agsi |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) @@ -307,8 +344,10 @@ in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - (* |> tap (fn th => tracing ("NEED TO PROVE" ^ @{make_string} th)) *) - |> Thm.elim_implies @{thm TrueI} + |> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th)) + (*|> Thm.elim_implies @{thm TrueI}*) + |> eqvt_at_elim + |> tap (fn th => tracing ("AFTER " ^ @{make_string} th)) |> fold Thm.elim_implies agsi |> fold Thm.elim_implies agsj |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) @@ -317,7 +356,6 @@ end *} -(* WASS *) ML {* (* Generates the replacement lemma in fully quantified form. *) @@ -414,7 +452,9 @@ val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas + (* val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} unique_clauses)) + *) fun elim_implies_eta A AB = Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single @@ -471,23 +511,29 @@ val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |> instantiate' [] [NONE, SOME (cterm_of thy h)] + (* val _ = tracing ("ihyp\n" ^ @{make_string} ihyp) val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm) val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro) val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim) + *) val _ = trace_msg (K "Proving Replacement lemmas...") val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses + (* val _ = tracing (cat_lines (map @{make_string} repLemmas)) + *) val _ = trace_msg (K "Proving cases for unique existence...") val (ex1s, values) = split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) - + + (* val _ = tracing ("ex1s\n" ^ cat_lines (map @{make_string} ex1s)) val _ = tracing ("values\n" ^ cat_lines (map @{make_string} values)) + *) val _ = trace_msg (K "Proving: Graph is a function") val graph_is_function = complete @@ -992,26 +1038,33 @@ val ((G, GIntro_thms, G_elim, G_induct, G_eqvt), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy + (* val _ = tracing ("Graph - name: " ^ @{make_string} G) val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms)) val _ = tracing ("Graph Equivariance " ^ @{make_string} G_eqvt) - + *) val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy + (* val _ = tracing ("f - name: " ^ @{make_string} f) val _ = tracing ("f_defthm:\n" ^ @{make_string} f_defthm) + *) val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees + val _ = tracing ("recursive calls:\n" ^ cat_lines (map @{make_string} RCss)) + val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) = PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy + (* val _ = tracing ("Relation - name: " ^ @{make_string} R) val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss)) val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt) + *) val (_, lthy) = Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy @@ -1029,7 +1082,7 @@ mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume val compat = - mk_compat_proof_obligations domT ranT fvar f abstract_qglrs + mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> Thm.assume) val compat_store = store_compat_thms n compat @@ -1167,7 +1220,9 @@ val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 - val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) + val f_exp = SumTree.mk_proj RST n' i' + (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) + val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) val rew = (n, fold_rev lambda vars f_exp) @@ -1187,11 +1242,23 @@ end val qglrs = map convert_eqs fqgars + + fun pp_f (f, args, precond, lhs, rhs) = + (tracing ("lhs: " ^ commas + (map (fn t => Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), t))) lhs)); + tracing ("rhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), rhs)))) + + fun pp_q (args, precond, lhs, rhs) = + (tracing ("qlhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), lhs))); + tracing ("qrhs: " ^ Syntax.string_of_term ctxt (subst_bounds (map Free (rev args), rhs)))) + in Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} end +*} +ML {* fun define_projections fixes mutual fsum lthy = let fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = @@ -1572,17 +1639,31 @@ apply(case_tac x) apply(simp) apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) -apply(simp_all add: lam.distinct)[3] -apply(auto)[1] +apply(simp add: lam.eq_iff lam.distinct) apply(auto)[1] -apply(simp add: fresh_star_def) -apply(simp_all add: lam.distinct)[5] +apply(simp add: lam.eq_iff lam.distinct) +apply(auto)[1] +apply(simp add: fresh_star_def lam.eq_iff lam.distinct) +apply(simp_all add: lam.distinct) apply(simp add: lam.eq_iff) apply(simp add: lam.eq_iff) apply(simp add: lam.eq_iff) sorry - +(* this should not work *) +nominal_primrec + bnds :: "lam \ name set" +where + "bnds (Var x) = {}" +| "bnds (App t1 t2) = (bnds t1) \ (bnds t2)" +| "bnds (Lam x t) = (bnds t) \ {x}" +apply(rule_tac y="x" in lam.exhaust) +apply(simp_all)[3] +apply(simp_all only: lam.distinct) +apply(simp add: lam.eq_iff) +apply(simp add: lam.eq_iff) +apply(simp add: lam.eq_iff) +sorry end