1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory Terms
1227
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
begin
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 5
atom_decl name
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 6
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 7
text {* primrec seems to be genarally faster than fun *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 8
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 9
section {*** lets with binding patterns ***}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 10
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 11
datatype rtrm1 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 12
rVr1 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 13
| rAp1 "rtrm1" "rtrm1"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 14
| rLm1 "name" "rtrm1" --"name is bound in trm1"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 15
| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 16
and bp =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 17
BUnit
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 18
| BVr "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 19
| BPr "bp" "bp"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
1198
+ − 21
print_theorems
+ − 22
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23
(* to be given by the user *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 24
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 25
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 26
bv1
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 27
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 28
"bv1 (BUnit) = {}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29
| "bv1 (BVr x) = {atom x}"
1183
+ − 30
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 31
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 32
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
1201
+ − 33
thm permute_rtrm1_permute_bp.simps
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 34
1225
+ − 35
local_setup {*
1199
+ − 36
snd o define_fv_alpha "Terms.rtrm1"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 37
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
1199
+ − 38
[[], [[]], [[], []]]] *}
1198
+ − 39
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 40
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 41
alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 42
alpha_bp ("_ \<approx>1b _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 43
thm alpha_rtrm1_alpha_bp.intros
1202
+ − 44
thm fv_rtrm1_fv_bp.simps
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45
1199
+ − 46
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)) *}
+ − 47
thm alpha1_inj
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 48
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 49
lemma alpha_bp_refl: "alpha_bp a a"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 50
apply induct
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 51
apply (simp_all add: alpha1_inj)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 52
done
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 53
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54
lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 55
apply rule
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57
apply (simp_all add: alpha_bp_refl)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
done
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
lemma alpha_bp_eq: "alpha_bp = (op =)"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
apply (rule ext)+
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
apply (rule alpha_bp_eq_eq)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 63
done
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 64
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 65
lemma bv1_eqvt[eqvt]:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 66
shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 67
apply (induct x)
1255
+ − 68
apply (simp_all add: eqvts atom_eqvt)
1201
+ − 69
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
lemma fv_rtrm1_eqvt[eqvt]:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 72
"(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
"(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
apply (induct t and b)
1255
+ − 75
apply (simp_all add: eqvts atom_eqvt)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
lemma alpha1_eqvt:
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 79
"t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 80
"alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 81
apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
apply (simp_all add:eqvts alpha1_inj)
1255
+ − 83
apply (tactic {*
+ − 84
ALLGOALS (
+ − 85
TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+ − 86
(etac @{thm alpha_gen_compose_eqvt})
+ − 87
) *})
+ − 88
apply (simp_all only: eqvts atom_eqvt)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 89
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 90
1215
+ − 91
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
+ − 92
(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)) *}
+ − 93
thm alpha1_equivp
1211
+ − 94
1227
+ − 95
local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
+ − 96
(rtac @{thm alpha1_equivp(1)} 1) *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 97
1190
+ − 98
local_setup {*
+ − 99
(fn ctxt => ctxt
+ − 100
|> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
+ − 101
|> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
+ − 102
|> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
+ − 103
|> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
+ − 104
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
+ − 105
*}
+ − 106
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 107
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 108
thm alpha_rtrm1_alpha_bp.induct
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 109
local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 110
(fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 111
local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
1227
+ − 112
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 113
local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 114
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 115
local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
1227
+ − 116
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 117
local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
1227
+ − 118
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 119
local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
1227
+ − 120
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 121
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 122
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 123
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 124
1253
+ − 125
setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
+ − 126
@{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 127
1227
+ − 128
lemmas
1250
+ − 129
permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
+ − 130
and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
1227
+ − 131
and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
+ − 132
and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 133
1246
+ − 134
lemma supports:
+ − 135
"(supp (atom x)) supports (Vr1 x)"
+ − 136
"(supp t \<union> supp s) supports (Ap1 t s)"
+ − 137
"(supp (atom x) \<union> supp t) supports (Lm1 x t)"
+ − 138
"(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
+ − 139
"{} supports BUnit"
+ − 140
"(supp (atom x)) supports (BVr x)"
+ − 141
"(supp a \<union> supp b) supports (BPr a b)"
1250
+ − 142
apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
1246
+ − 143
apply(rule_tac [!] allI)+
+ − 144
apply(rule_tac [!] impI)
+ − 145
apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 146
apply(simp_all add: fresh_atom)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 147
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 148
1246
+ − 149
lemma rtrm1_bp_fs:
+ − 150
"finite (supp (x :: trm1))"
+ − 151
"finite (supp (b :: bp))"
+ − 152
apply (induct x and b rule: trm1_bp_inducts)
+ − 153
apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
+ − 154
apply(simp_all add: supp_atom)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 155
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 156
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 157
instance trm1 :: fs
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 158
apply default
1246
+ − 159
apply (rule rtrm1_bp_fs(1))
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 160
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 161
1183
+ − 162
lemma fv_eq_bv: "fv_bp bp = bv1 bp"
+ − 163
apply(induct bp rule: trm1_bp_inducts(2))
+ − 164
apply(simp_all)
+ − 165
done
+ − 166
1209
+ − 167
lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 168
apply auto
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 169
apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 170
apply auto
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 171
done
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 172
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 173
lemma supp_fv:
1202
+ − 174
"supp t = fv_trm1 t"
+ − 175
"supp b = fv_bp b"
+ − 176
apply(induct t and b rule: trm1_bp_inducts)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 177
apply(simp_all)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 178
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 179
apply(simp only: supp_at_base[simplified supp_def])
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 180
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 181
apply(simp add: Collect_imp_eq Collect_neg_eq)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 182
apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 183
apply(simp add: supp_Abs fv_trm1)
1250
+ − 184
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 185
apply(simp add: alpha1_INJ)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 186
apply(simp add: Abs_eq_iff)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 187
apply(simp add: alpha_gen.simps)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 188
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
1183
+ − 189
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
+ − 190
apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
1250
+ − 191
apply(simp (no_asm) add: supp_def permute_trm1)
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
apply(simp add: alpha1_INJ alpha_bp_eq)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 193
apply(simp add: Abs_eq_iff)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 194
apply(simp add: alpha_gen)
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 195
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
1209
+ − 196
apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
1202
+ − 197
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+ − 198
apply(simp (no_asm) add: supp_def eqvts)
+ − 199
apply(fold supp_def)
+ − 200
apply(simp add: supp_at_base)
+ − 201
apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
+ − 202
apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
1183
+ − 203
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 204
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 205
lemma trm1_supp:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 206
"supp (Vr1 x) = {atom x}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 207
"supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 208
"supp (Lm1 x t) = (supp t) - {atom x}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 209
"supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
1183
+ − 210
by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 211
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 212
lemma trm1_induct_strong:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 213
assumes "\<And>name b. P b (Vr1 name)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 214
and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 215
and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 216
and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 217
shows "P a rtrma"
1183
+ − 218
sorry
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 219
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 220
section {*** lets with single assignments ***}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 221
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 222
datatype rtrm2 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 223
rVr2 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 224
| rAp2 "rtrm2" "rtrm2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 225
| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 226
| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 227
and rassign =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 228
rAs "name" "rtrm2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 229
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 230
(* to be given by the user *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 231
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
rbv2
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 233
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 234
"rbv2 (rAs x t) = {atom x}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 235
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 236
setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 237
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 238
local_setup {* snd o define_fv_alpha "Terms.rtrm2"
1202
+ − 239
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 240
[[[], []]]] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 241
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 242
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 243
alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 244
alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245
thm alpha_rtrm2_alpha_rassign.intros
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 246
1199
+ − 247
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)) *}
+ − 248
thm alpha2_inj
+ − 249
1215
+ − 250
lemma alpha2_eqvt:
+ − 251
"t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"
+ − 252
"a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"
+ − 253
sorry
1199
+ − 254
1215
+ − 255
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),
+ − 256
(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)) *}
+ − 257
thm alpha2_equivp
+ − 258
1227
+ − 259
local_setup {* define_quotient_type
+ − 260
[(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),
+ − 261
(([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]
+ − 262
((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 263
1190
+ − 264
local_setup {*
+ − 265
(fn ctxt => ctxt
+ − 266
|> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))
+ − 267
|> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))
+ − 268
|> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))
+ − 269
|> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))
+ − 270
|> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))
+ − 271
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))
+ − 272
|> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))
+ − 273
*}
+ − 274
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 275
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 276
local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 277
(fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 278
local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 279
(fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 280
local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]
1227
+ − 281
(fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 282
local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]
1227
+ − 283
(fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 284
local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]
1227
+ − 285
(fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
1230
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 286
local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 287
(fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}
a41c3a105104
rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]
1227
+ − 289
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}
+ − 290
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 291
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 292
section {*** lets with many assignments ***}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 293
1206
+ − 294
datatype rtrm3 =
+ − 295
rVr3 "name"
+ − 296
| rAp3 "rtrm3" "rtrm3"
+ − 297
| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
+ − 298
| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
+ − 299
and rassigns =
+ − 300
rANil
+ − 301
| rACons "name" "rtrm3" "rassigns"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 302
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 303
(* to be given by the user *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 304
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 305
bv3
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 306
where
1206
+ − 307
"bv3 rANil = {}"
+ − 308
| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 309
1206
+ − 310
setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 311
1206
+ − 312
local_setup {* snd o define_fv_alpha "Terms.rtrm3"
1202
+ − 313
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 314
[[], [[], [], []]]] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 315
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 316
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 317
notation
1206
+ − 318
alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
+ − 319
alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
+ − 320
thm alpha_rtrm3_alpha_rassigns.intros
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 321
1215
+ − 322
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)) *}
+ − 323
thm alpha3_inj
+ − 324
+ − 325
lemma alpha3_eqvt:
+ − 326
"t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
+ − 327
"a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
+ − 328
sorry
+ − 329
+ − 330
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
+ − 331
(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)) *}
+ − 332
thm alpha3_equivp
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 333
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 334
quotient_type
1206
+ − 335
trm3 = rtrm3 / alpha_rtrm3
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 336
and
1206
+ − 337
assigns = rassigns / alpha_rassigns
1215
+ − 338
by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 339
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 340
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 341
section {*** lam with indirect list recursion ***}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 342
1206
+ − 343
datatype rtrm4 =
+ − 344
rVr4 "name"
+ − 345
| rAp4 "rtrm4" "rtrm4 list"
+ − 346
| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
1215
+ − 347
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 348
1206
+ − 349
thm rtrm4.recs
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 350
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 351
(* there cannot be a clause for lists, as *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 352
(* permutations are already defined in Nominal (also functions, options, and so on) *)
1206
+ − 353
setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 354
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 355
(* "repairing" of the permute function *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 356
lemma repaired:
1206
+ − 357
fixes ts::"rtrm4 list"
+ − 358
shows "permute_rtrm4_list p ts = p \<bullet> ts"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 359
apply(induct ts)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 360
apply(simp_all)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 361
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 362
1206
+ − 363
thm permute_rtrm4_permute_rtrm4_list.simps
+ − 364
thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 365
1206
+ − 366
local_setup {* snd o define_fv_alpha "Terms.rtrm4" [
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 367
[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 368
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 369
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 370
notation
1206
+ − 371
alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
+ − 372
alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
+ − 373
thm alpha_rtrm4_alpha_rtrm4_list.intros
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 374
1216
+ − 375
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 list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+ − 376
thm alpha4_inj
1215
+ − 377
+ − 378
lemma alpha4_eqvt:
+ − 379
"t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"
+ − 380
"a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"
+ − 381
sorry
+ − 382
1216
+ − 383
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
1217
+ − 384
(build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+ − 385
thm alpha4_equivp
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 386
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 387
quotient_type
1206
+ − 388
qrtrm4 = rtrm4 / alpha_rtrm4 and
+ − 389
qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
1217
+ − 390
by (simp_all add: alpha4_equivp)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 391
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 392
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 393
datatype rtrm5 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 394
rVr5 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 395
| rAp5 "rtrm5" "rtrm5"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 396
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 397
and rlts =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 398
rLnil
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 399
| rLcons "name" "rtrm5" "rlts"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 400
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 401
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 402
rbv5
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 403
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 404
"rbv5 rLnil = {}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 405
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 406
1186
166cc41091b9
The alternate version of trm5 with additional binding. All proofs work the same.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 407
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 408
setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 409
print_theorems
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 410
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 411
local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 412
[[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 413
print_theorems
1187
+ − 414
1186
166cc41091b9
The alternate version of trm5 with additional binding. All proofs work the same.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 415
(* Alternate version with additional binding of name in rlts in rLcons *)
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 416
(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
1186
166cc41091b9
The alternate version of trm5 with additional binding. All proofs work the same.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 417
[[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *}
1187
+ − 418
print_theorems*)
1186
166cc41091b9
The alternate version of trm5 with additional binding. All proofs work the same.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 419
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 420
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 421
alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 422
alpha_rlts ("_ \<approx>l _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 423
thm alpha_rtrm5_alpha_rlts.intros
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 424
1199
+ − 425
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)) *}
+ − 426
thm alpha5_inj
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 427
1255
+ − 428
lemma rbv5_eqvt[eqvt]:
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 429
"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
1255
+ − 430
apply (induct x)
+ − 431
apply (simp_all add: eqvts atom_eqvt)
+ − 432
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 433
1255
+ − 434
lemma fv_rtrm5_rlts_eqvt[eqvt]:
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 435
"pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
1255
+ − 436
"pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+ − 437
apply (induct x and l)
+ − 438
apply (simp_all add: eqvts atom_eqvt)
+ − 439
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 440
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 441
lemma alpha5_eqvt:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 442
"xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 443
"xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
1255
+ − 444
apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 445
apply (simp_all add: alpha5_inj)
1255
+ − 446
apply (tactic {*
+ − 447
ALLGOALS (
+ − 448
TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+ − 449
(etac @{thm alpha_gen_compose_eqvt})
+ − 450
) *})
+ − 451
apply (simp_all only: eqvts atom_eqvt)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 452
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 453
1215
+ − 454
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
+ − 455
(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)) *}
+ − 456
thm alpha5_equivp
1213
+ − 457
+ − 458
quotient_type
+ − 459
trm5 = rtrm5 / alpha_rtrm5
+ − 460
and
+ − 461
lts = rlts / alpha_rlts
1215
+ − 462
by (auto intro: alpha5_equivp)
1213
+ − 463
+ − 464
local_setup {*
+ − 465
(fn ctxt => ctxt
+ − 466
|> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ − 467
|> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ − 468
|> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
+ − 469
|> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
+ − 470
|> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
+ − 471
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
+ − 472
|> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ − 473
|> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
+ − 474
*}
+ − 475
print_theorems
+ − 476
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 477
lemma alpha5_rfv:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 478
"(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 479
"(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 480
apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 481
apply(simp_all add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 482
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 483
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 484
lemma bv_list_rsp:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 485
shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 486
apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 487
apply(simp_all)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 488
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 489
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 490
lemma [quot_respect]:
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 491
"(alpha_rlts ===> op =) fv_rlts fv_rlts"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 492
"(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 493
"(alpha_rlts ===> op =) rbv5 rbv5"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 494
"(op = ===> alpha_rtrm5) rVr5 rVr5"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 495
"(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 496
"(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 497
"(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 498
"(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 499
"(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 500
apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 501
apply (clarify) apply (rule conjI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 502
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 503
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 504
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 505
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 506
lemma
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 507
shows "(alpha_rlts ===> op =) rbv5 rbv5"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 508
by (simp add: bv_list_rsp)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 509
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 510
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 511
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 512
instantiation trm5 and lts :: pt
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 513
begin
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 514
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 515
quotient_definition
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 516
"permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 517
is
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 518
"permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 519
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 520
quotient_definition
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 521
"permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 522
is
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 523
"permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 524
1250
+ − 525
instance by default
+ − 526
(simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 527
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 528
end
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 529
1250
+ − 530
lemmas
+ − 531
permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+ − 532
and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+ − 533
and bv5[simp] = rbv5.simps[quot_lifted]
+ − 534
and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 535
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 536
lemma lets_ok:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 537
"(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 538
apply (subst alpha5_INJ)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 539
apply (rule conjI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 540
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 541
apply (simp only: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 542
apply (simp add: permute_trm5_lts fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 543
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 544
apply (simp only: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 545
apply (simp add: permute_trm5_lts fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 546
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 547
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 548
lemma lets_ok2:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 549
"(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 550
(Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 551
apply (subst alpha5_INJ)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 552
apply (rule conjI)
1199
+ − 553
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 554
apply (simp only: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 555
apply (simp add: permute_trm5_lts fresh_star_def)
1199
+ − 556
apply (rule_tac x="0 :: perm" in exI)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 557
apply (simp only: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 558
apply (simp add: permute_trm5_lts fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 559
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 560
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 561
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 562
lemma lets_not_ok1:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 563
"x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 564
(Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
1200
+ − 565
apply (simp add: alpha5_INJ(3) alpha_gen)
+ − 566
apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 567
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 568
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 569
lemma distinct_helper:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 570
shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 571
apply auto
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 572
apply (erule alpha_rtrm5.cases)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 573
apply (simp_all only: rtrm5.distinct)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 574
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 575
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 576
lemma distinct_helper2:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 577
shows "(Vr5 x) \<noteq> (Ap5 y z)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 578
by (lifting distinct_helper)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 579
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 580
lemma lets_nok:
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 581
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 582
(Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 583
(Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
1200
+ − 584
apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 585
apply (simp add: distinct_helper2)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 586
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 587
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 588
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 589
(* example with a bn function defined over the type itself *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 590
datatype rtrm6 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 591
rVr6 "name"
1205
+ − 592
| rLm6 "name" "rtrm6" --"bind name in rtrm6"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 593
| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 594
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 595
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 596
rbv6
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 597
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 598
"rbv6 (rVr6 n) = {}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 599
| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 600
| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 601
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 602
setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 603
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 604
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 605
local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
1202
+ − 606
[[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
1201
+ − 607
notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 608
(* HERE THE RULES DIFFER *)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 609
thm alpha_rtrm6.intros
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 610
1201
+ − 611
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)) *}
+ − 612
thm alpha6_inj
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 613
1215
+ − 614
lemma alpha6_eqvt:
+ − 615
"xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 616
sorry
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 617
1215
+ − 618
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
+ − 619
(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)) *}
+ − 620
thm alpha6_equivp
+ − 621
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 622
quotient_type
1201
+ − 623
trm6 = rtrm6 / alpha_rtrm6
1215
+ − 624
by (auto intro: alpha6_equivp)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 625
1190
+ − 626
local_setup {*
+ − 627
(fn ctxt => ctxt
+ − 628
|> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
+ − 629
|> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))
+ − 630
|> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))
+ − 631
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))
+ − 632
|> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
+ − 633
*}
+ − 634
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 635
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 636
lemma [quot_respect]:
1201
+ − 637
"(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
1215
+ − 638
by (auto simp add: alpha6_eqvt)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 639
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 640
(* Definitely not true , see lemma below *)
1201
+ − 641
lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 642
apply simp apply clarify
1201
+ − 643
apply (erule alpha_rtrm6.induct)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 644
oops
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 645
1201
+ − 646
lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 647
apply simp
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 648
apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 649
apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 650
apply simp
1201
+ − 651
apply (simp add: alpha6_inj)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 652
apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 653
apply (simp add: alpha_gen fresh_star_def)
1201
+ − 654
apply (simp add: alpha6_inj)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 655
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 656
1201
+ − 657
lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y"
+ − 658
apply (induct_tac x y rule: alpha_rtrm6.induct)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 659
apply simp_all
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 660
apply (erule exE)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 661
apply (simp_all add: alpha_gen)
1201
+ − 662
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 663
1201
+ − 664
lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6"
+ − 665
by (simp add: fv6_rsp)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 666
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 667
lemma [quot_respect]:
1201
+ − 668
"(op = ===> alpha_rtrm6) rVr6 rVr6"
+ − 669
"(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6"
+ − 670
apply auto
+ − 671
apply (simp_all add: alpha6_inj)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 672
apply (rule_tac x="0::perm" in exI)
1201
+ − 673
apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)
+ − 674
done
+ − 675
+ − 676
lemma [quot_respect]:
+ − 677
"(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"
+ − 678
apply auto
+ − 679
apply (simp_all add: alpha6_inj)
+ − 680
apply (rule_tac [!] x="0::perm" in exI)
+ − 681
apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 682
(* needs rbv6_rsp *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 683
oops
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 684
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 685
instantiation trm6 :: pt begin
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 686
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 687
quotient_definition
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 688
"permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 689
is
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 690
"permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 691
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 692
instance
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 693
apply default
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 694
sorry
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 695
end
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 696
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 697
lemma lifted_induct:
1201
+ − 698
"\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);
+ − 699
\<And>name rtrm6 namea rtrm6a.
+ − 700
\<lbrakk>True;
+ − 701
\<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>
+ − 702
(fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
+ − 703
\<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
+ − 704
\<And>rtrm61 rtrm61a rtrm62 rtrm62a.
1202
+ − 705
\<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;
1201
+ − 706
\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
+ − 707
(fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
+ − 708
\<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>
+ − 709
\<Longrightarrow> P x1 x2"
+ − 710
apply (lifting alpha_rtrm6.induct[unfolded alpha_gen])
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 711
apply injection
1201
+ − 712
(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 713
oops
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 714
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 715
lemma lifted_inject_a3:
1201
+ − 716
"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =
1202
+ − 717
(rtrm61 = rtrm61a \<and>
1201
+ − 718
(\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
+ − 719
(fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"
+ − 720
apply(lifting alpha6_inj(3)[unfolded alpha_gen])
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 721
apply injection
1201
+ − 722
(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 723
oops
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 724
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 725
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 726
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 727
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 728
(* example with a respectful bn function defined over the type itself *)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 729
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 730
datatype rtrm7 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 731
rVr7 "name"
1198
+ − 732
| rLm7 "name" "rtrm7" --"bind left in right"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 733
| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 734
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 735
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 736
rbv7
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 737
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 738
"rbv7 (rVr7 n) = {atom n}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 739
| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 740
| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 741
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 742
setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
1201
+ − 743
thm permute_rtrm7.simps
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 744
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 745
local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
1202
+ − 746
[[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
1198
+ − 747
print_theorems
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 748
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 749
alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 750
(* HERE THE RULES DIFFER *)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 751
thm alpha_rtrm7.intros
1198
+ − 752
thm fv_rtrm7.simps
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 753
inductive
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 754
alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 755
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 756
a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 757
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 758
| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 759
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 760
lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 761
apply simp
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 762
apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 763
apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 764
apply simp
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 765
apply (rule a3)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 766
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 767
apply (simp_all add: alpha_gen fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 768
apply (rule a1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 769
apply (rule refl)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 770
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 771
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 772
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 773
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 774
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 775
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 776
datatype rfoo8 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 777
Foo0 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 778
| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 779
and rbar8 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 780
Bar0 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 781
| Bar1 "name" "name" "rbar8" --"bind second name in b"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 782
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 783
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 784
rbv8
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 785
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 786
"rbv8 (Bar0 x) = {}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 787
| "rbv8 (Bar1 v x b) = {atom v}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 788
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 789
setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 790
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 791
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 792
local_setup {* snd o define_fv_alpha "Terms.rfoo8" [
1202
+ − 793
[[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 794
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 795
alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 796
alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 797
(* HERE THE RULE DIFFERS *)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 798
thm alpha_rfoo8_alpha_rbar8.intros
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 799
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 800
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 801
inductive
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 802
alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 803
and
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 804
alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 805
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 806
a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 807
| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 808
| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 809
| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 810
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 811
lemma "(alpha8b ===> op =) rbv8 rbv8"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 812
apply simp apply clarify
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 813
apply (erule alpha8f_alpha8b.inducts(2))
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 814
apply (simp_all)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 815
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 816
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 817
lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 818
apply (erule alpha8f_alpha8b.inducts(2))
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 819
apply (simp_all add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 820
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 821
lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 822
apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 823
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 824
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 825
lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 826
apply simp apply clarify
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 827
apply (erule alpha8f_alpha8b.inducts(1))
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 828
apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
1183
+ − 829
done
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 830
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 831
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 832
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 833
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 834
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 835
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 836
datatype rlam9 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 837
Var9 "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 838
| Lam9 "name" "rlam9" --"bind name in rlam"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 839
and rbla9 =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 840
Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 841
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 842
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 843
rbv9
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 844
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 845
"rbv9 (Var9 x) = {}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 846
| "rbv9 (Lam9 x b) = {atom x}"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 847
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 848
setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 849
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 850
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 851
local_setup {* snd o define_fv_alpha "Terms.rlam9" [
1202
+ − 852
[[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 853
notation
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 854
alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 855
alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 856
(* HERE THE RULES DIFFER *)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 857
thm alpha_rlam9_alpha_rbla9.intros
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 858
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 859
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 860
inductive
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 861
alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 862
and
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 863
alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 864
where
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 865
a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 866
| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 867
| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 868
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 869
quotient_type
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 870
lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 871
sorry
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 872
1190
+ − 873
local_setup {*
+ − 874
(fn ctxt => ctxt
+ − 875
|> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
+ − 876
|> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
+ − 877
|> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
+ − 878
|> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
+ − 879
|> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
+ − 880
|> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
+ − 881
*}
+ − 882
print_theorems
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 883
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 884
instantiation lam9 and bla9 :: pt
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 885
begin
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 886
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 887
quotient_definition
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 888
"permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 889
is
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 890
"permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 891
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 892
quotient_definition
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 893
"permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 894
is
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 895
"permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 896
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 897
instance
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 898
sorry
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 899
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 900
end
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 901
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 902
lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 903
\<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 904
apply (lifting a3[unfolded alpha_gen])
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 905
apply injection
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 906
sorry
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 907
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 908
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 909
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 910
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 911
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 912
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 913
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 914
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 915
text {* type schemes *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 916
datatype ty =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 917
Var "name"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 918
| Fun "ty" "ty"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 919
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 920
setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 921
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 922
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 923
datatype tyS =
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 924
All "name set" "ty"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 925
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 926
setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 927
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 928
1199
+ − 929
local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *}
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 930
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 931
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 932
(*
1185
+ − 933
Doesnot work yet since we do not refer to fv_ty
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 934
local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 935
print_theorems
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 936
*)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 937
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 938
primrec
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 939
fv_tyS
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 940
where
1185
+ − 941
"fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 942
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 943
inductive
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 944
alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 945
where
1185
+ − 946
a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2))
1182
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 947
\<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 948
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 949
lemma
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 950
shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 951
apply(rule a1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 952
apply(simp add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 953
apply(rule_tac x="0::perm" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 954
apply(simp add: fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 955
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 956
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 957
lemma
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 958
shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 959
apply(rule a1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 960
apply(simp add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 961
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 962
apply(simp add: fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 963
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 964
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 965
lemma
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 966
shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 967
apply(rule a1)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 968
apply(simp add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 969
apply(rule_tac x="0::perm" in exI)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 970
apply(simp add: fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 971
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 972
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 973
lemma
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 974
assumes a: "a \<noteq> b"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 975
shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 976
using a
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 977
apply(clarify)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 978
apply(erule alpha_tyS.cases)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 979
apply(simp add: alpha_gen)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 980
apply(erule conjE)+
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 981
apply(erule exE)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 982
apply(erule conjE)+
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 983
apply(clarify)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 984
apply(simp)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 985
apply(simp add: fresh_star_def)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 986
apply(auto)
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 987
done
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 988
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 989
3c32f91fa771
Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 990
end