--- a/Nominal/Ex/LamTest.thy Thu Jan 06 23:06:45 2011 +0000
+++ b/Nominal/Ex/LamTest.thy Fri Jan 07 02:30:00 2011 +0000
@@ -12,6 +12,10 @@
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 {*
@@ -96,6 +100,16 @@
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 *)
@@ -114,6 +128,7 @@
(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
@@ -228,7 +243,6 @@
end
*}
-
ML {*
(* expects i <= j *)
fun lookup_compat_thm i j cts =
@@ -244,7 +258,6 @@
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" *)
@@ -256,22 +269,14 @@
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
@@ -320,33 +325,20 @@
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
@@ -375,31 +367,21 @@
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)
@@ -409,8 +391,6 @@
|> 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 =
@@ -422,8 +402,6 @@
|> 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
@@ -431,8 +409,6 @@
|> 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
@@ -482,13 +458,20 @@
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
+ |> Local_Theory.conceal
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -504,6 +487,9 @@
[] (* 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
@@ -517,7 +503,7 @@
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
*}
@@ -574,10 +560,10 @@
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
@@ -928,8 +914,9 @@
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
@@ -956,11 +943,13 @@
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
@@ -971,11 +960,12 @@
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
@@ -998,10 +988,12 @@
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
@@ -1501,6 +1493,7 @@
"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)