--- a/Nominal/Ex/LamTest.thy Sat Jan 15 21:16:15 2011 +0000
+++ b/Nominal/Ex/LamTest.thy Mon Jan 17 12:33:37 2011 +0000
@@ -9,86 +9,6 @@
| 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 {*
@@ -333,33 +253,6 @@
*}
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)
@@ -375,12 +268,10 @@
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" *)
@@ -388,12 +279,10 @@
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)
@@ -462,10 +351,9 @@
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', ...} =
@@ -480,8 +368,6 @@
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
@@ -489,64 +375,38 @@
|> 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
*}
ML {*
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas eqvt_lemmas clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
let
val Globals {x, y, ranT, fvar, ...} = globals
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
@@ -565,9 +425,7 @@
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
-
- val _ = tracing ("DONE unique clauses")
+ map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
fun elim_implies_eta A AB =
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
@@ -605,9 +463,6 @@
*}
-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
@@ -627,13 +482,6 @@
|> 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
@@ -666,10 +514,9 @@
*}
-
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
@@ -689,8 +536,14 @@
[] (* 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 eqvt_thm' =
+ 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 =
@@ -730,7 +583,7 @@
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
*}
@@ -762,10 +615,10 @@
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
- val ((R, RIntro_thms, R_elim, _, R_eqvt), lthy) =
- inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+ val ((R, RIntro_thms, R_elim, _, _), 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
@@ -1145,39 +998,18 @@
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 _ = tracing ("recursive calls:\n" ^ cat_lines (map pp_thm RCss))
- *)
-
- val ((R, RIntro_thmss, R_elim, R_eqvt), lthy) =
+ val ((R, RIntro_thmss, R_elim), 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
@@ -1199,13 +1031,6 @@
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
@@ -1352,16 +1177,6 @@
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}
@@ -1642,11 +1457,6 @@
end
*}
-ML {*
- Proof.theorem;
- Proof.refine
-*}
-
ML {*
fun gen_function is_external prep default_constraint fixspec eqns config lthy =