nominal2: comparison Nominal/Ex/LamTest.thy

equal deleted inserted replaced

-:619ecb57db38
+:3342a2d13d95
 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:
 val acc_downward = @{thm accp_downward}
 val accI = @{thm accp.accI}
 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) =
 ([], (fixes, assumes, arg) :: xs)
 | add_Ri _ _ _ _ = raise Match
 ML {*
 (** building proof obligations *)
 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')
 val RCs_rhs  = find_calls2 fvar rhs
 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')
-|> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs)
+|> 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')
+(*|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')*) (* HERE *)
-(*|> (curry Logic.mk_implies) @{term "Trueprop True"}*)  (* 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
 *}
 ML {*
 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
 HOLogic.mk_Trueprop Pbool
 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
 |> 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
 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
 in
 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
 fun abs lev v tm =
 if v aconv tm then Bound lev
 in
 (thms1 :: store_compat_thms (n - 1) thms2)
 end
 *}
+ML {*
-ML {*
+fun pp_thm thm =
-fun eqvt_at_elim 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 @{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 {*
 (* 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" *)
 (* 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
 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" *)
-(*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
+|> fold Thm.elim_implies (rev eqvtsj) (* HERE *)
-(*|> Thm.elim_implies @{thm TrueI}*) (* THERE *)
+(*|> eqvt_at_elim thy eqvtsj *)
-|> eqvt_at_elim
-(*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
 |> 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" *)
-(*|> tap (fn th => tracing ("NEED TO PROVE " ^ @{make_string} th))*)
+|> fold Thm.elim_implies (rev eqvtsi) (* HERE *)
-(*|> Thm.elim_implies @{thm TrueI}*)
+(* |> eqvt_at_elim thy eqvts *)
-|> eqvt_at_elim
-(*|> tap (fn th => tracing ("AFTER " ^ @{make_string} th))*)
 |> 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 {*
 (* 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
 end
 replace_lemma
 end
 *}
 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
 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 eqvtsi = nth eqvts (i - 1)
-val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+|> map (fold Thm.forall_elim cqsi)
-(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+|> 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')
-end
+|> 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
 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 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)
+fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
-|> fold_rev (Thm.implies_intr o cprop_of) CCas
+(llRI RS ih_intro_case)
-|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+|> 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 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 clausei) clauses rep_lemmas
+map2 (mk_uniqueness_clause thy globals compat_store eqvt_lemmas clausei) clauses rep_lemmas
-(*
-val _ = tracing ("unique_clauses\n" ^ cat_lines (map @{make_string} 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
 in
 (exactly_one, function_value)
 end
 *}
-ML Thm.forall_elim_vars
-ML Thm.implies_intr
 ML {* (ex1_implies_ex, ex1_implies_un) *}
 thm fundef_ex1_eqvt_at
 ML {*
 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" ^ @{make_string} ihyp_thm)
+val _ = tracing ("ihyp_thm\n" ^ pp_thm ihyp_thm)
-val _ = tracing ("ih_intro\n" ^ @{make_string} ih_intro)
+val _ = tracing ("ih_intro\n" ^ pp_thm ih_intro)
-val _ = tracing ("ih_elim\n" ^ @{make_string} ih_elim)
+val _ = tracing ("ih_elim\n" ^ pp_thm ih_elim)
-val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
+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
 |> Goal.protect
 |> fold_rev (Thm.implies_intr o cprop_of) compat
 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 - name: " ^ pp_thm G)
-val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms))
+val _ = tracing ("Graph intros:\n" ^ cat_lines (map pp_thm GIntro_thms))
-val _ = tracing ("Graph Equivariance " ^ @{make_string} G_eqvt)
+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 - name: " ^ pp_thm f)
-val _ = tracing ("f_defthm:\n" ^ @{make_string} f_defthm)
+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 - name: " ^ pp_thm R)
-val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss))
+val _ = tracing ("Relation intros:\n" ^ cat_lines (map pp_thm RIntro_thmss))
-val _ = tracing ("Relation Equivariance " ^ @{make_string} R_eqvt)
+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
 |> map (cert #> Thm.assume)
 val compat_store = store_compat_thms n compat
 (*
-val _ = tracing ("globals:\n" ^ @{make_string} globals)
+val _ = tracing ("globals:\n" ^ pp_thm globals)
-val _ = tracing ("complete:\n" ^ @{make_string} complete)
+val _ = tracing ("complete:\n" ^ pp_thm complete)
-val _ = tracing ("compat:\n" ^ @{make_string} compat)
+val _ = tracing ("compat:\n" ^ pp_thm compat)
-val _ = tracing ("compat_store:\n" ^ @{make_string} compat_store)
+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
 fun mk_partial_rules provedgoal =
 let
 ML {*
 fun gen_function is_external prep default_constraint fixspec eqns config lthy =
 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
 *}
 ML {*
 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)
+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]
 apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
 apply(simp add: Abs_fresh_iff)
 assumes a: "a \<notin> S" "b \<notin> S"
 shows "(a \<leftrightarrow> b) \<bullet> S = S"
 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"
 where
 "frees (Var x) = {x}"
 apply(simp add: Abs_fresh_iff)
 apply(simp)
 apply(drule test)
 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
 "(Var x)[y ::= s] = (if x=y then s else (Var x))"

changeset 2660	3342a2d13d95
parent 2657	1ea9c059fc0f
child 2661	16896fd8eff5