# HG changeset patch # User Christian Urban # Date 1295123056 0 # Node ID 3342a2d13d958965937403c36bfbc616f1cb78c1 # Parent 619ecb57db389193ed52bf5875d31dc68ab394fe nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions diff -r 619ecb57db38 -r 3342a2d13d95 Nominal/Ex/LamTest.thy --- 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 \* x" + shows "as \* f x" +using fresh +unfolding fresh_star_def +unfolding fresh_def +using supp_eqvt_at[OF asm fin] +by auto + definition "eqvt f \ \p. p \ 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 \ (removeAll x xs) = removeAll (p \ x) (p \ xs)" +by (induct xs) (auto) + +nominal_primrec + frees_lst :: "lam \ 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 \ name \ lam \ 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 \ (y, s) \ (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 \ 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 \ (removeAll x xs) = removeAll (p \ x) (p \ xs)" +by (induct xs) (auto) + +nominal_primrec + frees_lst :: "lam \ 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 \ name set" @@ -1745,6 +1889,116 @@ apply(rule_tac t="frees_sumC t - {x}" and s="(x \ a) \ (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 \ + (\p. supp ([bs]set. x) = supp ([cs]set. y) \ + supp ([bs]set. x) \* p \ + p \ x = y \ p \ 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 \ + (\p. supp ([bs]set. x) = supp ([cs]set. y) \ + supp ([bs]set. x) \* p \ + p \ x = y \ p \ bs = cs \ + supp p \ bs \ 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 \ + (\p. supp ([bs]lst. x) = supp ([cs]lst. y) \ + supp ([bs]lst. x) \* p \ + p \ x = y \ p \ 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 \ + (\p. supp ([bs]lst. x) = supp ([cs]lst. y) \ + supp ([bs]lst. x) \* p \ + p \ x = y \ p \ bs = cs \ + supp p \ set bs \ 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 \ name \ lam \ 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 \ (y, s) \ (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 \ ya = ya") +apply(subgoal_tac "p \ 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 \ name \ lam \ lam" ("_ [_ ::= _]" [100,100,100] 100) where