# HG changeset patch # User Christian Urban # Date 1268221735 -3600 # Node ID 4eaae533efc39050c18be45f7390b4d9575034c3 # Parent baa67b07f436407e47974b7359c0c532d885c3d7# Parent ebfbcadeac5e1b88b9ff499fdd8c79094d5c5432 merged diff -r baa67b07f436 -r 4eaae533efc3 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Mar 10 12:48:38 2010 +0100 +++ b/Nominal/Fv.thy Wed Mar 10 12:48:55 2010 +0100 @@ -193,6 +193,51 @@ end *} +ML {* +fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = +let + val {descr, sorts, ...} = dt_info; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); + val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} + val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); + fun alpha_bn_constr (cname, dts) args_in_bn = + let + val Ts = map (typ_of_dtyp descr sorts) dts; + val pi = Free("pi", @{typ perm}) + val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); + val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); + val args = map Free (names ~~ Ts); + val args2 = map Free (names2 ~~ Ts); + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val rhs = HOLogic.mk_Trueprop + (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); + fun lhs_arg ((dt, arg_no), (arg, arg2)) = + let + val argty = fastype_of arg; + val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); + val permarg = if is_rec then permute $ pi $ arg else arg + in + if is_rec_type dt then + if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2 + else (nth alpha_frees (body_index dt)) $ permarg $ arg2 + else + if arg_no mem args_in_bn then @{term True} + else HOLogic.mk_eq (permarg, arg2) + end + val arg_nos = 0 upto (length dts - 1) + val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) + val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) + in + eq + end + val (_, (_, _, constrs)) = nth descr ith_dtyp; + val eqs = map2i alpha_bn_constr constrs args_in_bns +in + ((bn, alpha_bn_free), (alpha_bn_name, eqs)) +end +*} + ML {* fn x => split_list(flat x) *} ML {* fn x => apsnd flat (split_list (map split_list x)) *} (* TODO: Notice datatypes without bindings and replace alpha with equality *) @@ -209,12 +254,17 @@ val nr_bns = non_rec_binds bindsall; val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); - val fv_bns = map snd bn_fv_bns; val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => "alpha_" ^ name_of_typ (nth_dtyp i)) descr); val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; val alpha_frees = map Free (alpha_names ~~ alpha_types); + (* We assume that a bn is either recursive or not *) + val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; + val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec)) + val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs; + val alpha_bn_frees = map snd bn_alpha_bns; + val alpha_bn_types = map fastype_of alpha_bn_frees; fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; @@ -269,14 +319,26 @@ HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); fun alpha_arg ((dt, arg_no), (arg, arg2)) = let - val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis; + val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; + val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; + val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis; in - if relevant = [] then ( - if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) - else (HOLogic.mk_eq (arg, arg2))) - else - if is_rec_type dt then let - (* THE HARD CASE *) + case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of + ([], [], []) => + if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) + else (HOLogic.mk_eq (arg, arg2)) + (* TODO: if more then check and accept *) + | (_, [], []) => @{term True} + | ([], [(((SOME (bn, _)), _, _), pi)], []) => + let + val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 + val ty = fastype_of (bn $ arg) + val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) + in + HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) + end + | ([], [], relevant) => + let val (rbinds, rpis) = split_list relevant val lhs_binds = fv_binds args rbinds val lhs = mk_pair (lhs_binds, arg); @@ -290,10 +352,10 @@ (* val pi_supps = map ((curry op $) @{term "supp :: perm \ atom set"}) rpis; val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) in - (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) +(* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen - (* TODO Add some test that is makes sense *) - end else @{term "True"} + end + | _ => error "Fv.alpha: not supported binding structure" end val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) val alpha_lhss = mk_conjl alphas @@ -307,7 +369,7 @@ val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; - fun filter_fun (a, b) = b mem rel_bns_nos; + fun filter_fun (_, b) = b mem rel_bns_nos; val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) @@ -325,38 +387,35 @@ val (alphas, lthy''') = (Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} - (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] - (add_binds alpha_eqs) [] lthy'') + (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) + (alpha_types @ alpha_bn_types)) [] + (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') + val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) in - ((fvs, alphas), lthy''') + ((all_fvs, alphas), lthy''') end *} (* atom_decl name - datatype lam = VAR "name" | APP "lam" "lam" | LET "bp" "lam" and bp = BP "name" "lam" - primrec bi::"bp \ atom set" where "bi (BP x t) = {atom x}" - setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} - - local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") - [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} + [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} print_theorems *) -(* +(*atom_decl name datatype rtrm1 = rVr1 "name" | rAp1 "rtrm1" "rtrm1" @@ -366,24 +425,38 @@ BUnit | BVr "name" | BPr "bp" "bp" - -(* to be given by the user *) - primrec bv1 where "bv1 (BUnit) = {}" | "bv1 (BVr x) = {atom x}" | "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp1)" - -setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *} - -local_setup {* define_fv_alpha "Fv.rtrm1" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], - [[], [[]], [[], []]]] *} +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *} +local_setup {* + snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1") + [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]], + [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} print_theorems *) +(* +atom_decl name +datatype rtrm5 = + rVr5 "name" +| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" +and rlts = + rLnil +| rLcons "name" "rtrm5" "rlts" +primrec + rbv5 +where + "rbv5 rLnil = {}" +| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" +setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5") + [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} +print_theorems +*) ML {* fun alpha_inj_tac dist_inj intrs elims = diff -r baa67b07f436 -r 4eaae533efc3 Nominal/Term5.thy --- a/Nominal/Term5.thy Wed Mar 10 12:48:38 2010 +0100 +++ b/Nominal/Term5.thy Wed Mar 10 12:48:55 2010 +0100 @@ -22,26 +22,16 @@ setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ - [ [], - [], - [(SOME @{term rbv5}, 0, 1)] ], - [ [], - []] ] *} +local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") + [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} print_theorems -(* Alternate version with additional binding of name in rlts in rLcons *) -(*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ - [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} -print_theorems*) - notation alpha_rtrm5 ("_ \5 _" [100, 100] 100) and alpha_rlts ("_ \l _" [100, 100] 100) -thm alpha_rtrm5_alpha_rlts.intros +thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} thm alpha5_inj lemma rbv5_eqvt[eqvt]: @@ -60,8 +50,15 @@ lemma alpha5_eqvt: "xa \5 y \ (x \ xa) \5 (x \ y)" "xb \l ya \ (x \ xb) \l (x \ ya)" - apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) - apply (simp_all add: alpha5_inj) + "alpha_rbv5 a b c \ True" +apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) +apply (simp_all add: alpha5_inj) +apply (erule exE) +apply (rule_tac x="pi" in exI) +apply clarify +apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) +apply (subst eqvts[symmetric]) +apply (subst eqvts[symmetric]) sorry lemma alpha5_equivp: @@ -84,25 +81,25 @@ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) + |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) *} print_theorems lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) + "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s) \ (l \l m \ fv_rlts l = fv_rlts m) \ (alpha_rbv5 a b c \ True)" + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) apply(simp_all) apply(simp add: alpha_gen) apply(erule conjE)+ apply(erule exE) apply(erule conjE)+ apply(simp_all) - done + sorry lemma bv_list_rsp: shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) + apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) apply(simp_all) apply(clarify) apply simp @@ -118,11 +115,22 @@ "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" + "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - done - + defer + apply clarify + apply (erule alpha_rlts.cases) + apply (erule alpha_rlts.cases) + apply (simp_all) + defer + apply (erule alpha_rlts.cases) + apply (simp_all) + defer + apply clarify + apply (simp add: alpha5_inj) + sorry (* may be true? *) lemma shows "(alpha_rlts ===> op =) rbv5 rbv5" by (simp add: bv_list_rsp) @@ -147,11 +155,10 @@ end -lemmas - permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] -and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] -and bv5[simp] = rbv5.simps[quot_lifted] -and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +lemmas bv5[simp] = rbv5.simps[quot_lifted] +lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] lemma lets_ok: "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" @@ -159,6 +166,7 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) +apply (metis flip_at_simps(1) supp_at_base supp_eqvt) done lemma lets_ok3: @@ -170,10 +178,12 @@ lemma lets_not_ok1: - "x \ y \ (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ - (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" + "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = + (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (simp add: alpha5_INJ alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) +apply (rule_tac x="0::perm" in exI) +apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) +apply auto done lemma distinct_helper: @@ -192,7 +202,7 @@ (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: distinct_helper2) +apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) done end