# HG changeset patch # User Christian Urban # Date 1294551533 0 # Node ID 1c3ad1256f16f00d3f3e98367f5e57623badc8a1 # Parent 0f0335d91456c8169c1b84c726a3d0b798161987 instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis diff -r 0f0335d91456 -r 1c3ad1256f16 Nominal/Ex/LamTest.thy --- a/Nominal/Ex/LamTest.thy Sun Jan 09 04:28:24 2011 +0000 +++ b/Nominal/Ex/LamTest.thy Sun Jan 09 05:38:53 2011 +0000 @@ -35,8 +35,8 @@ 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" - assumes eqvt: "eqvt G" shows "(p \ (f x)) = f (p \ x)" apply (simp only: f_def) apply(subst the_default_eqvt) @@ -46,7 +46,16 @@ 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 {* @@ -161,11 +170,13 @@ fun mk_compat_proof_obligations domT ranT fvar f glrs = let + (* val _ = tracing ("domT: " ^ @{make_string} domT) 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')) = let val shift = incr_boundvars (length qs') @@ -186,7 +197,8 @@ end in map mk_impl (unordered_pairs glrs) - |> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts))) + (*|> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts))) + *) end *} @@ -296,9 +308,6 @@ 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 @@ -308,7 +317,6 @@ |> eqvt_at_elim end | _ => thm - end *} ML {* @@ -330,10 +338,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)) + (*|> 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)) + (*|> 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" *) @@ -344,10 +352,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)) + (*|> 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)) + (*|> 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) @@ -491,10 +499,13 @@ end *} -(* AAA *) +ML Thm.forall_elim_vars + +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 f_def = +fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def = let val Globals {h, domT, ranT, x, ...} = globals val thy = ProofContext.theory_of ctxt @@ -510,40 +521,45 @@ val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |> 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\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 _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt) 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 + |> tap (fn th => tracing ("A\n" ^ @{make_string} th)) |> Thm.forall_elim_vars 0 + |> tap (fn th => tracing ("B\n" ^ @{make_string} th)) |> fold (curry op COMP) ex1s + |> tap (fn th => tracing ("C\n" ^ @{make_string} th)) |> Thm.implies_intr (ihyp) + |> tap (fn th => tracing ("D\n" ^ @{make_string} th)) |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) + |> tap (fn th => tracing ("E\n" ^ @{make_string} th)) |> Thm.forall_intr (cterm_of thy x) + |> tap (fn th => tracing ("F\n" ^ @{make_string} th)) |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) + |> tap (fn th => tracing ("G\n" ^ @{make_string} th)) |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) + |> tap (fn th => tracing ("H\n" ^ @{make_string} th)) + val goalstate = Conjunction.intr graph_is_function complete |> Thm.close_derivation @@ -1055,7 +1071,9 @@ 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 @@ -1096,9 +1114,10 @@ val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat - compat_store G_elim) f_defthm + compat_store G_elim G_eqvt) f_defthm val _ = tracing ("goalstate prove_stuff thm:\n" ^ @{make_string} goalstate) + val _ = tracing ("values prove_stuff thms:\n" ^ cat_lines (map @{make_string} values)) val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses