1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory Term1
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
begin
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 5
atom_decl name
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 6
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 7
section {*** lets with binding patterns ***}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 8
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 9
datatype rtrm1 =
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 10
rVr1 "name"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 11
| rAp1 "rtrm1" "rtrm1"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 12
| rLm1 "name" "rtrm1" --"name is bound in trm1"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 13
| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 14
and bp =
1488
+ − 15
BUnit
+ − 16
| BVr "name"
+ − 17
| BPr "bp" "bp"
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 18
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 19
print_theorems
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 21
(* to be given by the user *)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 22
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23
primrec
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 24
bv1
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 25
where
1488
+ − 26
"bv1 (BUnit) = {}"
+ − 27
| "bv1 (BVr x) = {atom x}"
+ − 28
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29
1277
+ − 30
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 31
thm permute_rtrm1_permute_bp.simps
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 32
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 33
local_setup {*
1277
+ − 34
snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
1400
+ − 35
[[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
1488
+ − 36
[[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 37
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 38
notation
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 39
alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 40
alpha_bp ("_ \<approx>1b _" [100, 100] 100)
1400
+ − 41
thm alpha_rtrm1_alpha_bp_alpha_bv1.intros
1435
55b49de0c2c7
Even with pattern simplified to a single clause, the supp equation doesn't seem true.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 42
(*thm fv_rtrm1_fv_bp.simps[no_vars]*)
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 43
1400
+ − 44
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *}
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45
thm alpha1_inj
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 46
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 47
local_setup {*
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 48
snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms bv1.simps permute_rtrm1_permute_bp.simps} @{context}))
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 49
*}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 50
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 51
local_setup {*
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 52
snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 53
*}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 54
1488
+ − 55
(*local_setup {*
1446
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context})
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57
*}
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
print_theorems
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
local_setup {*
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
*}
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 63
print_theorems
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 64
*)
a93f8df272de
build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 65
1300
+ − 66
local_setup {*
+ − 67
(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
1488
+ − 68
build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms permute_rtrm1_permute_bp.simps alpha1_inj} ctxt 1) ctxt) ctxt)) *}
1291
+ − 69
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
lemma alpha1_eqvt_proper[eqvt]:
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
"pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 72
"pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
apply (simp_all only: eqvts)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
apply rule
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 75
apply (simp_all add: alpha1_eqvt)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
apply (simp_all only: alpha1_eqvt)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 79
apply rule
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 80
apply (simp_all add: alpha1_eqvt)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 81
apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 83
apply (simp_all only: alpha1_eqvt)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 84
done
1274
+ − 85
thm eqvts_raw(1)
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 86
1488
+ − 87
lemma "(b \<approx>1 a \<longrightarrow> a \<approx>1 b) \<and> (x \<approx>1b y \<longrightarrow> y \<approx>1b x) \<and> (alpha_bv1 x y \<longrightarrow> alpha_bv1 y x)"
+ − 88
apply (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} @{context} 1 *})
+ − 89
done
+ − 90
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 91
lemma alpha1_equivp:
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 92
"equivp alpha_rtrm1"
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 93
"equivp alpha_bp"
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 94
sorry
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 95
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 96
(*
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 97
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
1488
+ − 98
(build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}, @{term alpha_bv1}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.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)) *}
+ − 99
thm alpha1_equivp*)
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 100
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 101
local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 102
(rtac @{thm alpha1_equivp(1)} 1) *}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 103
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 104
local_setup {*
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 105
(fn ctxt => ctxt
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 106
|> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 107
|> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 108
|> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 109
|> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 110
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 111
*}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 112
print_theorems
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 113
1278
+ − 114
local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 115
(fn _ => Skip_Proof.cheat_tac @{theory}) *}
1278
+ − 116
local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
+ − 117
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+ − 118
local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 119
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
1278
+ − 120
local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 121
(fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
1278
+ − 122
local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 123
(fn _ => Skip_Proof.cheat_tac @{theory}) *}
1278
+ − 124
local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 125
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 126
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 127
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 128
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 129
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 130
setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 131
@{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 132
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 133
lemmas
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 134
permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 135
and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
1488
+ − 136
and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt[quot_lifted]
+ − 137
and alpha1_INJ = alpha1_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 138
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 139
lemma supports:
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 140
"(supp (atom x)) supports (Vr1 x)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 141
"(supp t \<union> supp s) supports (Ap1 t s)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 142
"(supp (atom x) \<union> supp t) supports (Lm1 x t)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 143
"(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
1488
+ − 144
"{} supports BUnit"
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 145
"(supp (atom x)) supports (BVr x)"
1488
+ − 146
"(supp a \<union> supp b) supports (BPr a b)"
1428
+ − 147
apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 148
done
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 149
1429
+ − 150
prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *}
+ − 151
apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *})
+ − 152
done
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 153
1343
693df83172f0
Trying to fix the proofs for the single existential... So far failed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 154
instance trm1 and bp :: fs
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 155
apply default
1434
+ − 156
apply (simp_all add: rtrm1_bp_fs)
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 157
done
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 158
1345
+ − 159
lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp"
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 160
apply(induct bp rule: trm1_bp_inducts(2))
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 161
apply(simp_all)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 162
done
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 163
1345
+ − 164
lemma fv_eq_bv: "fv_bp = bv1"
+ − 165
apply(rule ext)
+ − 166
apply(rule fv_eq_bv_pre)
+ − 167
done
+ − 168
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 169
lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 170
apply auto
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 171
apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 172
apply auto
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 173
done
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 174
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 175
lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 176
apply rule
1425
112f998d2953
Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 177
apply (induct a b rule: alpha_rtrm1_alpha_bp_alpha_bv1.inducts(2))
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 178
apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 179
done
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 180
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 181
lemma alpha_bp_eq: "alpha_bp = (op =)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 182
apply (rule ext)+
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 183
apply (rule alpha_bp_eq_eq)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 184
done
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 185
1345
+ − 186
lemma ex_out:
+ − 187
"(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
+ − 188
"(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
+ − 189
"(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+ − 190
"(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+ − 191
"(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))"
+ − 192
apply (blast)+
+ − 193
done
+ − 194
+ − 195
lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
+ − 196
by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
+ − 197
1349
+ − 198
lemma supp_fv_let:
+ − 199
assumes sa : "fv_bp bp = supp bp"
1488
+ − 200
shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk>
+ − 201
\<Longrightarrow> supp (Lt1 bp ta tb) = supp ta \<union> (supp (bp, tb) - supp bp)"
1349
+ − 202
apply(fold supp_Abs)
1488
+ − 203
apply(simp (no_asm) only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
1434
+ − 204
apply(simp (no_asm) only: supp_def)
+ − 205
apply(simp only: permute_set_eq permute_trm1)
1488
+ − 206
apply(simp only: alpha1_INJ alpha_bp_eq)
1434
+ − 207
apply(simp only: ex_out)
+ − 208
apply(simp only: Collect_neg_conj)
+ − 209
apply(simp only: permute_ABS)
+ − 210
apply(simp only: Abs_eq_iff)
1488
+ − 211
apply(simp only: alpha_gen supp_Pair split_conv eqvts)
1544
+ − 212
apply(simp only: infinite_Un)
1434
+ − 213
apply(simp only: Collect_disj_eq)
+ − 214
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
1488
+ − 215
apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])
+ − 216
apply (simp only: eqvts Pair_eq)
+ − 217
done
1436
+ − 218
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 219
lemma supp_fv:
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 220
"supp t = fv_trm1 t"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 221
"supp b = fv_bp b"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 222
apply(induct t and b rule: trm1_bp_inducts)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 223
apply(simp_all)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 224
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 225
apply(simp only: supp_at_base[simplified supp_def])
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 226
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
1343
693df83172f0
Trying to fix the proofs for the single existential... So far failed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 227
apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute)
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 228
apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 229
apply(simp add: supp_Abs fv_trm1)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 230
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 231
apply(simp add: alpha1_INJ)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
apply(simp add: Abs_eq_iff)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 233
apply(simp add: alpha_gen.simps)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 234
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
1488
+ − 235
apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair)
+ − 236
apply blast
+ − 237
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
+ − 238
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
1436
+ − 239
apply(simp only: supp_at_base[simplified supp_def])
1488
+ − 240
apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq])
+ − 241
apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
1345
+ − 242
apply(fold supp_def)
1488
+ − 243
apply simp
+ − 244
done
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 245
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 246
lemma trm1_supp:
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 247
"supp (Vr1 x) = {atom x}"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 248
"supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 249
"supp (Lm1 x t) = (supp t) - {atom x}"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 250
"supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 251
by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 252
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 253
lemma trm1_induct_strong:
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 254
assumes "\<And>name b. P b (Vr1 name)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 255
and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 256
and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 257
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)"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 258
shows "P a rtrma"
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 259
sorry
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 260
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 261
end