nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:16896fd8eff5
+:7c5bca978886
 nominal_datatype lam =
 Var "name"
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l
-definition
-"eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
-lemma supp_eqvt_at:
-assumes asm: "eqvt_at f x"
-and     fin: "finite (supp x)"
-shows "supp (f x) \<subseteq> 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 \<sharp>* x"
-shows "as \<sharp>* f x"
-using fresh
-unfolding fresh_star_def
-unfolding fresh_def
-using supp_eqvt_at[OF asm fin]
-by auto
-definition
-"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
-lemma eqvtI:
-"(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
-apply(auto simp add: eqvt_def)
-done
-lemma the_default_eqvt:
-assumes unique: "\<exists>!x. P x"
-shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> 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 == (\<lambda>x::'a. THE_default d (G x))"
-assumes eqvt: "eqvt G"
-assumes ex1: "\<exists>!y. G x y"
-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 ()
 (thms1 :: store_compat_thms (n - 1) thms2)
 end
 *}
 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)
 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
 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" *)
 end
 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)
 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
 end
 *}
 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', ...} =
 mk_clause_context x ctxti cdescj
 (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
 val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
 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
 |> fold Thm.forall_elim cqsj'
 |> 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
-end
+*}
-*}
+ML {*
-ML {*
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas eqvt_lemmas clausei =
 let
 val Globals {x, y, ranT, fvar, ...} = globals
 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 val P = cterm_of thy (mk_eq (y, rhsC))
 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
+map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
-val _ = tracing ("DONE unique clauses")
 fun elim_implies_eta A AB =
 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
 val uniqueness = G_cases
 (exactly_one, function_value)
 end
 *}
-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
 val Globals {h, domT, ranT, x, ...} = globals
 val thy = ProofContext.theory_of ctxt
 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_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
 val _ = trace_msg (K "Proving Equivariance lemmas...")
 (goalstate, values)
 end
 *}
 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
 |> 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], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
+val eqvt_thm' =
-val eqvt_thm' = (Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}
+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 =
 let
 val (qs, t) = dest_all_all orig_intro
 |> fold_rev Logic.all (fvar :: qs)
 end
 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
 *}
 ML {*
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
 |> 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, _, R_eqvt), lthy) =
+val ((R, RIntro_thms, R_elim, _, _), lthy) =
-inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) 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
 fun fix_globals domT ranT fvar ctxt =
 let
 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, 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 ((R, RIntro_thmss, R_elim), lthy) =
-val _ = tracing ("recursive calls:\n" ^ cat_lines (map pp_thm 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: " ^ 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
 val newthy = ProofContext.theory_of lthy
 val compat =
 mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
 |> map (cert #> Thm.assume)
 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
 SumTree.mk_inj RST n' i' (replace_frees rews rhs)
 |> Envir.beta_norm)
 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
 *}
 in
 ((goal_state, afterqed), lthy')
 end
 *}
-ML {*
-Proof.theorem;
-Proof.refine
-*}
 ML {*
 fun gen_function is_external prep default_constraint fixspec eqns config lthy =
 let
 val ((goal_state, afterqed), lthy') =

changeset 2662	7c5bca978886
parent 2661	16896fd8eff5
child 3104	f7c4b8e6918b