114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
116 apply(simp add: permute_eqvt[symmetric]) |
116 apply(simp add: permute_eqvt[symmetric]) |
117 done |
117 done |
118 |
118 |
119 ML {* |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
120 build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} @{context} |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
121 *} |
121 thm alpha1_equivp |
122 ML Variable.export |
122 |
123 |
123 (*prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
124 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
|
125 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
124 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
126 |
125 |
127 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
126 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
128 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) |
127 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) |
129 |
128 |
130 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
129 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} |
131 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) |
130 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) |
132 |
|
133 lemma transp_aux: |
|
134 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
|
135 unfolding transp_def |
|
136 by blast |
|
137 |
131 |
138 lemma alpha1_equivp: |
132 lemma alpha1_equivp: |
139 "equivp alpha_rtrm1" |
133 "equivp alpha_rtrm1" |
140 "equivp alpha_bp" |
134 "equivp alpha_bp" |
141 apply (tactic {* |
135 apply (tactic {* |
145 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
139 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
146 resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} |
140 resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} |
147 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
141 THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) |
148 ) |
142 ) |
149 1 *}) |
143 1 *}) |
150 done |
144 done*) |
151 |
145 |
152 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
146 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
153 by (rule alpha1_equivp(1)) |
147 by (rule alpha1_equivp(1)) |
154 |
148 |
155 local_setup {* |
149 local_setup {* |
343 thm alpha_rtrm2_alpha_rassign.intros |
337 thm alpha_rtrm2_alpha_rassign.intros |
344 |
338 |
345 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} |
339 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} |
346 thm alpha2_inj |
340 thm alpha2_inj |
347 |
341 |
348 |
342 lemma alpha2_eqvt: |
349 lemma alpha2_equivp: |
343 "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)" |
350 "equivp alpha_rtrm2" |
344 "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)" |
351 "equivp alpha_rassign" |
345 sorry |
352 sorry |
346 |
|
347 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), |
|
348 (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *} |
|
349 thm alpha2_equivp |
|
350 |
353 |
351 |
354 quotient_type |
352 quotient_type |
355 trm2 = rtrm2 / alpha_rtrm2 |
353 trm2 = rtrm2 / alpha_rtrm2 |
356 and |
354 and |
357 assign = rassign / alpha_rassign |
355 assign = rassign / alpha_rassign |
358 by (auto intro: alpha2_equivp) |
356 by (rule alpha2_equivp(1)) (rule alpha2_equivp(2)) |
359 |
357 |
360 local_setup {* |
358 local_setup {* |
361 (fn ctxt => ctxt |
359 (fn ctxt => ctxt |
362 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
360 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
363 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
361 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
398 notation |
396 notation |
399 alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and |
397 alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and |
400 alpha_rassigns ("_ \<approx>3a _" [100, 100] 100) |
398 alpha_rassigns ("_ \<approx>3a _" [100, 100] 100) |
401 thm alpha_rtrm3_alpha_rassigns.intros |
399 thm alpha_rtrm3_alpha_rassigns.intros |
402 |
400 |
403 lemma alpha3_equivp: |
401 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *} |
404 "equivp alpha_rtrm3" |
402 thm alpha3_inj |
405 "equivp alpha_rassigns" |
403 |
406 sorry |
404 lemma alpha3_eqvt: |
|
405 "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)" |
|
406 "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)" |
|
407 sorry |
|
408 |
|
409 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []), |
|
410 (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *} |
|
411 thm alpha3_equivp |
407 |
412 |
408 quotient_type |
413 quotient_type |
409 trm3 = rtrm3 / alpha_rtrm3 |
414 trm3 = rtrm3 / alpha_rtrm3 |
410 and |
415 and |
411 assigns = rassigns / alpha_rassigns |
416 assigns = rassigns / alpha_rassigns |
412 by (auto intro: alpha3_equivp) |
417 by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) |
413 |
418 |
414 |
419 |
415 section {*** lam with indirect list recursion ***} |
420 section {*** lam with indirect list recursion ***} |
416 |
421 |
417 datatype rtrm4 = |
422 datatype rtrm4 = |
418 rVr4 "name" |
423 rVr4 "name" |
419 | rAp4 "rtrm4" "rtrm4 list" |
424 | rAp4 "rtrm4" "rtrm4 list" |
420 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
425 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
|
426 print_theorems |
421 |
427 |
422 thm rtrm4.recs |
428 thm rtrm4.recs |
423 |
429 |
424 (* there cannot be a clause for lists, as *) |
430 (* there cannot be a clause for lists, as *) |
425 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
431 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
442 |
448 |
443 notation |
449 notation |
444 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
450 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
445 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
451 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
446 thm alpha_rtrm4_alpha_rtrm4_list.intros |
452 thm alpha_rtrm4_alpha_rtrm4_list.intros |
|
453 |
|
454 (*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} *) |
|
455 |
|
456 lemma alpha4_eqvt: |
|
457 "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)" |
|
458 "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)" |
|
459 sorry |
|
460 |
|
461 (*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
|
462 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rassigns}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject rassigns.inject} @{thms alpha4_inj} @{thms rtrm4.distinct rassigns.distinct} @{thms alpha_rtrm4.cases alpha_rassigns.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}*) |
|
463 |
447 |
464 |
448 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
465 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
449 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
466 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
450 |
467 |
451 quotient_type |
468 quotient_type |
528 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
545 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
529 apply (subst permute_eqvt[symmetric]) |
546 apply (subst permute_eqvt[symmetric]) |
530 apply (simp) |
547 apply (simp) |
531 done |
548 done |
532 |
549 |
533 prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} |
550 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
534 by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *}) |
551 (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)) *} |
535 |
552 thm alpha5_equivp |
536 prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} |
|
537 by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *}) |
|
538 |
|
539 prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} |
|
540 by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *}) |
|
541 |
|
542 lemma alpha5_equivps: |
|
543 shows "equivp alpha_rtrm5" |
|
544 and "equivp alpha_rlts" |
|
545 ML_prf Goal.prove |
|
546 unfolding equivp_reflp_symp_transp reflp_def |
|
547 apply (simp_all add: alpha5_reflp_aux) |
|
548 unfolding symp_def |
|
549 apply (simp_all add: alpha5_symp_aux) |
|
550 unfolding transp_def |
|
551 apply (simp_all only: helper) |
|
552 apply (rule allI)+ |
|
553 apply (rule conjunct1[OF alpha5_transp_aux]) |
|
554 apply (rule allI)+ |
|
555 apply (rule conjunct2[OF alpha5_transp_aux]) |
|
556 done |
|
557 |
553 |
558 quotient_type |
554 quotient_type |
559 trm5 = rtrm5 / alpha_rtrm5 |
555 trm5 = rtrm5 / alpha_rtrm5 |
560 and |
556 and |
561 lts = rlts / alpha_rlts |
557 lts = rlts / alpha_rlts |
562 by (auto intro: alpha5_equivps) |
558 by (auto intro: alpha5_equivp) |
563 |
559 |
564 local_setup {* |
560 local_setup {* |
565 (fn ctxt => ctxt |
561 (fn ctxt => ctxt |
566 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
562 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
567 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
563 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
728 thm alpha_rtrm6.intros |
724 thm alpha_rtrm6.intros |
729 |
725 |
730 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)) *} |
726 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)) *} |
731 thm alpha6_inj |
727 thm alpha6_inj |
732 |
728 |
733 lemma alpha6_equivps: |
729 lemma alpha6_eqvt: |
734 shows "equivp alpha6" |
730 "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)" |
735 sorry |
731 sorry |
|
732 |
|
733 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
|
734 (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)) *} |
|
735 thm alpha6_equivp |
736 |
736 |
737 quotient_type |
737 quotient_type |
738 trm6 = rtrm6 / alpha_rtrm6 |
738 trm6 = rtrm6 / alpha_rtrm6 |
739 by (auto intro: alpha6_equivps) |
739 by (auto intro: alpha6_equivp) |
740 |
740 |
741 local_setup {* |
741 local_setup {* |
742 (fn ctxt => ctxt |
742 (fn ctxt => ctxt |
743 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
743 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
744 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
744 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
748 *} |
748 *} |
749 print_theorems |
749 print_theorems |
750 |
750 |
751 lemma [quot_respect]: |
751 lemma [quot_respect]: |
752 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" |
752 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" |
753 apply auto (* will work with eqvt *) |
753 by (auto simp add: alpha6_eqvt) |
754 sorry |
|
755 |
754 |
756 (* Definitely not true , see lemma below *) |
755 (* Definitely not true , see lemma below *) |
757 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" |
756 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" |
758 apply simp apply clarify |
757 apply simp apply clarify |
759 apply (erule alpha_rtrm6.induct) |
758 apply (erule alpha_rtrm6.induct) |