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 |
|
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
quotient_type 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 |
|
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
quotient_type
|
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
TY = ty / aty and
|
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
81 |
TRM = trm / atrm
|
534
|
82 |
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
|
83 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
quotient_definition
|
705
|
85 |
"TYP :: KIND"
|
|
86 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
87 |
"Type"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
quotient_definition
|
705
|
90 |
"KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
|
|
91 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
92 |
"KPi"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
quotient_definition
|
705
|
95 |
"TCONST :: ident \<Rightarrow> TY"
|
|
96 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
97 |
"TConst"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
quotient_definition
|
705
|
100 |
"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
|
|
101 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
102 |
"TApp"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
quotient_definition
|
705
|
105 |
"TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
|
|
106 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
107 |
"TPi"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
(* FIXME: does not work with CONST *)
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
quotient_definition
|
705
|
111 |
"CONS :: ident \<Rightarrow> TRM"
|
|
112 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
113 |
"Const"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
quotient_definition
|
705
|
116 |
"VAR :: name \<Rightarrow> TRM"
|
|
117 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
118 |
"Var"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
quotient_definition
|
705
|
121 |
"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
|
|
122 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
123 |
"App"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
quotient_definition
|
705
|
126 |
"LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
|
|
127 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
128 |
"Lam"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
thm TYP_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
thm KPI_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
thm TCONST_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
thm TAPP_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
thm TPI_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
thm VAR_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
thm CONS_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
thm APP_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
thm LAM_def
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
quotient_definition
|
705
|
142 |
"FV_kind :: KIND \<Rightarrow> name set"
|
|
143 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
144 |
"fv_kind"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
quotient_definition
|
705
|
147 |
"FV_ty :: TY \<Rightarrow> name set"
|
|
148 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
149 |
"fv_ty"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
quotient_definition
|
705
|
152 |
"FV_trm :: TRM \<Rightarrow> name set"
|
|
153 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
154 |
"fv_trm"
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
(* 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
|
161 |
overloading
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
begin
|
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
166 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
quotient_definition
|
705
|
168 |
"perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
|
|
169 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
170 |
"(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
|
299
|
171 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
quotient_definition
|
705
|
173 |
"perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
|
|
174 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
175 |
"(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
|
299
|
176 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
177 |
quotient_definition
|
705
|
178 |
"perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
|
|
179 |
as
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
"(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
|
299
|
181 |
|
604
|
182 |
end
|
|
183 |
|
439
|
184 |
(* TODO/FIXME: Think whether these RSP theorems are true. *)
|
636
|
185 |
lemma kpi_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
"(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
|
636
|
187 |
lemma tconst_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
"(op = ===> aty) TConst TConst" sorry
|
636
|
189 |
lemma tapp_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
"(aty ===> atrm ===> aty) TApp TApp" sorry
|
636
|
191 |
lemma tpi_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
"(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
|
636
|
193 |
lemma var_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
"(op = ===> atrm) Var Var" sorry
|
636
|
195 |
lemma app_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
196 |
"(atrm ===> atrm ===> atrm) App App" sorry
|
636
|
197 |
lemma const_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
198 |
"(op = ===> atrm) Const Const" sorry
|
636
|
199 |
lemma lam_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
"(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
|
437
|
201 |
|
636
|
202 |
lemma perm_kind_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
203 |
"(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
|
636
|
204 |
lemma perm_ty_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
205 |
"(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
|
636
|
206 |
lemma perm_trm_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
"(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
|
437
|
208 |
|
636
|
209 |
lemma fv_ty_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
210 |
"(aty ===> op =) fv_ty fv_ty" sorry
|
636
|
211 |
lemma fv_kind_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
"(akind ===> op =) fv_kind fv_kind" sorry
|
636
|
213 |
lemma fv_trm_rsp[quot_respect]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
"(atrm ===> op =) fv_trm fv_trm" sorry
|
441
|
215 |
|
439
|
216 |
|
301
|
217 |
thm akind_aty_atrm.induct
|
456
|
218 |
thm kind_ty_trm.induct
|
394
|
219 |
|
456
|
220 |
|
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
|
221 |
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
|
222 |
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
|
223 |
"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
|
224 |
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
|
225 |
"\<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
|
226 |
\<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
|
227 |
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
|
228 |
"\<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
|
229 |
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
|
230 |
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
|
231 |
"\<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
|
232 |
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
|
233 |
"\<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
|
234 |
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
|
235 |
"\<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
|
236 |
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
|
237 |
"\<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
|
238 |
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
|
239 |
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
|
240 |
"\<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
|
241 |
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
|
242 |
"\<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
|
243 |
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
|
244 |
"\<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
|
245 |
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
|
246 |
"\<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
|
247 |
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
|
248 |
"\<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
|
249 |
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
|
250 |
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
|
251 |
((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
|
252 |
((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
|
253 |
using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
254 |
apply(lifting akind_aty_atrm.induct)
|
492
|
255 |
(*
|
|
256 |
Profiling:
|
|
257 |
ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
|
|
258 |
ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
|
534
|
259 |
ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
|
496
|
260 |
ML_prf {* PolyML.profiling 1 *}
|
|
261 |
ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
|
500
|
262 |
*)
|
731
|
263 |
done
|
425
12fc780ff0e8
Integrated Stefan's tactic and changed substs to simps with empty context.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
264 |
|
458
|
265 |
(* Does not work:
|
|
266 |
lemma
|
|
267 |
assumes a0: "P1 TYP"
|
|
268 |
and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"
|
|
269 |
and a2: "\<And>id. P2 (TCONST id)"
|
|
270 |
and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"
|
|
271 |
and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"
|
|
272 |
and a5: "\<And>id. P3 (CONS id)"
|
|
273 |
and a6: "\<And>name. P3 (VAR name)"
|
|
274 |
and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"
|
|
275 |
and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"
|
|
276 |
shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"
|
|
277 |
using a0 a1 a2 a3 a4 a5 a6 a7 a8
|
|
278 |
*)
|
|
279 |
|
771
b2231990b059
simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
280 |
|
580
|
281 |
lemma "\<lbrakk>P TYP;
|
|
282 |
\<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);
|
|
283 |
\<And>id. Q (TCONST id);
|
|
284 |
\<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);
|
|
285 |
\<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);
|
|
286 |
\<And>id. R (CONS id); \<And>name. R (VAR name);
|
|
287 |
\<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
|
|
288 |
\<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
|
|
289 |
\<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
|
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
290 |
apply(lifting kind_ty_trm.induct)
|
456
|
291 |
done
|
|
292 |
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
293 |
end
|
299
|
294 |
|
297
28b264299590
updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
295 |
|
299
|
296 |
|
604
|
297 |
|