12 |
12 |
13 thm permute_weird_raw.simps[no_vars] |
13 thm permute_weird_raw.simps[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
16 |
16 |
17 thm eqvts |
|
18 |
|
19 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *} |
|
20 thm weird_inj |
|
21 |
|
22 (*local_setup {* |
|
23 (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []), |
|
24 build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *} |
|
25 |
|
26 (*prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *} |
|
27 |
|
28 apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj} @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *}) |
|
29 *) |
|
30 lemma "alpha_weird_raw x y \<longrightarrow> (\<forall>z. alpha_weird_raw y z \<longrightarrow> alpha_weird_raw x z)" |
|
31 apply (rule impI) |
|
32 apply (erule alpha_weird_raw.induct) |
|
33 apply (simp_all add: weird_inj) |
|
34 defer |
|
35 apply (rule allI) |
|
36 apply (rule impI) |
|
37 apply (erule alpha_weird_raw.cases) |
|
38 apply (simp_all add: weird_inj) |
|
39 apply (rule allI) |
|
40 apply (rule impI) |
|
41 apply (erule alpha_weird_raw.cases) |
|
42 apply (simp_all add: weird_inj) |
|
43 apply (erule conjE)+ |
|
44 apply (erule exE)+ |
|
45 apply (erule conjE)+ |
|
46 apply (erule exE)+ |
|
47 apply (rule conjI) |
|
48 apply (rule_tac x="pica + pic" in exI) |
|
49 apply (erule alpha_gen_compose_trans) |
|
50 apply assumption |
|
51 apply (simp add: alpha_eqvt) |
|
52 apply (rule_tac x="pia + pib" in exI) |
|
53 apply (rule_tac x="piaa + piba" in exI) |
|
54 apply (rule conjI) |
|
55 apply (erule alpha_gen_compose_trans) |
|
56 apply assumption |
|
57 apply (simp add: alpha_eqvt) |
|
58 apply (rule conjI) |
|
59 defer |
|
60 apply (rule_tac x="pid + pi" in exI) |
|
61 apply (erule alpha_gen_compose_trans) |
|
62 apply assumption |
|
63 apply (simp add: alpha_eqvt) |
|
64 sorry |
|
65 |
|
66 lemma "alpha_weird_raw x y \<Longrightarrow> alpha_weird_raw y x" |
|
67 apply (erule alpha_weird_raw.induct) |
|
68 apply (simp_all add: weird_inj) |
|
69 apply (erule conjE)+ |
|
70 apply (erule exE)+ |
|
71 apply (erule conjE)+ |
|
72 apply (erule exE)+ |
|
73 apply (rule conjI) |
|
74 apply (rule_tac x="- pic" in exI) |
|
75 apply (erule alpha_gen_compose_sym) |
|
76 apply (simp_all add: alpha_eqvt) |
|
77 apply (rule_tac x="- pia" in exI) |
|
78 apply (rule_tac x="- pib" in exI) |
|
79 apply (simp add: minus_add[symmetric]) |
|
80 apply (rule conjI) |
|
81 apply (erule alpha_gen_compose_sym) |
|
82 apply (simp_all add: alpha_eqvt) |
|
83 apply (rule conjI) |
|
84 apply (simp add: supp_minus_perm Int_commute) |
|
85 apply (rule_tac x="- pi" in exI) |
|
86 apply (erule alpha_gen_compose_sym) |
|
87 apply (simp_all add: alpha_eqvt) |
|
88 done |
|
89 |
|
90 |
|
91 abbreviation "WBind \<equiv> WBind_raw" |
|
92 abbreviation "WP \<equiv> WP_raw" |
|
93 abbreviation "WV \<equiv> WV_raw" |
|
94 |
|
95 lemma test: |
|
96 assumes a: "distinct [x, y, z]" |
|
97 shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
|
98 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
|
99 apply(rule_tac alpha_weird_raw.intros) |
|
100 unfolding alpha_gen |
|
101 using a |
|
102 apply(auto) |
|
103 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
104 apply(auto) |
|
105 apply(simp add: fresh_star_def flip_def fresh_def supp_swap) |
|
106 apply(rule alpha_weird_raw.intros) |
|
107 apply(simp add: alpha_weird_raw.intros(2)) |
|
108 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
109 apply(rule_tac x="0" in exI) |
|
110 apply(simp add: fresh_star_def) |
|
111 apply(auto) |
|
112 apply(rule alpha_weird_raw.intros) |
|
113 apply(simp add: alpha_weird_raw.intros(2)) |
|
114 apply(simp add: flip_def supp_swap supp_perm) |
|
115 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
116 apply(simp) |
|
117 apply(auto) |
|
118 apply(simp add: flip_def fresh_def supp_swap) |
|
119 apply(rule alpha_weird_raw.intros) |
|
120 apply(simp add: alpha_weird_raw.intros(2)) |
|
121 done*) |
|
122 |
17 |
123 text {* example 1 *} |
18 text {* example 1 *} |
124 |
19 |
125 (* ML {* set show_hyps *} *) |
20 (* ML {* set show_hyps *} *) |
126 |
21 |