--- a/Nominal/Ex/LamTest.thy Fri Jan 14 14:22:25 2011 +0000
+++ b/Nominal/Ex/LamTest.thy Sat Jan 15 20:24:16 2011 +0000
@@ -34,6 +34,17 @@
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"
@@ -151,9 +162,10 @@
val case_split = @{thm HOL.case_split}
val fundef_default_value = @{thm FunDef.fundef_default_value}
val not_acc_down = @{thm not_accp_down}
+*}
-
+ML {*
fun find_calls tree =
let
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
@@ -192,13 +204,6 @@
fun mk_compat_proof_obligations domT ranT fvar f glrs =
let
- (*
- val _ = tracing ("domT: " ^ @{make_string} domT)
- val _ = tracing ("ranT: " ^ @{make_string} ranT)
- val _ = tracing ("fvar: " ^ @{make_string} fvar)
- val _ = tracing ("f: " ^ @{make_string} f)
- *)
-
fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
let
val shift = incr_boundvars (length qs')
@@ -210,17 +215,14 @@
(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')
- |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs)
- |> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')
- (*|> (curry Logic.mk_implies) @{term "Trueprop True"}*) (* HERE *)
+ |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* HERE *)
+ (*|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')*) (* HERE *)
|> 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
map mk_impl (unordered_pairs glrs)
- (*|> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts)))
- *)
end
*}
@@ -238,8 +240,10 @@
|> mk_forall_rename ("x", x)
|> mk_forall_rename ("P", Pbool)
end
+*}
(** making a context with it's own local bindings **)
+ML {*
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
let
@@ -261,8 +265,9 @@
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
cqs = cqs, ags = ags, case_hyp = case_hyp }
end
+*}
-
+ML {*
(* lowlevel term function. FIXME: remove *)
fun abstract_over_list vs body =
let
@@ -327,18 +332,33 @@
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 thm =
+(*
+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 @{theory} t
+ 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
+ |> eqvt_at_elim thy eqvts
end
| _ => thm
+*)
*}
ML {*
@@ -348,7 +368,7 @@
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
-fun get_compat_thm thy cts i j ctxi ctxj =
+fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
let
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
@@ -357,13 +377,12 @@
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" *)
- (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
- (*|> Thm.elim_implies @{thm TrueI}*) (* THERE *)
- |> eqvt_at_elim
- (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
+ |> 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" *)
@@ -371,13 +390,12 @@
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" *)
- (*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
- (*|> Thm.elim_implies @{thm TrueI}*)
- |> eqvt_at_elim
- (*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
+ |> fold Thm.elim_implies (rev eqvtsi) (* HERE *)
+ (* |> eqvt_at_elim thy eqvts *)
|> fold Thm.elim_implies agsi
|> fold Thm.elim_implies agsj
|> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -391,7 +409,7 @@
(* Generates the replacement lemma in fully quantified form. *)
fun mk_replacement_lemma thy h ih_elim clause =
let
- val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
+ val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...},
RCs, tree, ...} = clause
local open Conv in
val ih_conv = arg1_conv o arg_conv o arg_conv
@@ -419,50 +437,104 @@
*}
ML {*
-fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
+fun mk_eqvt_lemma thy ih_eqvt clause =
+ let
+ val ClauseInfo {cdata=ClauseContext {cqs, case_hyp, ...}, RCs, ...} = clause
+
+ local open Conv in
+ val ih_conv = arg1_conv o arg_conv o arg_conv
+ end
+
+ val ih_eqvt_case =
+ Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
+
+ fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) =
+ (llRI RS ih_eqvt_case)
+ |> fold_rev (Thm.implies_intr o cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ in
+ map prep_eqvt RCs
+ |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev Thm.forall_intr cqs)
+ |> map (Thm.close_derivation)
+ end
+*}
+
+ML {*
+fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
let
val Globals {h, y, x, fvar, ...} = globals
- val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
+ val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ...}, ...} = 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
+ mk_clause_context x ctxti cdescj
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
- val compat = get_compat_thm thy compat_store i j cctxi cctxj
val Ghsj' = map
(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 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 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 eqvtsi = nth eqvts (i - 1)
+ |> map (fold Thm.forall_elim cqsi)
+ |> map (fold Thm.elim_implies [case_hyp])
+
+ val eqvtsj = nth eqvts (j - 1)
+ |> map (fold Thm.forall_elim cqsj')
+ |> map (fold Thm.elim_implies [case_hypj'])
+
+ 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' *)
+ |> ppp "A"
|> Thm.implies_elim RLj_import
(* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+ |> ppp "B"
|> (fn it => trans OF [it, compat])
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+ |> ppp "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 *)
+ |> ppp "D"
|> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
+ |> ppp "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 *)
+ |> ppp "F"
|> Thm.implies_intr (cprop_of y_eq_rhsj'h)
+ |> ppp "G"
|> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
+ |> ppp "H"
|> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
+ |> ppp "I"
end
*}
-(* HERE *)
ML {*
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas 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
@@ -470,9 +542,10 @@
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
- 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
+ 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
@@ -480,11 +553,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 clausei) clauses rep_lemmas
-
- (*
- val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} unique_clauses))
- *)
+ map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas
fun elim_implies_eta A AB =
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
@@ -521,8 +590,6 @@
end
*}
-ML Thm.forall_elim_vars
-ML Thm.implies_intr
ML {* (ex1_implies_ex, ex1_implies_un) *}
thm fundef_ex1_eqvt_at
@@ -546,43 +613,33 @@
|> 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" ^ @{make_string} ihyp_thm)
- val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro)
- val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim)
- val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
+ (*
+ 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 _ = tracing (cat_lines (map @{make_string} repLemmas))
+ val _ = trace_msg (K "Proving Equivariance lemmas...")
+ val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
split_list (map (mk_uniqueness_case thy globals G f
- ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+ ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)
- val _ = tracing ("ex1s\n" ^ cat_lines (map @{make_string} ex1s))
- val _ = tracing ("values\n" ^ cat_lines (map @{make_string} values))
-
val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
- |> tap (fn th => tracing ("A\n" ^ @{make_string} th))
|> Thm.forall_elim_vars 0
- |> tap (fn th => tracing ("B\n" ^ @{make_string} th))
|> fold (curry op COMP) ex1s
- |> tap (fn th => tracing ("C\n" ^ @{make_string} th))
|> Thm.implies_intr (ihyp)
- |> tap (fn th => tracing ("D\n" ^ @{make_string} th))
|> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
- |> tap (fn th => tracing ("E\n" ^ @{make_string} th))
|> Thm.forall_intr (cterm_of thy x)
- |> tap (fn th => tracing ("F\n" ^ @{make_string} th))
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
- |> tap (fn th => tracing ("G\n" ^ @{make_string} th))
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
- |> tap (fn th => tracing ("H\n" ^ @{make_string} th))
-
val goalstate = Conjunction.intr graph_is_function complete
|> Thm.close_derivation
@@ -1078,33 +1135,33 @@
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 _ = 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: " ^ @{make_string} f)
- val _ = tracing ("f_defthm:\n" ^ @{make_string} f_defthm)
+ 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 @{make_string} RCss))
+ 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: " ^ @{make_string} R)
- val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
- val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt)
+ 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) =
@@ -1129,19 +1186,16 @@
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 _ = 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
- val _ = tracing ("goalstate prove_stuff thm:\n" ^ @{make_string} goalstate)
- val _ = tracing ("values prove_stuff thms:\n" ^ cat_lines (map @{make_string} values))
-
val mk_trsimps =
mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
@@ -1585,16 +1639,11 @@
let
val ((goal_state, afterqed), lthy') =
prepare_function is_external prep default_constraint fixspec eqns config lthy
-
- val _ = tracing ("goal state:\n" ^ @{make_string} goal_state)
- val _ = tracing ("concl of goal state:\n" ^ Syntax.string_of_term lthy' (concl_of goal_state))
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
- (*|> tap (fn x => tracing ("after thm:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*)
|> Proof.refine (Method.primitive_text (K goal_state))
|> Seq.hd
- (*|> tap (fn x => tracing ("after ref:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*)
end
*}
@@ -1683,6 +1732,76 @@
apply(simp_all only: lam.distinct)
apply(simp add: lam.eq_iff)
apply(simp add: lam.eq_iff)
+apply(subst (asm) Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+oops
+
+lemma removeAll_eqvt[eqvt]:
+ shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+by (induct xs) (auto)
+
+nominal_primrec
+ frees_lst :: "lam \<Rightarrow> atom list"
+where
+ "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
+| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+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)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+oops
+
+nominal_primrec
+ subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
+where
+ "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
+apply(simp_all add: lam.distinct)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+apply(subst (asm) Abs_eq_iff3)
+apply(erule exE)
+
+
+
+nominal_primrec
+ 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"
+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)
+(*
+apply(subst (asm) Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+*)
apply(subgoal_tac "finite (supp (x, xa, t, ta, depth_sumC t, depth_sumC ta))")
apply(erule_tac ?'a="name" in obtain_at_base)
unfolding fresh_def[symmetric]
@@ -1719,6 +1838,31 @@
unfolding permute_set_eq
using a by (auto simp add: permute_flip_at)
+lemma removeAll_eqvt[eqvt]:
+ shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+by (induct xs) (auto)
+
+nominal_primrec
+ frees_lst :: "lam \<Rightarrow> atom list"
+where
+ "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
+| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+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)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+oops
nominal_primrec
frees :: "lam \<Rightarrow> name set"
@@ -1745,6 +1889,116 @@
apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
oops
+thm Abs_eq_iff[simplified alphas]
+
+lemma Abs_set_eq_iff2:
+ fixes x y::"'a::fs"
+ shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
+ (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
+ supp ([bs]set. x) \<sharp>* p \<and>
+ p \<bullet> x = y \<and> p \<bullet> bs = cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+by simp
+
+lemma Abs_set_eq_iff3:
+ fixes x y::"'a::fs"
+ assumes a: "finite bs" "finite cs"
+ shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
+ (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
+ supp ([bs]set. x) \<sharp>* p \<and>
+ p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
+ supp p \<subseteq> bs \<union> cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+apply(auto)
+using set_renaming_perm
+sorry
+
+lemma Abs_eq_iff2:
+ fixes x y::"'a::fs"
+ shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
+ (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
+ supp ([bs]lst. x) \<sharp>* p \<and>
+ p \<bullet> x = y \<and> p \<bullet> bs = cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+by simp
+
+lemma Abs_eq_iff3:
+ fixes x y::"'a::fs"
+ shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
+ (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
+ supp ([bs]lst. x) \<sharp>* p \<and>
+ p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
+ supp p \<subseteq> set bs \<union> set cs)"
+unfolding Abs_eq_iff
+unfolding alphas
+unfolding supp_Abs
+apply(auto)
+using list_renaming_perm
+apply -
+apply(drule_tac x="bs" in meta_spec)
+apply(drule_tac x="p" in meta_spec)
+apply(erule exE)
+apply(rule_tac x="q" in exI)
+apply(simp add: set_eqvt)
+sorry
+
+nominal_primrec
+ subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
+where
+ "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
+apply(simp_all add: lam.distinct)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+apply(subst (asm) Abs_eq_iff3)
+apply(erule exE)
+apply(erule conjE)+
+apply(clarify)
+apply(perm_simp)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(drule fresh_star_supp_conv)
+apply(simp add: Abs_fresh_star_iff)
+thm fresh_eqvt_at
+apply(rule_tac f="subst_sumC" in fresh_eqvt_at)
+apply(assumption)
+apply(simp add: finite_supp)
+prefer 2
+apply(simp)
+apply(simp add: eqvt_at_def)
+apply(perm_simp)
+apply(subgoal_tac "p \<bullet> ya = ya")
+apply(subgoal_tac "p \<bullet> sa = sa")
+apply(simp)
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+
+
+
nominal_primrec
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100)
where