Nominal/Term5.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 10 Mar 2010 12:48:55 +0100
changeset 1393 4eaae533efc3
parent 1391 ebfbcadeac5e
child 1399 40e1646ff934
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory Term5
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
atom_decl name
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
datatype rtrm5 =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
  rVr5 "name"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
| rAp5 "rtrm5" "rtrm5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
and rlts =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
  rLnil
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
| rLcons "name" "rtrm5" "rlts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
primrec
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
  rbv5
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
where
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
  "rbv5 rLnil = {}"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
1277
6eacf60ce41d Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1270
diff changeset
    22
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    25
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    26
  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
notation
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
  alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
  alpha_rlts ("_ \<approx>l _" [100, 100] 100)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    32
thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    34
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
thm alpha5_inj
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
lemma rbv5_eqvt[eqvt]:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
  apply (induct x)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
  apply (simp_all add: eqvts atom_eqvt)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
lemma fv_rtrm5_rlts_eqvt[eqvt]:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
  "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
  "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
  apply (induct x and l)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
  apply (simp_all add: eqvts atom_eqvt)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
  done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
lemma alpha5_eqvt:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    53
  "alpha_rbv5 a b c \<Longrightarrow> True"
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    54
apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    55
apply (simp_all add: alpha5_inj)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    56
apply (erule exE)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    57
apply (rule_tac x="pi" in exI)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    58
apply clarify
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    59
apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric])
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    60
apply (subst eqvts[symmetric])
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    61
apply (subst eqvts[symmetric])
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    62
sorry
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    64
lemma alpha5_equivp:
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    65
  "equivp alpha_rtrm5"
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    66
  "equivp alpha_rlts"
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    67
  sorry
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
quotient_type
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
  trm5 = rtrm5 / alpha_rtrm5
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
  lts = rlts / alpha_rlts
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
  by (auto intro: alpha5_equivp)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
local_setup {*
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
(fn ctxt => ctxt
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    78
 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    79
 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    80
 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    81
 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    82
 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    83
 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    84
 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    85
 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
*}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
lemma alpha5_rfv:
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    90
  "(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)"
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    91
  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    92
  apply(simp_all)
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    93
  apply(simp add: alpha_gen)
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    94
  apply(erule conjE)+
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    95
  apply(erule exE)
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    96
  apply(erule conjE)+
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
    97
  apply(simp_all)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
    98
  sorry
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
lemma bv_list_rsp:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   102
  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
  apply(simp_all)
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   104
  apply(clarify)
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   105
  apply simp
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
  done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
lemma [quot_respect]:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
  "(alpha_rlts ===> op =) fv_rlts fv_rlts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   110
  "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
  "(alpha_rlts ===> op =) rbv5 rbv5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
  "(op = ===> alpha_rtrm5) rVr5 rVr5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
  "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   114
  "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   115
  "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
  "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
  "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   118
  "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   120
  apply (clarify)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   121
  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   122
  defer
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   123
  apply clarify
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   124
  apply (erule alpha_rlts.cases)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   125
  apply (erule alpha_rlts.cases)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   126
  apply (simp_all)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   127
  defer
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   128
  apply (erule alpha_rlts.cases)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   129
  apply (simp_all)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   130
  defer
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   131
  apply clarify
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   132
  apply (simp add: alpha5_inj)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   133
  sorry (* may be true? *)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
lemma
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   135
  shows "(alpha_rlts ===> op =) rbv5 rbv5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   136
  by (simp add: bv_list_rsp)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   137
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   138
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   139
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
instantiation trm5 and lts :: pt
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   141
begin
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   142
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   143
quotient_definition
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
  "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   145
is
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   146
  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   148
quotient_definition
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   149
  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
is
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   151
  "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   152
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   153
instance by default
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   154
  (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   155
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
end
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   157
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   158
lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   159
lemmas bv5[simp] = rbv5.simps[quot_lifted]
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   160
lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   161
lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   162
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   163
lemma lets_ok:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   164
  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   165
apply (simp add: alpha5_INJ)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   166
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   167
apply (simp_all add: alpha_gen)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   168
apply (simp add: permute_trm5_lts fresh_star_def)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   169
apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   170
done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   171
1286
87894b5156f4 Example that shows that current alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1277
diff changeset
   172
lemma lets_ok3:
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   173
  "x \<noteq> y \<Longrightarrow>
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   174
   (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   175
   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   176
apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
1286
87894b5156f4 Example that shows that current alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1277
diff changeset
   177
done
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   178
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   179
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   180
lemma lets_not_ok1:
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   181
  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   182
   (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
1288
0203cd5cfd6c The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1287
diff changeset
   183
apply (simp add: alpha5_INJ alpha_gen)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   184
apply (rule_tac x="0::perm" in exI)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   185
apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   186
apply auto
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   187
done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   188
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   189
lemma distinct_helper:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   190
  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   191
  apply auto
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
  apply (erule alpha_rtrm5.cases)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   193
  apply (simp_all only: rtrm5.distinct)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   194
  done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   195
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   196
lemma distinct_helper2:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
  shows "(Vr5 x) \<noteq> (Ap5 y z)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   198
  by (lifting distinct_helper)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   200
lemma lets_nok:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   201
  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   202
   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   203
   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
1391
ebfbcadeac5e Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1288
diff changeset
   205
apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
1270
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   206
done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   207
8c3cf9f4f5f2 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   208
end