1271
|
1 |
theory TySch
|
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
|
2 |
imports "Parser" "../Attic/Prove" "FSet"
|
1271
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
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
|
7 |
ML {* val _ = cheat_fv_rsp := false *}
|
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 |
ML {* val _ = cheat_const_rsp := false *}
|
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 |
ML {* val _ = cheat_equivp := false *}
|
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 |
ML {* val _ = cheat_fv_eqvt := false *}
|
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 |
ML {* val _ = cheat_alpha_eqvt := false *}
|
1271
|
12 |
|
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
|
13 |
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
|
14 |
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
|
15 |
| 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
|
16 |
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
|
17 |
All xs::"name fset" ty::"t" bind xs in ty
|
1271
|
18 |
|
1515
|
19 |
thm t_tyS.fv
|
|
20 |
thm t_tyS.eq_iff
|
|
21 |
thm t_tyS.bn
|
|
22 |
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
|
23 |
thm t_tyS.inducts
|
1515
|
24 |
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
|
25 |
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
|
1430
|
26 |
|
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
|
27 |
lemma finite_fv_t_tyS:
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
28 |
shows "finite (fv_t t)" "finite (fv_tyS ts)"
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
29 |
by (induct rule: t_tyS.inducts) (simp_all)
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
30 |
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
31 |
lemma supp_fv_t_tyS:
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
32 |
shows "fv_t t = supp t" "fv_tyS ts = supp ts"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
33 |
apply(induct rule: t_tyS.inducts)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
34 |
apply(simp_all only: t_tyS.fv)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
35 |
prefer 3
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
36 |
apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
37 |
prefer 2
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
38 |
apply(subst finite_supp_Abs)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
39 |
apply(drule sym)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
40 |
apply(simp add: finite_fv_t_tyS(1))
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
41 |
apply(simp)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
42 |
apply(simp_all (no_asm) only: supp_def)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
43 |
apply(simp_all only: t_tyS.perm)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
apply(simp_all only: permute_ABS)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
45 |
apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
46 |
apply(simp_all only: alpha_gen)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
47 |
apply(simp_all only: eqvts[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
48 |
apply(simp_all only: eqvts eqvts_raw)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
49 |
apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
50 |
apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
apply(simp_all only: de_Morgan_conj[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
52 |
done
|
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
|
53 |
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
54 |
instance t and tyS :: fs
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
55 |
apply default
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
56 |
apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
57 |
done
|
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
|
58 |
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
60 |
|
bf321f16d025
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
61 |
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
|
62 |
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
|
63 |
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
|
64 |
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)"
|
|
65 |
shows "P a t \<and> P' d 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
|
66 |
proof -
|
1538
|
67 |
have " (\<forall>p. P a (p \<bullet> t)) \<and> (\<forall>p. P' d (p \<bullet> ts))"
|
|
68 |
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
|
69 |
apply (simp add: a1)
|
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
|
70 |
apply (simp_all)
|
1538
|
71 |
apply (rule allI)
|
|
72 |
apply (rule a2)
|
|
73 |
defer defer
|
|
74 |
apply (rule allI)
|
|
75 |
apply (rule a3)
|
|
76 |
apply simp_all
|
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
|
77 |
sorry
|
1538
|
78 |
then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
|
|
79 |
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
|
80 |
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
|
81 |
|
1271
|
82 |
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
|
83 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
|
1515
|
84 |
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
|
85 |
apply(rule_tac x="0::perm" in exI)
|
1271
|
86 |
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
|
87 |
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
|
88 |
apply(simp add: fresh_star_def fresh_zero_perm)
|
1271
|
89 |
done
|
|
90 |
|
|
91 |
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
|
92 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
|
1515
|
93 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
94 |
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
|
1510
|
95 |
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
|
96 |
apply auto
|
1271
|
97 |
done
|
|
98 |
|
|
99 |
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
|
100 |
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
|
1515
|
101 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
102 |
apply(rule_tac x="0::perm" in exI)
|
1515
|
103 |
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
|
104 |
oops
|
1271
|
105 |
|
|
106 |
lemma
|
|
107 |
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
|
108 |
shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
|
1271
|
109 |
using a
|
1515
|
110 |
apply(simp add: t_tyS.eq_iff)
|
1271
|
111 |
apply(clarify)
|
1515
|
112 |
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
|
113 |
apply auto
|
1271
|
114 |
done
|
|
115 |
|
|
116 |
end
|