# HG changeset patch # User Christian Urban # Date 1295267617 0 # Node ID 7c5bca97888683a312a7cbc7b7b979a8c91308ec # Parent 16896fd8eff5fc6e2155006eb115a51ad3ef32c0 eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation diff -r 16896fd8eff5 -r 7c5bca978886 Nominal/Ex/LamTest.thy --- a/Nominal/Ex/LamTest.thy Sat Jan 15 21:16:15 2011 +0000 +++ b/Nominal/Ex/LamTest.thy Mon Jan 17 12:33:37 2011 +0000 @@ -9,86 +9,6 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l -definition - "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" - -lemma supp_eqvt_at: - assumes asm: "eqvt_at f x" - and fin: "finite (supp x)" - shows "supp (f x) \ supp x" -apply(rule supp_is_subset) -unfolding supports_def -unfolding fresh_def[symmetric] -using asm -apply(simp add: eqvt_at_def) -apply(simp add: swap_fresh_fresh) -apply(rule fin) -done - -lemma finite_supp_eqvt_at: - assumes asm: "eqvt_at f x" - and fin: "finite (supp x)" - shows "finite (supp (f x))" -apply(rule finite_subset) -apply(rule supp_eqvt_at[OF asm fin]) -apply(rule fin) -done - -lemma fresh_eqvt_at: - assumes asm: "eqvt_at f x" - and fin: "finite (supp x)" - and fresh: "as \* x" - shows "as \* f x" -using fresh -unfolding fresh_star_def -unfolding fresh_def -using supp_eqvt_at[OF asm fin] -by auto - -definition - "eqvt f \ \p. p \ f = f" - -lemma eqvtI: - "(\p. p \ f \ f) \ eqvt f" -apply(auto simp add: eqvt_def) -done - -lemma the_default_eqvt: - assumes unique: "\!x. P x" - shows "(p \ (THE_default d P)) = (THE_default d (p \ P))" - apply(rule THE_default1_equality [symmetric]) - apply(rule_tac p="-p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel) - apply(rule unique) - apply(rule_tac p="-p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel) - apply(rule THE_defaultI'[OF unique]) - done - -lemma fundef_ex1_eqvt: - fixes x::"'a::pt" - assumes f_def: "f == (\x::'a. THE_default d (G x))" - assumes eqvt: "eqvt G" - assumes ex1: "\!y. G x y" - shows "(p \ (f x)) = f (p \ x)" - apply (simp only: f_def) - apply(subst the_default_eqvt) - apply (rule ex1) - apply(perm_simp) - using eqvt - apply(simp add: eqvt_def) - done - -lemma fundef_ex1_eqvt_at: - fixes x::"'a::pt" - assumes f_def: "f == (\x::'a. THE_default d (G x))" - assumes eqvt: "eqvt G" - assumes ex1: "\!y. G x y" - shows "eqvt_at f x" - unfolding eqvt_at_def - using assms - apply(auto intro: fundef_ex1_eqvt) - done ML {* @@ -333,33 +253,6 @@ *} ML {* -fun pp_thm thm = - let - val hyps = Thm.hyps_of thm - val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of thm) - in - (@{make_string} thm) ^ "\n hyps: " ^ (commas (map (Syntax.string_of_term @{context}) hyps)) - ^ " tpairs: " ^ (commas (map (Syntax.string_of_term @{context}) tpairs)) - end -*} - - -ML {* -fun eqvt_at_elim thy (eqvts:thm list) thm = - case (prop_of thm) of - Const ("==>", _) $ (t as (@{term Trueprop} $ (Const (@{const_name eqvt_at}, _) $ _ $ _))) $ _ => - let - val el_thm = Skip_Proof.make_thm thy t - val _ = tracing ("NEED TO PROVE " ^ @{make_string} el_thm) - val _ = tracing ("HAVE\n" ^ cat_lines (map @{make_string} eqvts)) - in - Thm.elim_implies el_thm thm - |> eqvt_at_elim thy eqvts - end - | _ => thm -*} - -ML {* (* expects i <= j *) fun lookup_compat_thm i j cts = nth (nth cts (i - 1)) (j - i) @@ -375,12 +268,10 @@ in if j < i then let val compat = lookup_compat_thm j i cts - val _ = tracing ("XXXX compat clause if:\n" ^ @{make_string} compat) in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.elim_implies (rev eqvtsj) (* HERE *) - (*|> eqvt_at_elim thy eqvtsj *) |> 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" *) @@ -388,12 +279,10 @@ else let val compat = lookup_compat_thm i j cts - (* val _ = tracing ("XXXX compat clause else:\n" ^ @{make_string} compat) *) in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.elim_implies (rev eqvtsi) (* HERE *) - (* |> eqvt_at_elim thy eqvtsi *) |> fold Thm.elim_implies agsi |> fold Thm.elim_implies agsj |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) @@ -462,10 +351,9 @@ ML {* fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj = let - val _ = tracing "START" - val Globals {h, y, x, fvar, ...} = globals - val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei + val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, + ags = agsi, ...}, ...} = clausei val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = @@ -480,8 +368,6 @@ val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) - val _ = tracing "POINT B" - val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj'] val RLj_import = RLj @@ -489,64 +375,38 @@ |> fold Thm.elim_implies agsj' |> fold Thm.elim_implies Ghsj' - val _ = tracing "POINT C" - val eqvtsi = nth eqvts (i - 1) |> map (fold Thm.forall_elim cqsi) |> map (fold Thm.elim_implies [case_hyp]) |> map (fold Thm.elim_implies agsi) - val _ = tracing "POINT D" - val eqvtsj = nth eqvts (j - 1) - |> tap (fn thms => tracing ("O1:\n" ^ cat_lines (map @{make_string} thms))) |> map (fold Thm.forall_elim cqsj') - |> tap (fn thms => tracing ("O2:\n" ^ cat_lines (map @{make_string} thms))) |> map (fold Thm.elim_implies [case_hypj']) - |> tap (fn thms => tracing ("O3:\n" ^ cat_lines (map @{make_string} thms))) |> map (fold Thm.elim_implies agsj') - val _ = tracing ("eqvtsi:\n" ^ cat_lines (map @{make_string} eqvtsi)) - val _ = tracing ("eqvtsj:\n" ^ cat_lines (map @{make_string} eqvtsj)) - val _ = tracing ("case_hypi:\n" ^ @{make_string} case_hyp) - val _ = tracing ("case_hypj:\n" ^ @{make_string} case_hypj') - val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj - - val _ = tracing ("compats:\n" ^ pp_thm compat) - - fun pppp str = tap (fn thm => tracing (str ^ ": " ^ pp_thm thm)) - fun ppp str = I in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) - |> pppp "A" |> Thm.implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) - |> pppp "B" |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) - |> pppp "C" |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) - |> pppp "D" |> fold_rev (Thm.implies_intr o cprop_of) Ghsj' - |> pppp "E" |> fold_rev (Thm.implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) - |> pppp "F" |> Thm.implies_intr (cprop_of y_eq_rhsj'h) - |> pppp "G" |> Thm.implies_intr (cprop_of lhsi_eq_lhsj') - |> pppp "H" |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') - |> pppp "I" end *} ML {* -fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas eqvt_lemmas clausei = +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei = let val Globals {x, y, ranT, fvar, ...} = globals val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei @@ -565,9 +425,7 @@ val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = - map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas - - val _ = tracing ("DONE unique clauses") + map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems fun elim_implies_eta A AB = Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single @@ -605,9 +463,6 @@ *} -ML {* (ex1_implies_ex, ex1_implies_un) *} -thm fundef_ex1_eqvt_at - ML {* fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def = let @@ -627,13 +482,6 @@ |> instantiate' [] [NONE, SOME (cterm_of thy h)] val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) - (* - val _ = tracing ("ihyp_thm\n" ^ pp_thm ihyp_thm) - val _ = tracing ("ih_intro\n" ^ pp_thm ih_intro) - val _ = tracing ("ih_elim\n" ^ pp_thm ih_elim) - val _ = tracing ("ih_eqvt\n" ^ pp_thm ih_eqvt) - *) - val _ = trace_msg (K "Proving Replacement lemmas...") val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses @@ -666,10 +514,9 @@ *} - ML {* (* wrapper -- restores quantifiers in rule specifications *) -fun inductive_def (binding as ((R, T), _)) intrs lthy = +fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy = let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = lthy @@ -689,8 +536,14 @@ [] (* no special monos *) ||> Local_Theory.restore_naming lthy - val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy - val eqvt_thm' = (Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI} + val eqvt_thm' = + if eqvt_flag = false then NONE + else + let + 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 = @@ -730,7 +583,7 @@ val G_intros = map2 mk_GIntro clauses RCss in - inductive_def ((Binding.name n, T), NoSyn) G_intros lthy + inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy end *} @@ -762,10 +615,10 @@ val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss - val ((R, RIntro_thms, R_elim, _, R_eqvt), lthy) = - inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy + val ((R, RIntro_thms, R_elim, _, _), lthy) = + inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy in - ((R, Library.unflat R_intross RIntro_thms, R_elim, R_eqvt), lthy) + ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) end @@ -1145,39 +998,18 @@ val trees = map build_tree clauses val RCss = map find_calls trees - val ((G, GIntro_thms, G_elim, G_induct, G_eqvt), lthy) = + val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy - (* - val _ = tracing ("Graph - name: " ^ pp_thm G) - val _ = tracing ("Graph intros:\n" ^ cat_lines (map pp_thm GIntro_thms)) - val _ = tracing ("Graph Equivariance " ^ pp_thm 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: " ^ pp_thm f) - val _ = tracing ("f_defthm:\n" ^ pp_thm 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 pp_thm RCss)) - *) - - val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) = + val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy - (* - val _ = tracing ("Relation - name: " ^ pp_thm R) - val _ = tracing ("Relation intros:\n" ^ cat_lines (map pp_thm RIntro_thmss)) - val _ = tracing ("Relation Equivariance " ^ pp_thm R_eqvt) - *) - val (_, lthy) = Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy @@ -1199,13 +1031,6 @@ val compat_store = store_compat_thms n compat - (* - val _ = tracing ("globals:\n" ^ pp_thm globals) - val _ = tracing ("complete:\n" ^ pp_thm complete) - val _ = tracing ("compat:\n" ^ pp_thm compat) - val _ = tracing ("compat_store:\n" ^ pp_thm compat_store) - *) - val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim G_eqvt) f_defthm @@ -1352,16 +1177,6 @@ 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} @@ -1642,11 +1457,6 @@ end *} -ML {* - Proof.theorem; - Proof.refine -*} - ML {* fun gen_function is_external prep default_constraint fixspec eqns config lthy =