1599
|
1 |
theory ExTySch
|
|
2 |
imports "Parser"
|
1271
|
3 |
begin
|
|
4 |
|
1599
|
5 |
(* Type Schemes *)
|
1271
|
6 |
atom_decl name
|
|
7 |
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
8 |
nominal_datatype t =
|
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
9 |
Var "name"
|
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
10 |
| Fun "t" "t"
|
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
11 |
and tyS =
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
12 |
All xs::"name fset" ty::"t" bind xs in ty
|
1271
|
13 |
|
1568
|
14 |
lemma size_eqvt_raw:
|
|
15 |
"size (pi \<bullet> t :: t_raw) = size t"
|
|
16 |
"size (pi \<bullet> ts :: tyS_raw) = size ts"
|
|
17 |
apply (induct rule: t_raw_tyS_raw.inducts)
|
|
18 |
apply simp_all
|
|
19 |
done
|
1562
|
20 |
|
|
21 |
instantiation t and tyS :: size begin
|
|
22 |
|
|
23 |
quotient_definition
|
|
24 |
"size_t :: t \<Rightarrow> nat"
|
|
25 |
is
|
|
26 |
"size :: t_raw \<Rightarrow> nat"
|
|
27 |
|
|
28 |
quotient_definition
|
|
29 |
"size_tyS :: tyS \<Rightarrow> nat"
|
|
30 |
is
|
|
31 |
"size :: tyS_raw \<Rightarrow> nat"
|
|
32 |
|
|
33 |
lemma size_rsp:
|
|
34 |
"alpha_t_raw x y \<Longrightarrow> size x = size y"
|
|
35 |
"alpha_tyS_raw a b \<Longrightarrow> size a = size b"
|
|
36 |
apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
|
|
37 |
apply (simp_all only: t_raw_tyS_raw.size)
|
|
38 |
apply (simp_all only: alpha_gen)
|
|
39 |
apply clarify
|
1568
|
40 |
apply (simp_all only: size_eqvt_raw)
|
1562
|
41 |
done
|
|
42 |
|
|
43 |
lemma [quot_respect]:
|
|
44 |
"(alpha_t_raw ===> op =) size size"
|
|
45 |
"(alpha_tyS_raw ===> op =) size size"
|
|
46 |
by (simp_all add: size_rsp)
|
|
47 |
|
|
48 |
lemma [quot_preserve]:
|
|
49 |
"(rep_t ---> id) size = size"
|
|
50 |
"(rep_tyS ---> id) size = size"
|
|
51 |
by (simp_all add: size_t_def size_tyS_def)
|
|
52 |
|
|
53 |
instance
|
|
54 |
by default
|
|
55 |
|
|
56 |
end
|
|
57 |
|
|
58 |
thm t_raw_tyS_raw.size(4)[quot_lifted]
|
|
59 |
thm t_raw_tyS_raw.size(5)[quot_lifted]
|
|
60 |
thm t_raw_tyS_raw.size(6)[quot_lifted]
|
|
61 |
|
|
62 |
|
1515
|
63 |
thm t_tyS.fv
|
|
64 |
thm t_tyS.eq_iff
|
|
65 |
thm t_tyS.bn
|
|
66 |
thm t_tyS.perm
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
67 |
thm t_tyS.inducts
|
1515
|
68 |
thm t_tyS.distinct
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
69 |
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
|
1430
|
70 |
|
1553
4355eb3b7161
Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
72 |
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
73 |
lemma induct:
|
1537
0b21101157b1
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
74 |
assumes a1: "\<And>name b. P b (Var name)"
|
0b21101157b1
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
75 |
and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
|
1538
|
76 |
and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
|
1568
|
77 |
shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
|
1537
0b21101157b1
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
78 |
proof -
|
1539
|
79 |
have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
|
1538
|
80 |
apply (rule t_tyS.induct)
|
1537
0b21101157b1
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
81 |
apply (simp add: a1)
|
1539
|
82 |
apply (simp)
|
|
83 |
apply (rule allI)+
|
1538
|
84 |
apply (rule a2)
|
1539
|
85 |
apply simp
|
|
86 |
apply simp
|
|
87 |
apply (rule allI)
|
1538
|
88 |
apply (rule allI)
|
1605
|
89 |
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
|
1539
|
90 |
apply clarify
|
1605
|
91 |
apply(rule_tac t="p \<bullet> All fset t" and
|
|
92 |
s="pa \<bullet> (p \<bullet> All fset t)" in subst)
|
1568
|
93 |
apply (rule supp_perm_eq)
|
|
94 |
apply assumption
|
|
95 |
apply (simp only: t_tyS.perm)
|
1538
|
96 |
apply (rule a3)
|
1568
|
97 |
apply(erule_tac x="(pa + p)" in allE)
|
|
98 |
apply simp
|
|
99 |
apply (simp add: eqvts eqvts_raw)
|
|
100 |
apply (rule at_set_avoiding2)
|
|
101 |
apply (simp add: fin_fset_to_set)
|
|
102 |
apply (simp add: finite_supp)
|
|
103 |
apply (simp add: eqvts finite_supp)
|
|
104 |
apply (subst atom_eqvt_raw[symmetric])
|
|
105 |
apply (subst fmap_eqvt[symmetric])
|
|
106 |
apply (subst fset_to_set_eqvt[symmetric])
|
|
107 |
apply (simp only: fresh_star_permute_iff)
|
|
108 |
apply (simp add: fresh_star_def)
|
|
109 |
apply clarify
|
|
110 |
apply (simp add: fresh_def)
|
|
111 |
apply (simp add: t_tyS_supp)
|
|
112 |
done
|
1538
|
113 |
then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
|
|
114 |
then show ?thesis by simp
|
1537
0b21101157b1
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
115 |
qed
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
116 |
|
1271
|
117 |
lemma
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
118 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
|
1515
|
119 |
apply(simp add: t_tyS.eq_iff)
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
120 |
apply(rule_tac x="0::perm" in exI)
|
1271
|
121 |
apply(simp add: alpha_gen)
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
122 |
apply(auto)
|
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
123 |
apply(simp add: fresh_star_def fresh_zero_perm)
|
1271
|
124 |
done
|
|
125 |
|
|
126 |
lemma
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
127 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
|
1515
|
128 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
129 |
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
|
1510
|
130 |
apply(simp add: alpha_gen fresh_star_def eqvts)
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
131 |
apply auto
|
1271
|
132 |
done
|
|
133 |
|
|
134 |
lemma
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
135 |
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
|
1515
|
136 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
137 |
apply(rule_tac x="0::perm" in exI)
|
1515
|
138 |
apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
139 |
oops
|
1271
|
140 |
|
|
141 |
lemma
|
|
142 |
assumes a: "a \<noteq> b"
|
1525
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
143 |
shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
|
1271
|
144 |
using a
|
1515
|
145 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
146 |
apply(clarify)
|
1515
|
147 |
apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
|
1477
4ac3485899e1
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
148 |
apply auto
|
1271
|
149 |
done
|
|
150 |
|
1596
|
151 |
(* PROBLEM:
|
|
152 |
Type schemes with separate datatypes
|
|
153 |
|
|
154 |
nominal_datatype T =
|
|
155 |
TVar "name"
|
|
156 |
| TFun "T" "T"
|
|
157 |
nominal_datatype TyS =
|
|
158 |
TAll xs::"name list" ty::"T" bind xs in ty
|
|
159 |
|
|
160 |
*** exception Datatype raised
|
|
161 |
*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
|
|
162 |
*** At command "nominal_datatype".
|
|
163 |
*)
|
|
164 |
|
|
165 |
|
1271
|
166 |
end
|