nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:0f0335d91456
+:1c3ad1256f16
 done
 lemma fundef_ex1_eqvt:
 fixes x::"'a::pt"
 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+assumes eqvt: "eqvt G"
 assumes ex1: "\<exists>!y. G x y"
-assumes eqvt: "eqvt G"
 shows "(p \<bullet> (f x)) = f (p \<bullet> 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 == (\<lambda>x::'a. THE_default d (G x))"
+assumes eqvt: "eqvt G"
+assumes ex1: "\<exists>!y. G x y"
+shows "eqvt_at f x"
+unfolding eqvt_at_def
+using assms
+apply(auto intro: fundef_ex1_eqvt)
+done
 ML {*
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if ! trace then tracing (msg ()) else ()
 ML {*
 (** building proof obligations *)
 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')
 val RCs_rhs  = find_calls2 fvar rhs
 |> curry abstract_over fvar
 |> curry subst_bound f
 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
 *}
 ML {*
 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
 *}
 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 =
 let
 val compat = lookup_compat_thm j i cts
 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" *)
 end
 else
 let
 val compat = lookup_compat_thm i j cts
 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)
 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
 end
 in
 (exactly_one, function_value)
 end
 *}
-(* AAA *)
+ML Thm.forall_elim_vars
-ML {*
+ML {* (ex1_implies_ex, ex1_implies_un) *}
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
+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
 val Globals {h, domT, ranT, x, ...} = globals
 val thy = ProofContext.theory_of ctxt
 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
 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
 |> Goal.protect
 |> fold_rev (Thm.implies_intr o cprop_of) compat
 *)
 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 ("compat_store:\n" ^ @{make_string} compat_store)
 *)
 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
 fun mk_partial_rules provedgoal =

changeset 2655	1c3ad1256f16
parent 2654	0f0335d91456
child 2656	33a6b690fb53