297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory LFex
600
+ − 2
imports Nominal "../QuotList"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3
begin
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
492
+ − 5
atom_decl name ident
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 6
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 7
nominal_datatype kind =
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
Type
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 9
| KPi "ty" "name" "kind"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 10
and ty =
492
+ − 11
TConst "ident"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 12
| TApp "ty" "trm"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 13
| TPi "ty" "name" "ty"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 14
and trm =
492
+ − 15
Const "ident"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 16
| Var "name"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 17
| App "trm" "trm"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 18
| Lam "ty" "name" "trm"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 19
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 20
function
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21
fv_kind :: "kind \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 22
and fv_ty :: "ty \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 23
and fv_trm :: "trm \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 24
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 25
"fv_kind (Type) = {}"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 26
| "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 27
| "fv_ty (TConst i) = {}"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 28
| "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 29
| "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 30
| "fv_trm (Const i) = {}"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 31
| "fv_trm (Var x) = {x}"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 32
| "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 33
| "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 34
sorry
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 35
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 36
termination fv_kind sorry
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 37
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 38
inductive
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 39
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 40
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 41
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 42
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 43
a1: "(Type) \<approx>ki (Type)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 44
| a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 45
| a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk>
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 46
\<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 47
| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 48
| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 49
| a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 50
| a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk>
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 51
\<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 52
| a6: "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 53
| a7: "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 54
| a8: "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 55
| a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 56
| a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk>
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 57
\<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 58
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 59
lemma al_refl:
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 60
fixes K::"kind"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 61
and A::"ty"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 62
and M::"trm"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 63
shows "K \<approx>ki K"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 64
and "A \<approx>ty A"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 65
and "M \<approx>tr M"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 66
apply(induct K and A and M rule: kind_ty_trm.inducts)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 67
apply(auto intro: akind_aty_atrm.intros)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 68
done
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 69
534
+ − 70
lemma alpha_equivps:
+ − 71
shows "equivp akind"
+ − 72
and "equivp aty"
+ − 73
and "equivp atrm"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 74
sorry
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 75
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 76
quotient KIND = kind / akind
534
+ − 77
by (rule alpha_equivps)
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 78
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 79
quotient TY = ty / aty
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 80
and TRM = trm / atrm
534
+ − 81
by (auto intro: alpha_equivps)
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 82
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 83
print_quotients
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 84
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 85
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 86
TYP :: "KIND"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 87
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 88
"TYP \<equiv> Type"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 89
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 90
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 91
KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 92
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 93
"KPI \<equiv> KPi"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 94
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 95
quotient_def
492
+ − 96
TCONST :: "ident \<Rightarrow> TY"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 97
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 98
"TCONST \<equiv> TConst"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 99
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 100
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 101
TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 102
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 103
"TAPP \<equiv> TApp"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 104
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 105
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 106
TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 107
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 108
"TPI \<equiv> TPi"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 109
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 110
(* FIXME: does not work with CONST *)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 111
quotient_def
492
+ − 112
CONS :: "ident \<Rightarrow> TRM"
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 113
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 114
"CONS \<equiv> Const"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 115
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 116
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 117
VAR :: "name \<Rightarrow> TRM"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 118
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 119
"VAR \<equiv> Var"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 120
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 121
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 122
APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 123
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 124
"APP \<equiv> App"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 125
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 126
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 127
LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 128
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 129
"LAM \<equiv> Lam"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 130
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 131
thm TYP_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 132
thm KPI_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 133
thm TCONST_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 134
thm TAPP_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 135
thm TPI_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 136
thm VAR_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 137
thm CONS_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 138
thm APP_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 139
thm LAM_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 140
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 141
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 142
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 143
FV_kind :: "KIND \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 144
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 145
"FV_kind \<equiv> fv_kind"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 146
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 147
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 148
FV_ty :: "TY \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 149
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 150
"FV_ty \<equiv> fv_ty"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 151
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 152
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 153
FV_trm :: "TRM \<Rightarrow> name set"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 154
where
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 155
"FV_trm \<equiv> fv_trm"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 156
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 157
thm FV_kind_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 158
thm FV_ty_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 159
thm FV_trm_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 160
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 161
(* FIXME: does not work yet *)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 162
overloading
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 163
perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 164
perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 165
perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked)
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 166
begin
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 167
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 168
quotient_def
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 169
perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 170
where
299
+ − 171
"perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
+ − 172
+ − 173
quotient_def
+ − 174
perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
+ − 175
where
+ − 176
"perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
+ − 177
+ − 178
quotient_def
+ − 179
perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+ − 180
where
+ − 181
"perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
+ − 182
604
+ − 183
end
+ − 184
439
+ − 185
(* TODO/FIXME: Think whether these RSP theorems are true. *)
506
+ − 186
lemma kpi_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 187
"(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
506
+ − 188
lemma tconst_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
"(op = ===> aty) TConst TConst" sorry
506
+ − 190
lemma tapp_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
"(aty ===> atrm ===> aty) TApp TApp" sorry
506
+ − 192
lemma tpi_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 193
"(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
506
+ − 194
lemma var_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 195
"(op = ===> atrm) Var Var" sorry
506
+ − 196
lemma app_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
"(atrm ===> atrm ===> atrm) App App" sorry
506
+ − 198
lemma const_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 199
"(op = ===> atrm) Const Const" sorry
506
+ − 200
lemma lam_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 201
"(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
437
+ − 202
506
+ − 203
lemma perm_kind_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 204
"(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
506
+ − 205
lemma perm_ty_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 206
"(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
506
+ − 207
lemma perm_trm_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 208
"(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
437
+ − 209
506
+ − 210
lemma fv_ty_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 211
"(aty ===> op =) fv_ty fv_ty" sorry
506
+ − 212
lemma fv_kind_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 213
"(akind ===> op =) fv_kind fv_kind" sorry
506
+ − 214
lemma fv_trm_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 215
"(atrm ===> op =) fv_trm fv_trm" sorry
441
+ − 216
439
+ − 217
301
+ − 218
thm akind_aty_atrm.induct
456
+ − 219
thm kind_ty_trm.induct
394
+ − 220
456
+ − 221
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 222
lemma
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 223
assumes a0:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
"P1 TYP TYP"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
and a1:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
"\<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk>
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 227
\<Longrightarrow> P1 (KPI A x K) (KPI A' x K')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 228
and a2:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 229
"\<And>A A' K K' x x'. \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K');
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 231
and a3:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 232
"\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 233
and a4:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 234
"\<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 235
and a5:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 236
"\<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 237
and a6:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
"\<And>A A' B x x' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B');
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
and a7:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 241
"\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 242
and a8:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
"\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 244
and a9:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 245
"\<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 246
and a10:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 247
"\<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 248
and a11:
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 249
"\<And>A A' M x x' M' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M');
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and>
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
apply -
567
+ − 256
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
582
+ − 257
apply(tactic {* regularize_tac @{context} 1 *})
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
apply(tactic {* all_inj_repabs_tac @{context} 1 *})
573
+ − 259
apply(fold perm_kind_def perm_ty_def perm_trm_def)
506
+ − 260
apply(tactic {* clean_tac @{context} 1 *})
492
+ − 261
(*
+ − 262
Profiling:
+ − 263
ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
+ − 264
ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
534
+ − 265
ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
496
+ − 266
ML_prf {* PolyML.profiling 1 *}
+ − 267
ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
500
+ − 268
*)
441
+ − 269
done
425
12fc780ff0e8
Integrated Stefan's tactic and changed substs to simps with empty context.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 270
458
+ − 271
(* Does not work:
+ − 272
lemma
+ − 273
assumes a0: "P1 TYP"
+ − 274
and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"
+ − 275
and a2: "\<And>id. P2 (TCONST id)"
+ − 276
and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"
+ − 277
and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"
+ − 278
and a5: "\<And>id. P3 (CONS id)"
+ − 279
and a6: "\<And>name. P3 (VAR name)"
+ − 280
and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"
+ − 281
and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"
+ − 282
shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"
+ − 283
using a0 a1 a2 a3 a4 a5 a6 a7 a8
+ − 284
*)
+ − 285
580
+ − 286
lemma "\<lbrakk>P TYP;
+ − 287
\<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);
+ − 288
\<And>id. Q (TCONST id);
+ − 289
\<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);
+ − 290
\<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);
+ − 291
\<And>id. R (CONS id); \<And>name. R (VAR name);
+ − 292
\<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
+ − 293
\<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
+ − 294
\<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
586
+ − 295
apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
456
+ − 296
done
+ − 297
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 298
end
299
+ − 299
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 300
299
+ − 301
604
+ − 302