author | wenzelm |
Sat, 23 Apr 2011 13:00:19 +0200 | |
changeset 42463 | f270e3e18be5 |
parent 42187 | b4f4ed5b8586 |
child 45125 | c15b0faeb70a |
permissions | -rw-r--r-- |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
1 |
theory Specialisation_Examples |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40054
diff
changeset
|
2 |
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
begin |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
|
42187 | 5 |
declare [[values_timeout = 480.0]] |
42142
d24a93025feb
raised various timeouts to accommodate sluggish SML/NJ
krauss
parents:
41413
diff
changeset
|
6 |
|
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
section {* Specialisation Examples *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
|
39919
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
9 |
primrec nth_el' |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
"nth_el' [] i = None" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
definition |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
15 |
"greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
|
36257
3f3e9f18f302
adopting examples to changes in the predicate compiler
bulwahn
parents:
36054
diff
changeset
|
17 |
code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index . |
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39919
diff
changeset
|
18 |
ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *} |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
19 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
thm greater_than_index.equation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
values [expected "{}"] "{x. greater_than_index [0,2,3,2]}" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
subsection {* Common subterms *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
text {* If a predicate is called with common subterms as arguments, |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
this predicate should be specialised. |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
*} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
definition max_nat :: "nat => nat => nat" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
where "max_nat a b = (if a <= b then b else a)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
lemma [code_pred_inline]: |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
"max = max_nat" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
36 |
by (simp add: fun_eq_iff max_def max_nat_def) |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
definition |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
"max_of_my_Suc x = max x (Suc x)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
text {* In this example, max is specialised, hence the mode o => i => bool is possible *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
|
36257
3f3e9f18f302
adopting examples to changes in the predicate compiler
bulwahn
parents:
36054
diff
changeset
|
43 |
code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc . |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
45 |
thm max_of_my_SucP.equation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
|
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39919
diff
changeset
|
47 |
ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *} |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
48 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
49 |
values "{x. max_of_my_SucP x 6}" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
50 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
51 |
subsection {* Sorts *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
52 |
|
39919
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
53 |
declare sorted.Nil [code_pred_intro] |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
54 |
sorted_single [code_pred_intro] |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
55 |
sorted_many [code_pred_intro] |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
56 |
|
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
57 |
code_pred sorted proof - |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
58 |
assume "sorted xa" |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
59 |
assume 1: "xa = [] \<Longrightarrow> thesis" |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
60 |
assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis" |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
61 |
assume 3: "\<And>x y zs. xa = x # y # zs \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> thesis" |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
62 |
show thesis proof (cases xa) |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
63 |
case Nil with 1 show ?thesis . |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
64 |
next |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
65 |
case (Cons x xs) show ?thesis proof (cases xs) |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
66 |
case Nil with Cons 2 show ?thesis by simp |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
67 |
next |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
68 |
case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
69 |
moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
70 |
ultimately show ?thesis by (rule 3) |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
71 |
qed |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
72 |
qed |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
73 |
qed |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
thm sorted.equation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
76 |
section {* Specialisation in POPLmark theory *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
78 |
notation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
79 |
Some ("\<lfloor>_\<rfloor>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
80 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
notation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
82 |
None ("\<bottom>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
84 |
notation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
85 |
length ("\<parallel>_\<parallel>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
86 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
87 |
notation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
88 |
Cons ("_ \<Colon>/ _" [66, 65] 65) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
89 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
90 |
primrec |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
91 |
nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
92 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
93 |
"[]\<langle>i\<rangle> = \<bottom>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
94 |
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> \<lfloor>x\<rfloor> | Suc j \<Rightarrow> xs \<langle>j\<rangle>)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
96 |
primrec assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" ("_\<langle>_\<rangle>\<^isub>?" [90, 0] 91) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
97 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
98 |
"[]\<langle>a\<rangle>\<^isub>? = \<bottom>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
99 |
| "(x # xs)\<langle>a\<rangle>\<^isub>? = (if fst x = a then \<lfloor>snd x\<rfloor> else xs\<langle>a\<rangle>\<^isub>?)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
100 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
101 |
primrec unique :: "('a \<times> 'b) list \<Rightarrow> bool" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
102 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
103 |
"unique [] = True" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
104 |
| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^isub>? = \<bottom> \<and> unique xs)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
105 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
106 |
datatype type = |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
107 |
TVar nat |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
108 |
| Top |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
109 |
| Fun type type (infixr "\<rightarrow>" 200) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
110 |
| TyAll type type ("(3\<forall><:_./ _)" [0, 10] 10) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
111 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
112 |
datatype binding = VarB type | TVarB type |
42463 | 113 |
type_synonym env = "binding list" |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
114 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
115 |
primrec is_TVarB :: "binding \<Rightarrow> bool" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
116 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
117 |
"is_TVarB (VarB T) = False" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
118 |
| "is_TVarB (TVarB T) = True" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
119 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
120 |
primrec type_ofB :: "binding \<Rightarrow> type" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
121 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
122 |
"type_ofB (VarB T) = T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
123 |
| "type_ofB (TVarB T) = T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
124 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
125 |
primrec mapB :: "(type \<Rightarrow> type) \<Rightarrow> binding \<Rightarrow> binding" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
126 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
127 |
"mapB f (VarB T) = VarB (f T)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
128 |
| "mapB f (TVarB T) = TVarB (f T)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
129 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
130 |
datatype trm = |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
131 |
Var nat |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
132 |
| Abs type trm ("(3\<lambda>:_./ _)" [0, 10] 10) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
133 |
| TAbs type trm ("(3\<lambda><:_./ _)" [0, 10] 10) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
134 |
| App trm trm (infixl "\<bullet>" 200) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
135 |
| TApp trm type (infixl "\<bullet>\<^isub>\<tau>" 200) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
136 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
137 |
primrec liftT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<up>\<^isub>\<tau>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
138 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
139 |
"\<up>\<^isub>\<tau> n k (TVar i) = (if i < k then TVar i else TVar (i + n))" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
140 |
| "\<up>\<^isub>\<tau> n k Top = Top" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
141 |
| "\<up>\<^isub>\<tau> n k (T \<rightarrow> U) = \<up>\<^isub>\<tau> n k T \<rightarrow> \<up>\<^isub>\<tau> n k U" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
142 |
| "\<up>\<^isub>\<tau> n k (\<forall><:T. U) = (\<forall><:\<up>\<^isub>\<tau> n k T. \<up>\<^isub>\<tau> n (k + 1) U)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
143 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
144 |
primrec lift :: "nat \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("\<up>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
145 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
146 |
"\<up> n k (Var i) = (if i < k then Var i else Var (i + n))" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
147 |
| "\<up> n k (\<lambda>:T. t) = (\<lambda>:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
148 |
| "\<up> n k (\<lambda><:T. t) = (\<lambda><:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
149 |
| "\<up> n k (s \<bullet> t) = \<up> n k s \<bullet> \<up> n k t" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
150 |
| "\<up> n k (t \<bullet>\<^isub>\<tau> T) = \<up> n k t \<bullet>\<^isub>\<tau> \<up>\<^isub>\<tau> n k T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
151 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
152 |
primrec substTT :: "type \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>\<tau>" [300, 0, 0] 300) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
153 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
154 |
"(TVar i)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
155 |
(if k < i then TVar (i - 1) else if i = k then \<up>\<^isub>\<tau> k 0 S else TVar i)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
156 |
| "Top[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = Top" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
157 |
| "(T \<rightarrow> U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> \<rightarrow> U[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
158 |
| "(\<forall><:T. U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = (\<forall><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. U[k+1 \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
159 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
160 |
primrec decT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<down>\<^isub>\<tau>") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
161 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
162 |
"\<down>\<^isub>\<tau> 0 k T = T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
163 |
| "\<down>\<^isub>\<tau> (Suc n) k T = \<down>\<^isub>\<tau> n k (T[k \<mapsto>\<^isub>\<tau> Top]\<^isub>\<tau>)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
164 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
165 |
primrec subst :: "trm \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("_[_ \<mapsto> _]" [300, 0, 0] 300) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
166 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
167 |
"(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
168 |
| "(t \<bullet> u)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet> u[k \<mapsto> s]" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
169 |
| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet>\<^isub>\<tau> \<down>\<^isub>\<tau> 1 k T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
170 |
| "(\<lambda>:T. t)[k \<mapsto> s] = (\<lambda>:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
171 |
| "(\<lambda><:T. t)[k \<mapsto> s] = (\<lambda><:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
172 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
173 |
primrec substT :: "trm \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> trm" ("_[_ \<mapsto>\<^isub>\<tau> _]" [300, 0, 0] 300) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
174 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
175 |
"(Var i)[k \<mapsto>\<^isub>\<tau> S] = (if k < i then Var (i - 1) else Var i)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
176 |
| "(t \<bullet> u)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet> u[k \<mapsto>\<^isub>\<tau> S]" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
177 |
| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet>\<^isub>\<tau> T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
178 |
| "(\<lambda>:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda>:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
179 |
| "(\<lambda><:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
180 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
181 |
primrec liftE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<up>\<^isub>e") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
182 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
183 |
"\<up>\<^isub>e n k [] = []" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
184 |
| "\<up>\<^isub>e n k (B \<Colon> \<Gamma>) = mapB (\<up>\<^isub>\<tau> n (k + \<parallel>\<Gamma>\<parallel>)) B \<Colon> \<up>\<^isub>e n k \<Gamma>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
185 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
186 |
primrec substE :: "env \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> env" ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>e" [300, 0, 0] 300) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
187 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
188 |
"[][k \<mapsto>\<^isub>\<tau> T]\<^isub>e = []" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
189 |
| "(B \<Colon> \<Gamma>)[k \<mapsto>\<^isub>\<tau> T]\<^isub>e = mapB (\<lambda>U. U[k + \<parallel>\<Gamma>\<parallel> \<mapsto>\<^isub>\<tau> T]\<^isub>\<tau>) B \<Colon> \<Gamma>[k \<mapsto>\<^isub>\<tau> T]\<^isub>e" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
190 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
191 |
primrec decE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<down>\<^isub>e") |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
192 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
193 |
"\<down>\<^isub>e 0 k \<Gamma> = \<Gamma>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
194 |
| "\<down>\<^isub>e (Suc n) k \<Gamma> = \<down>\<^isub>e n k (\<Gamma>[k \<mapsto>\<^isub>\<tau> Top]\<^isub>e)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
195 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
196 |
inductive |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
197 |
well_formed :: "env \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
198 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
199 |
wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
200 |
| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
201 |
| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
202 |
| wf_all: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
203 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
204 |
inductive |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
205 |
well_formedE :: "env \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
206 |
and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
207 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
208 |
"\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
209 |
| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
210 |
| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
211 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
212 |
inductive_cases well_formed_cases: |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
213 |
"\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
214 |
"\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
215 |
"\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
216 |
"\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
217 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
218 |
inductive_cases well_formedE_cases: |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
219 |
"B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
220 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
221 |
inductive |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
222 |
subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [50, 50, 50] 50) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
223 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
224 |
SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
225 |
| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
226 |
| SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow> |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
227 |
\<Gamma> \<turnstile> \<up>\<^isub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
228 |
| SA_arrow: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
229 |
| SA_all: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
230 |
\<Gamma> \<turnstile> (\<forall><:S\<^isub>1. S\<^isub>2) <: (\<forall><:T\<^isub>1. T\<^isub>2)" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
231 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
232 |
inductive |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
233 |
typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
234 |
where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
235 |
T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
236 |
| T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2" |
39919
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
237 |
| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>11 \<rightarrow> T\<^isub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>12" |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
238 |
| T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)" |
39919
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
239 |
| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>11. T\<^isub>12) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11 \<Longrightarrow> |
9f6503aaa77d
adjusted to inductive characterization of sorted
haftmann
parents:
39302
diff
changeset
|
240 |
\<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>12[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>" |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
241 |
| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
242 |
|
36257
3f3e9f18f302
adopting examples to changes in the predicate compiler
bulwahn
parents:
36054
diff
changeset
|
243 |
code_pred [inductify, skip_proof, specialise] typing . |
36033
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
244 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
245 |
thm typing.equation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
246 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
247 |
values 6 "{(E, t, T). typing E t T}" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
248 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
249 |
subsection {* Higher-order predicate *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
250 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
251 |
code_pred [inductify] mapB . |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
252 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
253 |
subsection {* Multiple instances *} |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
254 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
255 |
inductive subtype_refl' where |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
256 |
"\<Gamma> \<turnstile> t : T ==> \<not> (\<Gamma> \<turnstile> T <: T) ==> subtype_refl' t T" |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
257 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
258 |
code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' . |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
259 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
260 |
thm subtype_refl'.equation |
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
261 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
262 |
|
7106f079bd05
adding specialisation examples of the predicate compiler
bulwahn
parents:
diff
changeset
|
263 |
end |