Quot/Nominal/Terms.thy
changeset 1199 5770c73f2415
parent 1198 5523d5713a65
child 1200 a94c04c4a720
equal deleted inserted replaced
1198:5523d5713a65 1199:5770c73f2415
    29 | "bv1 (BVr x) = {atom x}"
    29 | "bv1 (BVr x) = {atom x}"
    30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
    30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
    31 
    31 
    32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
    32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
    33 
    33 
    34 ML {*
       
    35   val elims_ref = ref (@{thms refl})
       
    36   val intrs_ref = ref (@{thms refl})
       
    37 *}
       
    38 ML elims_ref
       
    39 local_setup {* 
    34 local_setup {* 
    40 fn ctxt =>
    35   snd o define_fv_alpha "Terms.rtrm1"
    41   let val ((fv, ind), ctxt') =
       
    42     define_fv_alpha "Terms.rtrm1"
       
    43   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
    36   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
    44   [[], [[]], [[], []]]] ctxt;
    37   [[], [[]], [[], []]]] *}
    45   val elims' = ProofContext.export ctxt' ctxt (#elims ind)
       
    46   val intrs' = ProofContext.export ctxt' ctxt (#intrs ind)
       
    47   val _ = (elims_ref := elims');
       
    48   val _ = (intrs_ref := intrs');
       
    49   in ctxt' end *}
       
    50 print_theorems
    38 print_theorems
    51 
    39 
    52 notation
    40 notation
    53   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
    41   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
    54   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
    42   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
    55 thm alpha_rtrm1_alpha_bp.intros
    43 thm alpha_rtrm1_alpha_bp.intros
    56 
    44 
    57 prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *}
    45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
    58 apply -
    46 thm alpha1_inj
    59 prefer 4
       
    60 apply (rule iffI)
       
    61 apply (tactic {* eresolve_tac (!elims_ref) 1 *})
       
    62 apply (simp only: rtrm1.distinct)
       
    63 apply (simp only: rtrm1.distinct)
       
    64 apply (simp only: rtrm1.distinct)
       
    65 apply (rule conjI) apply (simp only: rtrm1.inject)
       
    66 apply (rule conjI) apply (simp only: rtrm1.inject)
       
    67 apply (simp only: rtrm1.inject)
       
    68 apply (simp only: alpha_rtrm1_alpha_bp.intros)
       
    69 sorry
       
    70 
       
    71 lemma alpha1_inj:
       
    72 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
       
    73 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
       
    74 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))"
       
    75 "(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) =
       
    76    ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and>
       
    77    (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))"
       
    78 "alpha_bp BUnit BUnit"
       
    79 "(alpha_bp (BVr name) (BVr namea)) = (name = namea)"
       
    80 "(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)"
       
    81 apply -
       
    82 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    83 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    84 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    85 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    86 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    87 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
       
    88 done
       
    89 
    47 
    90 lemma alpha_bp_refl: "alpha_bp a a"
    48 lemma alpha_bp_refl: "alpha_bp a a"
    91 apply induct
    49 apply induct
    92 apply (simp_all  add: alpha1_inj)
    50 apply (simp_all  add: alpha1_inj)
    93 done
    51 done
   342 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
   300 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
   343 
   301 
   344 local_setup {* snd o define_fv_alpha "Terms.rtrm2"
   302 local_setup {* snd o define_fv_alpha "Terms.rtrm2"
   345   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
   303   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
   346    [[[], []]]] *}
   304    [[[], []]]] *}
   347 print_theorems
       
   348 
   305 
   349 notation
   306 notation
   350   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
   307   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
   351   alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
   308   alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
   352 thm alpha_rtrm2_alpha_rassign.intros
   309 thm alpha_rtrm2_alpha_rassign.intros
       
   310 
       
   311 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)) *}
       
   312 thm alpha2_inj
       
   313 
   353 
   314 
   354 lemma alpha2_equivp:
   315 lemma alpha2_equivp:
   355   "equivp alpha_rtrm2"
   316   "equivp alpha_rtrm2"
   356   "equivp alpha_rassign"
   317   "equivp alpha_rassign"
   357   sorry
   318   sorry
   490 notation
   451 notation
   491   alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
   452   alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
   492   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
   453   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
   493 thm alpha_rtrm5_alpha_rlts.intros
   454 thm alpha_rtrm5_alpha_rlts.intros
   494 
   455 
   495 lemma alpha5_inj:
   456 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
   496   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
   457 thm alpha5_inj
   497   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
       
   498   "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
       
   499          (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))"
       
   500   "rLnil \<approx>l rLnil"
       
   501   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
       
   502 apply -
       
   503 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
       
   504 apply rule
       
   505 apply (erule alpha_rtrm5.cases)
       
   506 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
       
   507 apply rule
       
   508 apply (erule alpha_rtrm5.cases)
       
   509 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
       
   510 apply rule
       
   511 apply (erule alpha_rtrm5.cases)
       
   512 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
       
   513 apply rule
       
   514 apply (erule alpha_rlts.cases)
       
   515 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
       
   516 done
       
   517 
   458 
   518 lemma alpha5_equivps:
   459 lemma alpha5_equivps:
   519   shows "equivp alpha_rtrm5"
   460   shows "equivp alpha_rtrm5"
   520   and   "equivp alpha_rlts"
   461   and   "equivp alpha_rlts"
   521 sorry
   462 sorry
   558   apply (simp_all add: alpha5_inj)
   499   apply (simp_all add: alpha5_inj)
   559   apply (erule exE)+
   500   apply (erule exE)+
   560   apply(unfold alpha_gen)
   501   apply(unfold alpha_gen)
   561   apply (erule conjE)+
   502   apply (erule conjE)+
   562   apply (rule conjI)
   503   apply (rule conjI)
       
   504   apply (rule_tac x="x \<bullet> pi" in exI)
       
   505   apply (rule conjI)
       
   506   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
       
   507   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
       
   508   apply(rule conjI)
       
   509   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
       
   510   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
       
   511   apply (subst permute_eqvt[symmetric])
       
   512   apply (simp)
   563   apply (rule_tac x="x \<bullet> pia" in exI)
   513   apply (rule_tac x="x \<bullet> pia" in exI)
   564   apply (rule conjI)
   514   apply (rule conjI)
   565   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
   515   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
   566   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
   516   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
   567   apply(rule conjI)
   517   apply(rule conjI)
   568   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
   518   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
   569   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
   519   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
   570   apply (subst permute_eqvt[symmetric])
       
   571   apply (simp)
       
   572   apply (rule_tac x="x \<bullet> pi" in exI)
       
   573   apply (rule conjI)
       
   574   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
       
   575   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
       
   576   apply(rule conjI)
       
   577   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
       
   578   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
       
   579   apply (subst permute_eqvt[symmetric])
   520   apply (subst permute_eqvt[symmetric])
   580   apply (simp)
   521   apply (simp)
   581   done
   522   done
   582 
   523 
   583 lemma alpha5_rfv:
   524 lemma alpha5_rfv:
   676 lemma lets_ok2:
   617 lemma lets_ok2:
   677   "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
   618   "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
   678    (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
   619    (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
   679 apply (subst alpha5_INJ)
   620 apply (subst alpha5_INJ)
   680 apply (rule conjI)
   621 apply (rule conjI)
   681 apply (rule_tac x="0 :: perm" in exI)
   622 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   682 apply (simp only: alpha_gen)
   623 apply (simp only: alpha_gen)
   683 apply (simp add: permute_trm5_lts fresh_star_def)
   624 apply (simp add: permute_trm5_lts fresh_star_def)
   684 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   625 apply (rule_tac x="0 :: perm" in exI)
   685 apply (simp only: alpha_gen)
   626 apply (simp only: alpha_gen)
   686 apply (simp add: permute_trm5_lts fresh_star_def)
   627 apply (simp add: permute_trm5_lts fresh_star_def)
   687 done
   628 done
   688 
   629 
   689 
   630 
   695 apply (simp add: alpha_gen)
   636 apply (simp add: alpha_gen)
   696 apply (simp add: permute_trm5_lts fresh_star_def)
   637 apply (simp add: permute_trm5_lts fresh_star_def)
   697 apply (simp add: alpha5_INJ(5))
   638 apply (simp add: alpha5_INJ(5))
   698 apply(clarify)
   639 apply(clarify)
   699 apply (simp add: alpha5_INJ(2))
   640 apply (simp add: alpha5_INJ(2))
   700 apply (simp only: alpha5_INJ(1))
   641 apply (simp add: alpha5_INJ(1))
   701 done
   642 done
   702 
   643 
   703 lemma distinct_helper:
   644 lemma distinct_helper:
   704   shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
   645   shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
   705   apply auto
   646   apply auto
  1066   All "name set" "ty" 
  1007   All "name set" "ty" 
  1067 
  1008 
  1068 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
  1009 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
  1069 print_theorems
  1010 print_theorems
  1070 
  1011 
  1071 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
  1012 local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *}
  1072 print_theorems 
  1013 print_theorems 
  1073 
  1014 
  1074 (*
  1015 (*
  1075 Doesnot work yet since we do not refer to fv_ty
  1016 Doesnot work yet since we do not refer to fv_ty
  1076 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
  1017 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}