# HG changeset patch # User Cezary Kaliszyk # Date 1267455843 -3600 # Node ID 0203cd5cfd6c2aaf285b35572d7d0ff3f6cf7d5a # Parent 8557af71724e066dd9c615392d6a4f3c8954d26a The new alpha-equivalence and testing in Trm2 and Trm5. diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Mar 01 14:26:14 2010 +0100 +++ b/Nominal/Fv.thy Mon Mar 01 16:04:03 2010 +0100 @@ -1,5 +1,5 @@ theory Fv -imports "Nominal2_Atoms" "Abs" +imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *) begin (* Bindings are given as a list which has a length being equal @@ -54,6 +54,7 @@ in the database. *) +(* TODO: should be const_name union *) ML {* open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); (* TODO: It is the same as one in 'nominal_atoms' *) @@ -64,7 +65,12 @@ fold (fn a => fn b => if a = noatoms then b else if b = noatoms then a else - HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; + HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms; + fun mk_conjl props = + fold (fn a => fn b => + if a = @{term True} then b else + if b = @{term True} then a else + HOLogic.mk_conj (a, b)) props @{term True}; fun mk_diff a b = if b = noatoms then a else if b = a then noatoms else @@ -90,6 +96,8 @@ *} +ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ perm"}) $ p1 $ p2 *} + (* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = @@ -105,58 +113,75 @@ "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); - fun fv_alpha_constr i (cname, dts) bindcs = + fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; - val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); + val bindslen = length bindcs + val pi_strs = replicate bindslen "pi" + val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; + val bind_pis = bindcs ~~ pis; + val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); - val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); + val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); val args2 = map Free (names2 ~~ Ts); - val c = Const (cname, Ts ---> (nth_dtyp i)); - val fv_c = nth fv_frees i; - val alpha = nth alpha_frees i; - fun fv_bind args (NONE, i) = + val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); + val fv_c = nth fv_frees ith_dtyp; + val alpha = nth alpha_frees ith_dtyp; + val arg_nos = 0 upto (length dts - 1) + fun fv_bind args (NONE, i, _) = if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else (* TODO we assume that all can be 'atomized' *) if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else mk_single_atom (nth args i) - | fv_bind args (SOME f, i) = f $ (nth args i); - fun fv_arg ((dt, x), bindxs) = + | fv_bind args (SOME f, i, _) = f $ (nth args i); + fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + fun fv_arg ((dt, x), arg_no) = let val arg = if is_rec_type dt then nth fv_frees (body_index dt) $ x else (* TODO: we just assume everything can be 'atomized' *) if (is_funtype o fastype_of) x then mk_atoms x else - HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] - val sub = mk_union (map (fv_bind args) bindxs) + HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]; + (* If i = j then we generate it only once *) + val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; + val sub = fv_binds args relevant in mk_diff arg sub end; val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))) + (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) val alpha_rhs = HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); - fun alpha_arg ((dt, bindxs), (arg, arg2)) = - if bindxs = [] 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 *) - val lhs_binds = mk_union (map (fv_bind args) bindxs); - val lhs = mk_pair (lhs_binds, arg); - val rhs_binds = mk_union (map (fv_bind args2) bindxs); - val rhs = mk_pair (rhs_binds, arg2); - val alpha = nth alpha_frees (body_index dt); - val fv = nth fv_frees (body_index dt); - val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs; - val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre - in - HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t) - (* TODO Add some test that is makes sense *) - end else @{term "True"} - val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2)) - val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs) + fun alpha_arg ((dt, arg_no), (arg, arg2)) = + let + val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) 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 *) + val (rbinds, rpis) = split_list relevant + val lhs_binds = fv_binds args rbinds + val lhs = mk_pair (lhs_binds, arg); + val rhs_binds = fv_binds args2 rbinds; + val rhs = mk_pair (rhs_binds, arg2); + val alpha = nth alpha_frees (body_index dt); + val fv = nth fv_frees (body_index dt); + (* TODO: check that pis have empty intersection *) + val pi = foldr1 add_perm rpis; + val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; + in + Syntax.check_term lthy alpha_gen_pre + (* TODO Add some test that is makes sense *) + end else @{term "True"} + end + val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) + val alpha_lhss = mk_conjl alphas + val alpha_lhss_ex = + fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss + val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) in (fv_eq, alpha_eq) end; diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Term2.thy --- a/Nominal/Term2.thy Mon Mar 01 14:26:14 2010 +0100 +++ b/Nominal/Term2.thy Mon Mar 01 16:04:03 2010 +0100 @@ -23,8 +23,11 @@ setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], - [[[], []]]] *} + [[[], + [], + [(NONE, 0, 1)], + [(SOME @{term rbv2}, 0, 1)]], + [[]]] *} notation alpha_rtrm2 ("_ \2 _" [100, 100] 100) and diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Term5.thy --- a/Nominal/Term5.thy Mon Mar 01 14:26:14 2010 +0100 +++ b/Nominal/Term5.thy Mon Mar 01 16:04:03 2010 +0100 @@ -22,8 +22,13 @@ 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)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} + [ [], + [], + [(SOME @{term rbv5}, 0, 1)] ], + [ [], + []] ] *} print_theorems (* Alternate version with additional binding of name in rlts in rLcons *) @@ -57,17 +62,12 @@ "xb \l ya \ (x \ xb) \l (x \ ya)" apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) apply (simp_all add: alpha5_inj) - apply (tactic {* - ALLGOALS ( - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt}) - ) *}) - apply (simp_all only: eqvts atom_eqvt) - done +sorry -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), - (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} -thm alpha5_equivp +lemma alpha5_equivp: + "equivp alpha_rtrm5" + "equivp alpha_rlts" + sorry quotient_type trm5 = rtrm5 / alpha_rtrm5 @@ -92,13 +92,20 @@ "(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) - apply(simp_all add: alpha_gen) + apply(simp_all) + apply(simp add: alpha_gen) + apply(erule conjE)+ + apply(erule exE) + apply(erule conjE)+ + apply(simp_all) done lemma bv_list_rsp: shows "x \l y \ rbv5 x = rbv5 y" apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) apply(simp_all) + apply(clarify) + apply simp done lemma [quot_respect]: @@ -112,8 +119,7 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) - apply (clarify) apply (rule conjI) - apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) + apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) done @@ -149,49 +155,24 @@ lemma lets_ok: "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" -apply (subst alpha5_INJ) -apply (rule conjI) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: alpha5_INJ) apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -done - -lemma lets_ok2: - "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = - (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (subst alpha5_INJ) -apply (rule conjI) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="0 :: perm" in exI) -apply (simp only: alpha_gen) +apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) done lemma lets_ok3: - assumes a: "distinct [x, y]" - shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = - (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" -apply (subst alpha5_INJ) -apply (rule conjI) -apply (simp add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="(x \ y)" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (rule_tac x="0 :: perm" in exI) -apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) + "x \ y \ + (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ + (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" +apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) done + 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)))" -apply (simp add: alpha5_INJ(3) alpha_gen) +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)) done @@ -214,5 +195,4 @@ apply (simp add: distinct_helper2) done - end