nominal2: comparison Nominal/nominal_function

equal deleted inserted replaced

-:8ae1c2e6369e
+:747ebf2f066d
 let
 val f_ty = fastype_of f_trm
 val arg_ty = domain_type f_ty
 in
 Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm
+|> 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 =
 |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
 |> Thm.forall_intr (cterm_of thy x)
 |> (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
 |> Local_Theory.conceal
 |> Inductive.add_inductive_i
 [] (* no parameters *)
 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
 [] (* 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
 val (qs, t) = dest_all_all orig_intro
 val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
 in
 fold_rev (fn Free (n, T) =>
 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 *)
 fun define_graph Gname fvar domT ranT clauses RCss lthy =
 let
 |> fold_rev Logic.all (fvar :: qs)
 end
 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 =
 let
 val f_def =
 |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
 (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
-val ((R, RIntro_thms, R_elim, _, _), lthy) =
+val ((R, RIntro_thms, R_elim, _), lthy) =
-inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
 in
 ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
 end
 Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
 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) =
 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 val compat =
 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"
 (prove_stuff lthy globals G f R xclauses complete compat
 compat_store G_elim G_eqvt) f_defthm
 fun mk_partial_rules provedgoal =
 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)
 val psimps = PROFILE "Proving simplification rules"
 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function

changeset 2707	747ebf2f066d
parent 2677	72dfc74b6bd4
child 2709	eb4a2f4078ae