diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term6.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term6.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,155 @@ +theory Term6 +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +begin + +atom_decl name + +(* example with a bn function defined over the type itself, NOT respectful. *) + +datatype rtrm6 = + rVr6 "name" +| rLm6 "name" "rtrm6" --"bind name in 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" + +setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "Term6.rtrm6" [ + [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} +notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) +thm alpha_rtrm6.intros + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} +thm alpha6_inj + +local_setup {* +snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) +*} + +local_setup {* +snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} +*} + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) +*} + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), + (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} +thm alpha6_equivp + +quotient_type + trm6 = rtrm6 / alpha_rtrm6 + by (auto intro: alpha6_equivp) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) + |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) + |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) +*} +print_theorems + +lemma [quot_respect]: + "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" +by (auto simp add: alpha6_eqvt) + +(* Definitely not true , see lemma below *) +lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" +apply simp apply clarify +apply (erule alpha_rtrm6.induct) +oops + +lemma "(a :: name) \ b \ \ (alpha_rtrm6 ===> 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 (simp add: alpha6_inj) +apply (rule_tac x="(a \ b)" in exI) +apply (simp add: alpha_gen fresh_star_def) +apply (simp add: alpha6_inj) +done + +lemma fv6_rsp: "x \6 y \ fv_rtrm6 x = fv_rtrm6 y" +apply (induct_tac x y rule: alpha_rtrm6.induct) +apply simp_all +apply (erule exE) +apply (simp_all add: alpha_gen) +done + +lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" +by (simp add: fv6_rsp) + +lemma [quot_respect]: + "(op = ===> alpha_rtrm6) rVr6 rVr6" + "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" +apply auto +apply (simp_all add: alpha6_inj) +apply (rule_tac x="0::perm" in exI) +apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) +done + +lemma [quot_respect]: + "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" +apply auto +apply (simp_all add: alpha6_inj) +apply (rule_tac [!] x="0::perm" in exI) +apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) +(* 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; \name namea. name = namea \ P (Vr6 name) (Vr6 namea); + \name rtrm6 namea rtrm6a. + \True; + \pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \ + (fv_trm6 rtrm6 - {atom name}) \* pi \ pi \ rtrm6 = rtrm6a \ P (pi \ rtrm6) rtrm6a\ + \ P (Lm6 name rtrm6) (Lm6 namea rtrm6a); + \rtrm61 rtrm61a rtrm62 rtrm62a. + \rtrm61 = rtrm61a; P rtrm61 rtrm61a; + \pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ + (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a \ P (pi \ rtrm62) rtrm62a\ + \ P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\ +\ P x1 x2" +apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) +apply injection +(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) +oops + +lemma lifted_inject_a3: +"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = +(rtrm61 = rtrm61a \ + (\pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ + (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a))" +apply(lifting alpha6_inj(3)[unfolded alpha_gen]) +apply injection +(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) +oops + + + + +end