diff -r cb3da5b540f2 -r 85501074fd4f Quot/Nominal/Terms2.thy --- a/Quot/Nominal/Terms2.thy Thu Feb 18 08:37:45 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1143 +0,0 @@ -theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" -begin - -atom_decl name - -text {* primrec seems to be genarally faster than fun *} - -section {*** lets with binding patterns ***} - -datatype rtrm1 = - rVr1 "name" -| rAp1 "rtrm1" "rtrm1" -| rLm1 "name" "rtrm1" --"name is bound in trm1" -| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" -and bp = - 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 bp2)" - -local_setup {* define_raw_fv "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" - -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))))" -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) -done - -(* Shouyld we derive it? But bv is given by the user? *) -lemma bv1_eqvt[eqvt]: - shows "(pi \ bv1 x) = bv1 (pi \ x)" - apply (induct x) -apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) -done - -lemma fv_rtrm1_eqvt[eqvt]: - "(pi\fv_rtrm1 t) = fv_rtrm1 (pi\t)" - "(pi\fv_bp b) = fv_bp (pi\b)" - apply (induct t and b) - 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) - apply (simp_all add:eqvts alpha1_inj) - apply (erule exE) - apply (rule_tac x="pi \ pia" 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: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) - apply(simp add: permute_eqvt[symmetric]) - apply (erule exE) - apply (rule_tac x="pi \ pia" 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" - sorry - -quotient_type trm1 = rtrm1 / alpha1 - by (rule alpha1_equivp) - -quotient_definition - "Vr1 :: name \ trm1" -is - "rVr1" - -quotient_definition - "Ap1 :: trm1 \ trm1 \ trm1" -is - "rAp1" - -quotient_definition - "Lm1 :: name \ trm1 \ trm1" -is - "rLm1" - -quotient_definition - "Lt1 :: bp \ trm1 \ trm1 \ trm1" -is - "rLt1" - -quotient_definition - "fv_trm1 :: trm1 \ atom set" -is - "fv_rtrm1" - -lemma alpha_rfv1: - shows "t \1 s \ fv_rtrm1 t = fv_rtrm1 s" - apply(induct rule: alpha1.induct) - apply(simp_all add: alpha_gen.simps) - sorry - -lemma [quot_respect]: - "(op = ===> alpha1) rVr1 rVr1" - "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" - "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" - "(op = ===> alpha1 ===> alpha1 ===> alpha1) 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) -done - -lemma [quot_respect]: - "(op = ===> alpha1 ===> alpha1) permute permute" - by (simp add: alpha1_eqvt) - -lemma [quot_respect]: - "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" - by (simp add: alpha_rfv1) - -lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] -lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] - -instantiation trm1 and bp :: pt -begin - -quotient_definition - "permute_trm1 :: perm \ trm1 \ trm1" -is - "permute :: perm \ rtrm1 \ rtrm1" - -lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] - -instance -apply default -apply(induct_tac [!] x rule: trm1_bp_inducts(1)) -apply(simp_all) -done - -end - -lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] - -lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] - -lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] - -lemma lm1_supp_pre: - shows "(supp (atom x, t)) supports (Lm1 x t) " -apply(simp add: supports_def) -apply(fold fresh_def) -apply(simp add: fresh_Pair swap_fresh_fresh) -apply(clarify) -apply(subst swap_at_base_simps(3)) -apply(simp_all add: fresh_atom) -done - -lemma lt1_supp_pre: - shows "(supp (x, t, s)) supports (Lt1 t x s) " -apply(simp add: supports_def) -apply(fold fresh_def) -apply(simp add: fresh_Pair swap_fresh_fresh) -done - -lemma bp_supp: "finite (supp (bp :: bp))" - apply (induct bp) - apply(simp_all add: supp_def) - apply (fold supp_def) - apply (simp add: supp_at_base) - apply(simp add: Collect_imp_eq) - apply(simp add: Collect_neg_eq[symmetric]) - apply (fold supp_def) - apply (simp) - done - -instance trm1 :: fs -apply default -apply(induct_tac x rule: trm1_bp_inducts(1)) -apply(simp_all) -apply(simp add: supp_def alpha1_INJ eqvts) -apply(simp add: supp_def[symmetric] supp_at_base) -apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) -apply(simp add: Collect_imp_eq Collect_neg_eq) -apply(rule supports_finite) -apply(rule lm1_supp_pre) -apply(simp add: supp_Pair supp_atom) -apply(rule supports_finite) -apply(rule lt1_supp_pre) -apply(simp add: supp_Pair supp_atom bp_supp) -done - -lemma fv_eq_bv: "fv_bp bp = bv1 bp" -apply(induct bp rule: trm1_bp_inducts(2)) -apply(simp_all) -done - -lemma supp_fv: - shows "supp t = fv_trm1 t" -apply(induct t rule: trm1_bp_inducts(1)) -apply(simp_all) -apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp only: supp_at_base[simplified supp_def]) -apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp add: Collect_imp_eq Collect_neg_eq) -apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") -apply(simp add: supp_Abs fv_trm1) -apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) -apply(simp add: alpha1_INJ) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen.simps) -apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) -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: 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) -done - -lemma trm1_supp: - "supp (Vr1 x) = {atom x}" - "supp (Ap1 t1 t2) = supp t1 \ supp t2" - "supp (Lm1 x t) = (supp t) - {atom x}" - "supp (Lt1 b t s) = supp t \ (supp s - bv1 b)" -by (simp_all add: supp_fv fv_trm1 fv_eq_bv) - -lemma trm1_induct_strong: - assumes "\name b. P b (Vr1 name)" - and "\rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12\ \ P b (Ap1 rtrm11 rtrm12)" - and "\name rtrm1 b. \\c. P c rtrm1; (atom name) \ b\ \ P b (Lm1 name rtrm1)" - and "\bp rtrm11 rtrm12 b. \\c. P c rtrm11; \c. P c rtrm12; bv1 bp \* b\ \ P b (Lt1 bp rtrm11 rtrm12)" - shows "P a rtrma" -sorry - -section {*** lets with single assignments ***} - -datatype rtrm2 = - rVr2 "name" -| rAp2 "rtrm2" "rtrm2" -| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" -| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" -and rassign = - rAs "name" "rtrm2" - -(* to be given by the user *) -primrec - rbv2 -where - "rbv2 (rAs x t) = {atom x}" - -local_setup {* define_raw_fv "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 *) - -lemma alpha2_equivp: - "equivp alpha2" - "equivp alpha2a" - sorry - -quotient_type - trm2 = rtrm2 / alpha2 -and - assign = rassign / alpha2a - by (auto intro: alpha2_equivp) - - - -section {*** lets with many assignments ***} - -datatype trm3 = - Vr3 "name" -| Ap3 "trm3" "trm3" -| Lm3 "name" "trm3" --"bind (name) in (trm3)" -| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" -and assigns = - ANil -| ACons "name" "trm3" "assigns" - -(* to be given by the user *) -primrec - bv3 -where - "bv3 ANil = {}" -| "bv3 (ACons x t as) = {atom x} \ (bv3 as)" - -local_setup {* define_raw_fv "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" - -lemma alpha3_equivp: - "equivp alpha3" - "equivp alpha3a" - sorry - -quotient_type - qtrm3 = trm3 / alpha3 -and - qassigns = assigns / alpha3a - by (auto intro: alpha3_equivp) - - -section {*** lam with indirect list recursion ***} - -datatype trm4 = - Vr4 "name" -| Ap4 "trm4" "trm4 list" -| Lm4 "name" "trm4" --"bind (name) in (trm)" -print_theorems - -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"] *} - -(* "repairing" of the permute function *) -lemma repaired: - fixes ts::"trm4 list" - shows "permute_trm4_list p ts = p \ ts" - apply(induct ts) - apply(simp_all) - done - -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)" - -lemma alpha4_equivp: "equivp alpha4" sorry -lemma alpha4list_equivp: "equivp alpha4list" sorry - -quotient_type - qtrm4 = trm4 / alpha4 and - qtrm4list = "trm4 list" / alpha4list - by (simp_all add: alpha4_equivp alpha4list_equivp) - - -datatype rtrm5 = - rVr5 "name" -| rAp5 "rtrm5" "rtrm5" -| 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)" - -local_setup {* define_raw_fv "Terms.rtrm5" [ - [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 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 - -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))))" - "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 rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) -apply rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) -apply rule -apply (erule alpha5.cases) -apply (simp_all add: alpha5_alphalts.intros) -apply rule -apply (erule alphalts.cases) -apply (simp_all add: alpha5_alphalts.intros) -done - -lemma alpha5_equivps: - shows "equivp alpha5" - and "equivp alphalts" -sorry - -quotient_type - trm5 = rtrm5 / alpha5 -and - lts = rlts / alphalts - by (auto intro: alpha5_equivps) - -quotient_definition - "Vr5 :: name \ trm5" -is - "rVr5" - -quotient_definition - "Ap5 :: trm5 \ trm5 \ trm5" -is - "rAp5" - -quotient_definition - "Lt5 :: lts \ trm5 \ trm5" -is - "rLt5" - -quotient_definition - "Lnil :: lts" -is - "rLnil" - -quotient_definition - "Lcons :: name \ trm5 \ lts \ lts" -is - "rLcons" - -quotient_definition - "fv_trm5 :: trm5 \ atom set" -is - "fv_rtrm5" - -quotient_definition - "fv_lts :: lts \ atom set" -is - "fv_rlts" - -quotient_definition - "bv5 :: lts \ atom set" -is - "rbv5" - -lemma rbv5_eqvt: - "pi \ (rbv5 x) = rbv5 (pi \ x)" -sorry - -lemma fv_rtrm5_eqvt: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" -sorry - -lemma fv_rlts_eqvt: - "pi \ (fv_rlts x) = fv_rlts (pi \ x)" -sorry - -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 (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 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) - apply(rule conjI) - apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) - 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 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) - apply(rule conjI) - apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) - apply (subst permute_eqvt[symmetric]) - apply (simp) - done - -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(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(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" - 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 (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - 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 (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - done - -lemma - shows "(alphalts ===> op =) rbv5 rbv5" - by (simp add: bv_list_rsp) - -lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] - -instantiation trm5 and lts :: pt -begin - -quotient_definition - "permute_trm5 :: perm \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ rlts" - -lemma trm5_lts_zero: - "0 \ (x\trm5) = x" - "0 \ (y\lts) = y" -apply(induct x and y rule: trm5_lts_inducts) -apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) -done - -lemma trm5_lts_plus: - "(p + q) \ (x\trm5) = p \ q \ x" - "(p + q) \ (y\lts) = p \ q \ y" -apply(induct x and y rule: trm5_lts_inducts) -apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) -done - -instance -apply default -apply (simp_all add: trm5_lts_zero trm5_lts_plus) -done - -end - -lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] - -lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] - -lemmas bv5[simp] = rbv5.simps[quot_lifted] - -lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] - -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 (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="0 :: perm" in exI) -apply (simp only: 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) -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 (subst alpha5_INJ(3)) -apply(clarify) -apply (simp add: alpha_gen) -apply (simp add: permute_trm5_lts fresh_star_def) -apply (simp add: alpha5_INJ(5)) -apply(clarify) -apply (simp add: alpha5_INJ(2)) -apply (simp only: alpha5_INJ(1)) -done - -lemma distinct_helper: - shows "\(rVr5 x \5 rAp5 y z)" - apply auto - apply (erule alpha5.cases) - apply (simp_all only: rtrm5.distinct) - done - -lemma distinct_helper2: - shows "(Vr5 x) \ (Ap5 y z)" - by (lifting distinct_helper) - -lemma lets_nok: - "x \ y \ x \ z \ z \ y \ - (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 (subst alpha5_INJ) -apply (simp only: alpha_gen permute_trm5_lts fresh_star_def) -apply (subst alpha5_INJ(5)) -apply (subst alpha5_INJ(5)) -apply (simp add: distinct_helper2) -done - - -(* example with a bn function defined over the type itself *) -datatype rtrm6 = - rVr6 "name" -| rLm6 "name" "rtrm6" -| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" - -primrec - rbv6 -where - "rbv6 (rVr6 n) = {}" -| "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 - -inductive - alpha6 :: "rtrm6 \ rtrm6 \ bool" ("_ \6 _" [100, 100] 100) -where - a1: "a = b \ (rVr6 a) \6 (rVr6 b)" -| a2: "(\pi. (({atom a}, t) \gen alpha6 fv_rtrm6 pi ({atom b}, s))) \ rLm6 a t \6 rLm6 b s" -| a3: "(\pi. (((rbv6 t1), s1) \gen alpha6 fv_rtrm6 pi ((rbv6 t2), s2))) \ rLt6 t1 s1 \6 rLt6 t2 s2" - -lemma alpha6_equivps: - shows "equivp alpha6" -sorry - -quotient_type - trm6 = rtrm6 / alpha6 - by (auto intro: alpha6_equivps) - -quotient_definition - "Vr6 :: name \ trm6" -is - "rVr6" - -quotient_definition - "Lm6 :: name \ trm6 \ trm6" -is - "rLm6" - -quotient_definition - "Lt6 :: trm6 \ trm6 \ trm6" -is - "rLt6" - -quotient_definition - "fv_trm6 :: trm6 \ atom set" -is - "fv_rtrm6" - -quotient_definition - "bv6 :: trm6 \ atom set" -is - "rbv6" - -lemma [quot_respect]: - "(op = ===> alpha6 ===> alpha6) permute permute" -apply auto (* will work with eqvt *) -sorry - -(* Definitely not true , see lemma below *) - -lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" -apply simp apply clarify -apply (erule alpha6.induct) -oops - -lemma "(a :: name) \ b \ \ (alpha6 ===> op =) rbv6 rbv6" -apply simp -apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) -apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) -apply simp -apply (rule a2) -apply (rule_tac x="(a \ b)" in exI) -apply (simp add: alpha_gen fresh_star_def) -apply (rule a1) -apply (rule refl) -done - -lemma [quot_respect]:"(alpha6 ===> op =) fv_rtrm6 fv_rtrm6" -apply simp apply clarify -apply (induct_tac x y rule: alpha6.induct) -apply simp_all -apply (erule exE) -apply (simp_all add: alpha_gen) -apply (erule conjE)+ -apply (erule exE) -apply (erule conjE)+ -apply (simp) -oops - - -lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6" -by (simp_all add: a1) - -lemma [quot_respect]: - "(op = ===> alpha6 ===> alpha6) rLm6 rLm6" - "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6" -apply simp_all apply (clarify) -apply (rule a2) -apply (rule_tac x="0::perm" in exI) -apply (simp add: alpha_gen) -(* needs rfv6_rsp *) defer -apply clarify -apply (rule a3) -apply (rule_tac x="0::perm" in exI) -apply (simp add: alpha_gen) -(* needs rbv6_rsp *) -oops - -instantiation trm6 :: pt begin - -quotient_definition - "permute_trm6 :: perm \ trm6 \ trm6" -is - "permute :: perm \ rtrm6 \ rtrm6" - -instance -apply default -sorry -end - -lemma lifted_induct: -"\x1 = x2; \a b. a = b \ P (Vr6 a) (Vr6 b); - \a t b s. - \pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \ - (fv_trm6 t - {atom a}) \* pi \ pi \ t = s \ P (pi \ t) s \ - P (Lm6 a t) (Lm6 b s); - \t1 s1 t2 s2. - \pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \ - (fv_trm6 s1 - bv6 t1) \* pi \ pi \ s1 = s2 \ P (pi \ s1) s2 \ - P (Lt6 t1 s1) (Lt6 t2 s2)\ - \ P x1 x2" -unfolding alpha_gen -apply (lifting alpha6.induct[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *) -oops - -lemma lifted_inject_a3: - "\pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \ - (fv_trm6 s1 - bv6 t1) \* pi \ pi \ s1 = s2 \ Lt6 t1 s1 = Lt6 t2 s2" -apply(lifting a3[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *) -oops - - - - -(* example with a respectful bn function defined over the type itself *) - -datatype rtrm7 = - rVr7 "name" -| rLm7 "name" "rtrm7" -| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" - -primrec - rbv7 -where - "rbv7 (rVr7 n) = {atom n}" -| "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 - -inductive - alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) -where - a1: "a = b \ (rVr7 a) \7 (rVr7 b)" -| a2: "(\pi. (({atom a}, t) \gen alpha7 fv_rtrm7 pi ({atom b}, s))) \ rLm7 a t \7 rLm7 b s" -| a3: "(\pi. (((rbv7 t1), s1) \gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \ rLt7 t1 s1 \7 rLt7 t2 s2" - -lemma "(x::name) \ y \ \ (alpha7 ===> op =) rbv7 rbv7" - apply simp - apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) - apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) - apply simp - apply (rule a3) - apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alpha_gen fresh_star_def) - apply (rule a1) - apply (rule refl) -done - - - - - -datatype rfoo8 = - Foo0 "name" -| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" -and rbar8 = - Bar0 "name" -| Bar1 "name" "name" "rbar8" --"bind second name in b" - -primrec - rbv8 -where - "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 - -inductive - alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) -and - alpha8b :: "rbar8 \ rbar8 \ bool" ("_ \b _" [100, 100] 100) -where - a1: "a = b \ (Foo0 a) \f (Foo0 b)" -| a2: "a = b \ (Bar0 a) \b (Bar0 b)" -| a3: "b1 \b b2 \ (\pi. (((rbv8 b1), t1) \gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \ Foo1 b1 t1 \f Foo1 b2 t2" -| a4: "v1 = v2 \ (\pi. (({atom x1}, t1) \gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \ Bar1 v1 x1 t1 \b Bar1 v2 x2 t2" - -lemma "(alpha8b ===> op =) rbv8 rbv8" - apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all) -done - -lemma fv_rbar8_rsp_hlp: "x \b y \ fv_rbar8 x = fv_rbar8 y" - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all add: alpha_gen) -done -lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" - apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) -done - -lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" - apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(1)) - apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) - apply clarify - apply (erule alpha8f_alpha8b.inducts(2)) - apply (simp_all) -done - - - - - - -datatype rlam9 = - Var9 "name" -| Lam9 "name" "rlam9" --"bind name in rlam" -and rbla9 = - Bla9 "rlam9" "rlam9" --"bind bv(first) in second" - -primrec - rbv9 -where - "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)]]]] *} -print_theorems - -setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} -print_theorems - -inductive - alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100) -and - alpha9b :: "rbla9 \ rbla9 \ bool" ("_ \9b _" [100, 100] 100) -where - a1: "a = b \ (Var9 a) \9l (Var9 b)" -| a4: "(\pi. (({atom x1}, t1) \gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \ Lam9 x1 t1 \9l Lam9 x2 t2" -| a3: "b1 \9l b2 \ (\pi. (((rbv9 b1), t1) \gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \ Bla9 b1 t1 \9b Bla9 b2 t2" - -quotient_type - lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b -sorry - -quotient_definition - "qVar9 :: name \ lam9" -is - "Var9" - -quotient_definition - "qLam :: name \ lam9 \ lam9" -is - "Lam9" - -quotient_definition - "qBla9 :: lam9 \ lam9 \ bla9" -is - "Bla9" - -quotient_definition - "fv_lam9 :: lam9 \ atom set" -is - "fv_rlam9" - -quotient_definition - "fv_bla9 :: bla9 \ atom set" -is - "fv_rbla9" - -quotient_definition - "bv9 :: lam9 \ atom set" -is - "rbv9" - -instantiation lam9 and bla9 :: pt -begin - -quotient_definition - "permute_lam9 :: perm \ lam9 \ lam9" -is - "permute :: perm \ rlam9 \ rlam9" - -quotient_definition - "permute_bla9 :: perm \ bla9 \ bla9" -is - "permute :: perm \ rbla9 \ rbla9" - -instance -sorry - -end - -lemma "\b1 = b2; \pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \ (fv_lam9 t1 - bv9 b1) \* pi \ pi \ t1 = t2\ - \ qBla9 b1 t1 = qBla9 b2 t2" -apply (lifting a3[unfolded alpha_gen]) -apply injection -sorry - - - - - - - - -text {* type schemes *} -datatype ty = - Var "name" -| Fun "ty" "ty" - -setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *} -print_theorems - -datatype tyS = - All "name set" "ty" - -setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} -print_theorems - -abbreviation - "atoms xs \ {atom x| x. x \ xs}" - -local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} -print_theorems - -(* -doesn't work yet -local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} -print_theorems -*) - -primrec - fv_tyS -where - "fv_tyS (All xs T) = (fv_ty T - atoms xs)" - -inductive - alpha_tyS :: "tyS \ tyS \ bool" ("_ \tyS _" [100, 100] 100) -where - a1: "\pi. ((atoms xs1, T1) \gen (op =) fv_ty pi (atoms xs2, T2)) - \ All xs1 T1 \tyS All xs2 T2" - -lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {b, a} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done - -lemma - shows "All {a, b} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var b) (Var a))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: fresh_star_def) - done - -lemma - shows "All {a, b, c} (Fun (Var a) (Var b)) \tyS All {a, b} (Fun (Var a) (Var b))" - apply(rule a1) - apply(simp add: alpha_gen) - apply(rule_tac x="0::perm" in exI) - apply(simp add: fresh_star_def) - done - -lemma - assumes a: "a \ b" - shows "\(All {a, b} (Fun (Var a) (Var b)) \tyS All {c} (Fun (Var c) (Var c)))" - using a - apply(clarify) - apply(erule alpha_tyS.cases) - apply(simp add: alpha_gen) - apply(erule conjE)+ - apply(erule exE) - apply(erule conjE)+ - apply(clarify) - apply(simp) - apply(simp add: fresh_star_def) - apply(auto) - done - - -end