nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:a8ebcb368a15
+:e5fa8de0e4bd
 | Lam x::"name" l::"lam"  bind x in l
 definition
 "eqvt x \<equiv> \<forall>p. p \<bullet> x = x"
+lemma eqvtI:
+"(\<And>p. p \<bullet> x \<equiv> x) \<Longrightarrow> eqvt x"
+apply(auto simp add: eqvt_def)
+done
 ML {*
 val trace = Unsynchronized.ref false
 in
 rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
 end
 *}
+ML {*
+fun mk_eqvt trm =
+let
+val ty = fastype_of trm
+in
+Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
+|> HOLogic.mk_Trueprop
+end
+*}
 ML {*
 (** building proof obligations *)
 fun mk_compat_proof_obligations domT ranT fvar f glrs =
 in
 Logic.mk_implies
 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+(* HERE |> (curry Logic.mk_implies) (mk_eqvt fvar) *)
 |> (curry Logic.mk_implies) @{term "Trueprop True"}
 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
 |> curry abstract_over fvar
 |> curry subst_bound f
 end
 in
 (thms1 :: store_compat_thms (n - 1) thms2)
 end
 *}
 ML {*
 (* expects i <= j *)
 fun lookup_compat_thm i j cts =
 nth (nth cts (i - 1)) (j - i)
 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
 in if j < i then
 let
-val _ = tracing "then"
 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" *)
 |> Thm.elim_implies @{thm TrueI}
 |> 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 _ = tracing "else"
 val compat = lookup_compat_thm i j cts
-fun pp s (th:thm) = tracing (s ^ " compat thm: " ^ @{make_string} th)
 in
 compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-|> (tap (fn th => pp "*0" th))
 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-|> (tap (fn th => pp "*1" th))
 |> Thm.elim_implies @{thm TrueI}
 |> fold Thm.elim_implies agsi
-|> (tap (fn th => pp "*2" th))
 |> fold Thm.elim_implies agsj
-|> (tap (fn th => pp "*3" th))
 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
-|> (tap (fn th => pp "*4" th))
 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
 end
 end
 *}
 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
-val _ = tracing "1"
 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
-val _ = tracing "1A"
 val compat = get_compat_thm thy compat_store i j cctxi cctxj
-val _ = tracing "1B"
 val Ghsj' = map
 (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
-val _ = tracing "2"
 val RLj_import = RLj
 |> fold Thm.forall_elim cqsj'
 |> fold Thm.elim_implies agsj'
 |> fold Thm.elim_implies Ghsj'
-val _ = tracing "3"
 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 "4"
 in
 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
 |> Thm.implies_elim RLj_import
 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
 |> (fn it => trans OF [it, compat])
 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
-val _ = tracing "A"
 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
 |> fold_rev (Thm.implies_intr o cprop_of) CCas
 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
 val existence = fold (curry op COMP o prep_RC) RCs lGI
-val _ = tracing "B"
 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 _ = tracing "B2"
 val unique_clauses =
 map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
-val _ = tracing "C"
 fun elim_implies_eta A AB =
 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
-val _ = tracing "D"
 val uniqueness = G_cases
 |> Thm.forall_elim (cterm_of thy lhs)
 |> Thm.forall_elim (cterm_of thy y)
 |> Thm.forall_elim P
 |> Thm.elim_implies G_lhs_y
 |> fold elim_implies_eta unique_clauses
 |> Thm.implies_intr (cprop_of G_lhs_y)
 |> Thm.forall_intr (cterm_of thy y)
-val _ = tracing "E"
 val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 val exactly_one =
 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
 |> curry (op COMP) existence
 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
 |> Thm.implies_intr (cprop_of case_hyp)
 |> fold_rev (Thm.implies_intr o cprop_of) ags
 |> fold_rev Thm.forall_intr cqs
-val _ = tracing "F"
 val function_value =
 existence
 |> Thm.implies_intr ihyp
 |> Thm.implies_intr (cprop_of case_hyp)
 |> Thm.forall_intr (cterm_of thy x)
 |> Thm.forall_elim (cterm_of thy lhs)
 |> curry (op RS) refl
-val _ = tracing "G"
 in
 (exactly_one, function_value)
 end
 *}
 |> fold_rev (Thm.implies_intr o cprop_of) compat
 |> Thm.implies_intr (cprop_of complete)
 in
 (goalstate, values)
 end
+*}
+ML {*
+Inductive.add_inductive_i;
+Local_Theory.conceal
+*}
+ML {*
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
 let
-val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
+val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
 lthy
 |> Local_Theory.conceal
 |> Inductive.add_inductive_i
 {quiet_mode = true,
 verbose = ! trace,
 alt_name = Binding.empty,
 coind = false,
 [] (* 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' = (Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}
 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), lthy)
+((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy)
 end
 *}
 ML {*
 fun define_graph Gname fvar domT ranT clauses RCss 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, _), lthy) =
+val ((R, RIntro_thms, R_elim, _, R_eqvt), lthy) =
 inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
 in
-((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
+((R, Library.unflat R_intross RIntro_thms, R_elim, R_eqvt), lthy)
 end
 fun fix_globals domT ranT fvar ctxt =
 let
 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
 end
 in
 map2 mk_trsimp clauses psimps
 end
+*}
+ML {*
 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
 let
 val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
 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), lthy) =
+val ((G, GIntro_thms, G_elim, G_induct, G_eqvt), lthy) =
 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 val _ = tracing ("Graph - name: " ^ @{make_string} G)
 val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms))
+val _ = tracing ("Graph Equivariance" ^ @{make_string} 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: " ^ @{make_string} f)
 val _ = tracing ("f_defthm:\n" ^ @{make_string} 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 ((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: " ^ @{make_string} R)
 val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
+val _ = tracing ("Relation Equivariance" ^ @{make_string} 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
 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" ^ @{make_string} globals)
 val _ = tracing ("complete:\n" ^ @{make_string} complete)
 val _ = tracing ("compat:\n" ^ @{make_string} compat)
 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
 depth :: "lam \<Rightarrow> nat"
 where
 "depth (Var x) = 1"
 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
 | "depth (Lam x t) = (depth t) + 1"
+thm depth_graph.intros
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)

changeset 2650	e5fa8de0e4bd
parent 2649	a8ebcb368a15
child 2651	4aa72a88b2c1