# HG changeset patch # User Cezary Kaliszyk # Date 1266514433 -3600 # Node ID a228acf2907ea7100483f18ddb8f3705a8bc3710 # Parent 6fd072d3acd28f91199710f7ea8e396c6e546aea Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct. diff -r 6fd072d3acd2 -r a228acf2907e Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Thu Feb 18 15:03:09 2010 +0100 +++ b/Quot/Nominal/Fv.thy Thu Feb 18 18:33:53 2010 +0100 @@ -1,5 +1,5 @@ theory Fv -imports "Nominal2_Atoms" +imports "Nominal2_Atoms" "Abs" begin (* Bindings are given as a list which has a length being equal @@ -80,12 +80,19 @@ (* Copy from Term *) fun is_funtype (Type ("fun", [_, _])) = true | is_funtype _ = false; + (* Similar to one in USyntax *) + fun mk_pair (fst, snd) = + let val ty1 = fastype_of fst + val ty2 = fastype_of snd + val c = HOLogic.pair_const ty1 ty2 + in c $ fst $ snd + end; + *} - ML {* (* Currently needs just one full_tname to access Datatype *) -fun define_raw_fv full_tname bindsall lthy = +fun define_fv_alpha full_tname bindsall lthy = let val thy = ProofContext.theory_of lthy; val {descr, ...} = Datatype.the_info thy full_tname; @@ -95,19 +102,26 @@ "fv_" ^ name_of_typ (nth_dtyp i)) descr); val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; val fv_frees = map Free (fv_names ~~ fv_types); - fun fv_eq_constr i (cname, dts) bindcs = + 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); + fun fv_alpha_constr i (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 args = map Free (names ~~ Ts); + val names2 = Name.variant_list ("pi" :: 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; - fun fv_bind (NONE, i) = + val alpha = nth alpha_frees i; + 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 (SOME f, i) = f $ (nth args i); + | fv_bind args (SOME f, i) = f $ (nth args i); fun fv_arg ((dt, x), bindxs) = let val arg = @@ -115,70 +129,64 @@ (* 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 bindxs) + val sub = mk_union (map (fv_bind args) bindxs) in mk_diff arg sub end; - val _ = tracing ("d" ^ string_of_int (length dts)); - val _ = tracing (string_of_int (length args)); - val _ = tracing (string_of_int (length bindcs)); + val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq + (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))) + 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) in - (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq - (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) + (fv_eq, alpha_eq) end; - fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; - val fv_eqs = flat (map2 fv_eq descr bindsall) + fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds; + val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall)) + val add_binds = map (fn x => (Attrib.empty_binding, x)) + val (fvs, lthy') = (Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) + val (alphas, lthy'') = (Inductive.add_inductive_i + {quiet_mode = false, verbose = true, 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') in - (* The snd will be removed later *) - snd (Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) + ((fvs, alphas), lthy'') end *} -ML {* -fun define_alpha full_tname bindsall lthy = -let - val thy = ProofContext.theory_of lthy; - val {descr, ...} = Datatype.the_info thy full_tname; - val sorts = []; (* TODO *) - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); - 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); - fun alpha_eq_constr i (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 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 i)); - val alpha = nth alpha_frees i; - in - (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)))) - end; - fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds; - val alpha_eqs = flat (map2 alpha_eq descr bindsall) -in - (* The snd will be removed later *) - snd (Inductive.add_inductive_i - {quiet_mode = false, verbose = true, 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) [] (alpha_eqs) [] lthy) -end -*} - +(* tests atom_decl name -(*datatype ty = +datatype ty = Var "name set" ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} -local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} +local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *} print_theorems -*) + datatype rtrm1 = rVr1 "name" @@ -199,15 +207,12 @@ | "bv1 (BVr x) = {atom x}" | "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp1)" -local_setup {* define_raw_fv "Fv.rtrm1" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], +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)]]], [[], [[]], [[], []]]] *} print_theorems - -local_setup {* define_alpha "Fv.rtrm1" - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], - [[], [[]], [[], []]]] *} -print_theorems - +*) end diff -r 6fd072d3acd2 -r a228acf2907e Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Thu Feb 18 15:03:09 2010 +0100 +++ b/Quot/Nominal/Terms.thy Thu Feb 18 18:33:53 2010 +0100 @@ -27,34 +27,52 @@ | "bv1 (BVr x) = {atom x}" | "bv1 (BPr bp1 bp2) = (bv1 bp1) \ (bv1 bp2)" -local_setup {* define_raw_fv "Terms.rtrm1" +setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} + +local_setup {* snd o define_fv_alpha "Terms.rtrm1" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], [[], [[]], [[], []]]] *} print_theorems - -setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} - -inductive - alpha1 :: "rtrm1 \ rtrm1 \ bool" ("_ \1 _" [100, 100] 100) -where - a1: "a = b \ (rVr1 a) \1 (rVr1 b)" -| a2: "\t1 \1 t2; s1 \1 s2\ \ rAp1 t1 s1 \1 rAp1 t2 s2" -| a3: "(\pi. (({atom aa}, t) \gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \ rLm1 aa t \1 rLm1 ab s" -| a4: "t1 \1 t2 \ (\pi. (((bv1 b1), s1) \gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \ rLt1 b1 t1 s1 \1 rLt1 b2 t2 s2" +notation + alpha_rtrm1 ("_ \1 _" [100, 100] 100) and + alpha_bp ("_ \1b _" [100, 100] 100) +thm alpha_rtrm1_alpha_bp.intros lemma alpha1_inj: "(rVr1 a \1 rVr1 b) = (a = b)" "(rAp1 t1 s1 \1 rAp1 t2 s2) = (t1 \1 t2 \ s1 \1 s2)" -"(rLm1 aa t \1 rLm1 ab s) = (\pi. (({atom aa}, t) \gen alpha1 fv_rtrm1 pi ({atom ab}, s)))" -"(rLt1 b1 t1 s1 \1 rLt1 b2 t2 s2) = (t1 \1 t2 \ (\pi. (((bv1 b1), s1) \gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))" +"(rLm1 aa t \1 rLm1 ab s) = (\pi. (({atom aa}, t) \gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" +"(rLt1 bp rtrm11 rtrm12 \1 rLt1 bpa rtrm11a rtrm12a) = + ((\pi. (bv1 bp, bp) \gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \ rtrm11 \1 rtrm11a \ + (\pi. (bv1 bp, rtrm12) \gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))" +"alpha_bp BUnit BUnit" +"(alpha_bp (BVr name) (BVr namea)) = (name = namea)" +"(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \ alpha_bp bp2 bp2a)" apply - -apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) -apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) -apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) -apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) +apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) +apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) +apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) +apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) +apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) +apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) done -(* Shouyld we derive it? But bv is given by the user? *) +lemma alpha_bp_refl: "alpha_bp a a" +apply induct +apply (simp_all add: alpha1_inj) +done + +lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" +apply rule +apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) +apply (simp_all add: alpha_bp_refl) +done + +lemma alpha_bp_eq: "alpha_bp = (op =)" +apply (rule ext)+ +apply (rule alpha_bp_eq_eq) +done + lemma bv1_eqvt[eqvt]: shows "(pi \ bv1 x) = bv1 (pi \ x)" apply (induct x) @@ -68,10 +86,10 @@ apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) done - lemma alpha1_eqvt: - shows "t \1 s \ (pi \ t) \1 (pi \ s)" - apply (induct t s rule: alpha1.inducts) + "t \1 s \ (pi \ t) \1 (pi \ s)" + "alpha_bp a b \ alpha_bp (pi \ a) (pi \ b)" + apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) apply (simp_all add:eqvts alpha1_inj) apply (erule exE) apply (rule_tac x="pi \ pia" in exI) @@ -85,6 +103,8 @@ apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) apply(simp add: permute_eqvt[symmetric]) apply (erule exE) + apply (erule exE) + apply (rule conjI) apply (rule_tac x="pi \ pia" in exI) apply (simp add: alpha_gen) apply(erule conjE)+ @@ -95,12 +115,22 @@ apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) apply(simp add: permute_eqvt[symmetric]) + apply (rule_tac x="pi \ piaa" in exI) + apply (simp add: alpha_gen) + apply(erule conjE)+ + apply(rule conjI) + apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) + apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(rule conjI) + apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) + apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) + apply(simp add: permute_eqvt[symmetric]) done -lemma alpha1_equivp: "equivp alpha1" +lemma alpha1_equivp: "equivp alpha_rtrm1" sorry -quotient_type trm1 = rtrm1 / alpha1 +quotient_type trm1 = rtrm1 / alpha_rtrm1 by (rule alpha1_equivp) local_setup {* @@ -115,28 +145,30 @@ lemma alpha_rfv1: shows "t \1 s \ fv_rtrm1 t = fv_rtrm1 s" - apply(induct rule: alpha1.induct) + apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) apply(simp_all add: alpha_gen.simps) - sorry + done lemma [quot_respect]: - "(op = ===> alpha1) rVr1 rVr1" - "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" - "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" - "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" + "(op = ===> alpha_rtrm1) rVr1 rVr1" + "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" + "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" + "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" apply (auto simp add: alpha1_inj) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) apply (rule_tac x="0" in exI) +apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) +apply (rule_tac x="0" in exI) apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) done lemma [quot_respect]: - "(op = ===> alpha1 ===> alpha1) permute permute" + "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" by (simp add: alpha1_eqvt) lemma [quot_respect]: - "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" + "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" by (simp add: alpha_rfv1) lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] @@ -215,6 +247,12 @@ apply(simp_all) done +lemma helper: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" +apply auto +apply (rule_tac x="(x \ a)" in exI) +apply auto +done + lemma supp_fv: shows "supp t = fv_trm1 t" apply(induct t rule: trm1_bp_inducts(1)) @@ -233,11 +271,11 @@ apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \ supp (Abs (bv1 bp) rtrm12)") apply(simp add: supp_Abs fv_trm1 fv_eq_bv) apply(simp (no_asm) add: supp_def) -apply(simp add: alpha1_INJ) +apply(simp add: alpha1_INJ alpha_bp_eq) apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen) -apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) -apply(simp add: Collect_imp_eq Collect_neg_eq) +apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) +apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) done lemma trm1_supp: @@ -271,35 +309,27 @@ where "rbv2 (rAs x t) = {atom x}" -local_setup {* define_raw_fv "Terms.rtrm2" +setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} + +local_setup {* snd o define_fv_alpha "Terms.rtrm2" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], [[[], []]]] *} print_theorems -setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} - -inductive - alpha2 :: "rtrm2 \ rtrm2 \ bool" ("_ \2 _" [100, 100] 100) -and - alpha2a :: "rassign \ rassign \ bool" ("_ \2a _" [100, 100] 100) -where - a1: "a = b \ (rVr2 a) \2 (rVr2 b)" -| a2: "\t1 \2 t2; s1 \2 s2\ \ rAp2 t1 s1 \2 rAp2 t2 s2" -| a3: "(\pi. (({atom a}, t) \gen alpha2 fv_rtrm2 pi ({atom b}, s))) \ rLm2 a t \2 rLm2 b s" -| a4: "\\pi. ((rbv2 bt, t) \gen alpha2 fv_rtrm2 pi ((rbv2 bs), s)); - \pi. ((rbv2 bt, bt) \gen alpha2a fv_rassign pi (rbv2 bs, bs))\ - \ rLt2 bt t \2 rLt2 bs s" -| a5: "\a = b; t \2 s\ \ rAs a t \2a rAs b s" (* This way rbv2 can be lifted *) +notation + alpha_rtrm2 ("_ \2 _" [100, 100] 100) and + alpha_rassign ("_ \2b _" [100, 100] 100) +thm alpha_rtrm2_alpha_rassign.intros lemma alpha2_equivp: - "equivp alpha2" - "equivp alpha2a" + "equivp alpha_rtrm2" + "equivp alpha_rassign" sorry quotient_type - trm2 = rtrm2 / alpha2 + trm2 = rtrm2 / alpha_rtrm2 and - assign = rassign / alpha2a + assign = rassign / alpha_rassign by (auto intro: alpha2_equivp) local_setup {* @@ -333,36 +363,27 @@ "bv3 ANil = {}" | "bv3 (ACons x t as) = {atom x} \ (bv3 as)" -local_setup {* define_raw_fv "Terms.trm3" +setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} + +local_setup {* snd o define_fv_alpha "Terms.trm3" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], [[], [[], [], []]]] *} print_theorems -setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} - -inductive - alpha3 :: "trm3 \ trm3 \ bool" ("_ \3 _" [100, 100] 100) -and - alpha3a :: "assigns \ assigns \ bool" ("_ \3a _" [100, 100] 100) -where - a1: "a = b \ (Vr3 a) \3 (Vr3 b)" -| a2: "\t1 \3 t2; s1 \3 s2\ \ Ap3 t1 s1 \3 Ap3 t2 s2" -| a3: "(\pi. (({atom a}, t) \gen alpha3 fv_rtrm3 pi ({atom b}, s))) \ Lm3 a t \3 Lm3 b s" -| a4: "\\pi. ((bv3 bt, t) \gen alpha3 fv_trm3 pi ((bv3 bs), s)); - \pi. ((bv3 bt, bt) \gen alpha3a fv_assign pi (bv3 bs, bs))\ - \ Lt3 bt t \3 Lt3 bs s" -| a5: "ANil \3a ANil" -| a6: "\a = b; t \3 s; tt \3a st\ \ ACons a t tt \3a ACons b s st" +notation + alpha_trm3 ("_ \3 _" [100, 100] 100) and + alpha_assigns ("_ \3a _" [100, 100] 100) +thm alpha_trm3_alpha_assigns.intros lemma alpha3_equivp: - "equivp alpha3" - "equivp alpha3a" + "equivp alpha_trm3" + "equivp alpha_assigns" sorry quotient_type - qtrm3 = trm3 / alpha3 + qtrm3 = trm3 / alpha_trm3 and - qassigns = assigns / alpha3a + qassigns = assigns / alpha_assigns by (auto intro: alpha3_equivp) @@ -376,10 +397,6 @@ thm trm4.recs -local_setup {* define_raw_fv "Terms.trm4" [ - [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} -print_theorems - (* there cannot be a clause for lists, as *) (* permutations are already defined in Nominal (also functions, options, and so on) *) setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} @@ -395,22 +412,21 @@ thm permute_trm4_permute_trm4_list.simps thm permute_trm4_permute_trm4_list.simps[simplified repaired] -inductive - alpha4 :: "trm4 \ trm4 \ bool" ("_ \4 _" [100, 100] 100) -and alpha4list :: "trm4 list \ trm4 list \ bool" ("_ \4list _" [100, 100] 100) -where - a1: "a = b \ (Vr4 a) \4 (Vr4 b)" -| a2: "\t1 \4 t2; s1 \4list s2\ \ Ap4 t1 s1 \4 Ap4 t2 s2" -| a3: "(\pi. (({atom a}, t) \gen alpha4 fv_rtrm4 pi ({atom b}, s))) \ Lm4 a t \4 Lm4 b s" -| a5: "[] \4list []" -| a6: "\t \4 s; ts \4list ss\ \ (t#ts) \4list (s#ss)" +local_setup {* snd o define_fv_alpha "Terms.trm4" [ + [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} +print_theorems -lemma alpha4_equivp: "equivp alpha4" sorry -lemma alpha4list_equivp: "equivp alpha4list" sorry +notation + alpha_trm4 ("_ \4 _" [100, 100] 100) and + alpha_trm4_list ("_ \4l _" [100, 100] 100) +thm alpha_trm4_alpha_trm4_list.intros + +lemma alpha4_equivp: "equivp alpha_trm4" sorry +lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry quotient_type - qtrm4 = trm4 / alpha4 and - qtrm4list = "trm4 list" / alpha4list + qtrm4 = trm4 / alpha_trm4 and + qtrm4list = "trm4 list" / alpha_trm4_list by (simp_all add: alpha4_equivp alpha4list_equivp) @@ -429,66 +445,55 @@ | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" -local_setup {* define_raw_fv "Terms.rtrm5" [ +setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} print_theorems (* Alternate version with additional binding of name in rlts in rLcons *) -(*local_setup {* define_raw_fv "Terms.rtrm5" [ +(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} print_theorems*) - -setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} -print_theorems - -inductive - alpha5 :: "rtrm5 \ rtrm5 \ bool" ("_ \5 _" [100, 100] 100) -and - alphalts :: "rlts \ rlts \ bool" ("_ \l _" [100, 100] 100) -where - a1: "a = b \ (rVr5 a) \5 (rVr5 b)" -| a2: "\t1 \5 t2; s1 \5 s2\ \ rAp5 t1 s1 \5 rAp5 t2 s2" -| a3: "\\pi. ((rbv5 l1, t1) \gen alpha5 fv_rtrm5 pi (rbv5 l2, t2)); - \pi. ((rbv5 l1, l1) \gen alphalts fv_rlts pi (rbv5 l2, l2))\ - \ rLt5 l1 t1 \5 rLt5 l2 t2" -| a4: "rLnil \l rLnil" -| a5: "ls1 \l ls2 \ t1 \5 t2 \ n1 = n2 \ rLcons n1 t1 ls1 \l rLcons n2 t2 ls2" - -print_theorems +notation + alpha_rtrm5 ("_ \5 _" [100, 100] 100) and + alpha_rlts ("_ \l _" [100, 100] 100) +thm alpha_rtrm5_alpha_rlts.intros lemma alpha5_inj: "((rVr5 a) \5 (rVr5 b)) = (a = b)" "(rAp5 t1 s1 \5 rAp5 t2 s2) = (t1 \5 t2 \ s1 \5 s2)" - "(rLt5 l1 t1 \5 rLt5 l2 t2) = ((\pi. ((rbv5 l1, t1) \gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \ - (\pi. ((rbv5 l1, l1) \gen alphalts fv_rlts pi (rbv5 l2, l2))))" + "(rLt5 l1 t1 \5 rLt5 l2 t2) = ((\pi. ((rbv5 l1, t1) \gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \ + (\pi. ((rbv5 l1, l1) \gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))" "rLnil \l rLnil" "(rLcons n1 t1 ls1 \l rLcons n2 t2 ls2) = (n1 = n2 \ ls1 \l ls2 \ t1 \5 t2)" apply - -apply (simp_all add: alpha5_alphalts.intros) +apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) apply rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) +apply (erule alpha_rtrm5.cases) +apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) apply rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) +apply (erule alpha_rtrm5.cases) +apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) apply rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) +apply (erule alpha_rtrm5.cases) +apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) apply rule -apply (erule alphalts.cases) -apply (simp_all add: alpha5_alphalts.intros) +apply (erule alpha_rlts.cases) +apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) done lemma alpha5_equivps: - shows "equivp alpha5" - and "equivp alphalts" + shows "equivp alpha_rtrm5" + and "equivp alpha_rlts" sorry quotient_type - trm5 = rtrm5 / alpha5 + trm5 = rtrm5 / alpha_rtrm5 and - lts = rlts / alphalts + lts = rlts / alpha_rlts by (auto intro: alpha5_equivps) local_setup {* @@ -519,13 +524,13 @@ lemma alpha5_eqvt: "xa \5 y \ (x \ xa) \5 (x \ y)" "xb \l ya \ (x \ xb) \l (x \ ya)" - apply(induct rule: alpha5_alphalts.inducts) + apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) apply (simp_all add: alpha5_inj) apply (erule exE)+ apply(unfold alpha_gen) apply (erule conjE)+ apply (rule conjI) - apply (rule_tac x="x \ pi" in exI) + apply (rule_tac x="x \ pia" in exI) apply (rule conjI) apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) @@ -534,7 +539,7 @@ apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) apply (subst permute_eqvt[symmetric]) apply (simp) - apply (rule_tac x="x \ pia" in exI) + apply (rule_tac x="x \ pi" in exI) apply (rule conjI) apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) @@ -548,27 +553,27 @@ lemma alpha5_rfv: "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" "(l \l m \ fv_rlts l = fv_rlts m)" - apply(induct rule: alpha5_alphalts.inducts) + apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) apply(simp_all add: alpha_gen) done lemma bv_list_rsp: shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha5_alphalts.inducts(2)) + apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) apply(simp_all) done lemma [quot_respect]: - "(alphalts ===> op =) fv_rlts fv_rlts" - "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5" - "(alphalts ===> op =) rbv5 rbv5" - "(op = ===> alpha5) rVr5 rVr5" - "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" - "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" - "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" - "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" - "(op = ===> alpha5 ===> alpha5) permute permute" - "(op = ===> alphalts ===> alphalts) permute permute" + "(alpha_rlts ===> op =) fv_rlts fv_rlts" + "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" + "(alpha_rlts ===> op =) rbv5 rbv5" + "(op = ===> alpha_rtrm5) rVr5 rVr5" + "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" + "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" + "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" + "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" + "(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) @@ -579,7 +584,7 @@ done lemma - shows "(alphalts ===> op =) rbv5 rbv5" + shows "(alpha_rlts ===> op =) rbv5 rbv5" by (simp add: bv_list_rsp) lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] @@ -668,7 +673,7 @@ lemma distinct_helper: shows "\(rVr5 x \5 rAp5 y z)" apply auto - apply (erule alpha5.cases) + apply (erule alpha_rtrm5.cases) apply (simp_all only: rtrm5.distinct) done @@ -701,13 +706,15 @@ | "rbv6 (rLm6 n t) = {atom n} \ rbv6 t" | "rbv6 (rLt6 l r) = rbv6 l \ rbv6 r" -local_setup {* define_raw_fv "Terms.rtrm6" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} -print_theorems - setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} print_theorems +local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} +notation alpha_rtrm6 ("_ \6a _" [100, 100] 100) +(* HERE THE RULES DIFFER *) +thm alpha_rtrm6.intros + inductive alpha6 :: "rtrm6 \ rtrm6 \ bool" ("_ \6 _" [100, 100] 100) where @@ -841,13 +848,16 @@ | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" | "rbv7 (rLt7 l r) = rbv7 l \ rbv7 r" -local_setup {* define_raw_fv "Terms.rtrm7" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} -print_theorems - setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} print_theorems +local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} +notation + alpha_rtrm7 ("_ \7a _" [100, 100] 100) +(* HERE THE RULES DIFFER *) +thm alpha_rtrm7.intros + inductive alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) where @@ -884,13 +894,18 @@ "rbv8 (Bar0 x) = {}" | "rbv8 (Bar1 v x b) = {atom v}" -local_setup {* define_raw_fv "Terms.rfoo8" [ - [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} -print_theorems - setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} print_theorems +local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ + [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} +notation + alpha_rfoo8 ("_ \f' _" [100, 100] 100) and + alpha_rbar8 ("_ \b' _" [100, 100] 100) +(* HERE THE RULE DIFFERS *) +thm alpha_rfoo8_alpha_rbar8.intros + + inductive alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) and @@ -941,12 +956,17 @@ "rbv9 (Var9 x) = {}" | "rbv9 (Lam9 x b) = {atom x}" -local_setup {* define_raw_fv "Terms.rlam9" [ - [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} +setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} print_theorems -setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} -print_theorems +local_setup {* snd o define_fv_alpha "Terms.rlam9" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} +notation + alpha_rlam9 ("_ \9l' _" [100, 100] 100) and + alpha_rbla9 ("_ \9b' _" [100, 100] 100) +(* HERE THE RULES DIFFER *) +thm alpha_rlam9_alpha_rbla9.intros + inductive alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100)