44 ]) 1 |
44 ]) 1 |
45 end |
45 end |
46 ) |
46 ) |
47 *} |
47 *} |
48 |
48 |
49 |
49 ML {* |
50 prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *} |
|
51 ML_prf {* |
|
52 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
50 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
53 ind_tac induct THEN_ALL_NEW |
51 ind_tac induct THEN_ALL_NEW |
54 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
52 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
55 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
53 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
56 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) |
54 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) |
57 THEN_ALL_NEW split_conjs |
55 THEN_ALL_NEW split_conjs |
58 *} |
56 *} |
59 |
57 (*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 *})*) |
60 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 *}) |
58 |
61 apply (simp_all) |
59 lemma "alpha_weird_raw x y \<longrightarrow> (\<forall>z. alpha_weird_raw y z \<longrightarrow> alpha_weird_raw x z)" |
|
60 apply (rule impI) |
|
61 apply (erule alpha_weird_raw.induct) |
|
62 apply (simp_all add: weird_inj) |
|
63 defer |
|
64 apply (rule allI) |
|
65 apply (rule impI) |
|
66 apply (erule alpha_weird_raw.cases) |
|
67 apply (simp_all add: weird_inj) |
|
68 apply (rule allI) |
|
69 apply (rule impI) |
|
70 apply (erule alpha_weird_raw.cases) |
|
71 apply (simp_all add: weird_inj) |
|
72 apply (erule conjE)+ |
|
73 apply (erule exE)+ |
|
74 apply (rule conjI) |
|
75 apply (rule_tac x="pica + pic" in exI) |
62 apply (erule alpha_gen_compose_trans) |
76 apply (erule alpha_gen_compose_trans) |
63 apply assumption |
77 apply assumption |
64 apply (simp add: alpha_eqvt) |
78 apply (simp add: alpha_eqvt) |
65 defer defer |
79 apply (rule conjI) |
|
80 defer |
|
81 apply (rule_tac x="pia + pi" in exI) |
66 apply (erule alpha_gen_compose_trans) |
82 apply (erule alpha_gen_compose_trans) |
67 apply assumption |
83 apply assumption |
68 apply (simp add: alpha_eqvt) |
84 apply (simp add: alpha_eqvt) |
69 apply (subgoal_tac "pia + pb + (pib + pa) = (pia + pib) + (pb + pa)") |
85 (* Normally: (pia + pb + (pib + pa)) *) |
70 apply simp |
86 apply (rule_tac x="piaa + pib" in exI) |
|
87 apply (rule_tac x="piab + piba" in exI) |
71 apply (erule alpha_gen_compose_trans) |
88 apply (erule alpha_gen_compose_trans) |
72 apply assumption |
89 apply assumption |
73 apply (simp add: alpha_eqvt) |
90 apply (simp add: alpha_eqvt) |
74 sorry |
91 done |
75 |
92 |
|
93 lemma "alpha_weird_raw x y \<Longrightarrow> alpha_weird_raw y x" |
|
94 apply (erule alpha_weird_raw.induct) |
|
95 apply (simp_all add: weird_inj) |
|
96 apply (erule conjE)+ |
|
97 apply (erule exE)+ |
|
98 apply (rule conjI) |
|
99 defer (* simple *) |
|
100 apply (rule conjI) |
|
101 apply (rule_tac x="- pia" in exI) |
|
102 apply (rule_tac x="- pib" in exI) |
|
103 apply (simp add: minus_add[symmetric]) |
|
104 apply (erule alpha_gen_compose_sym) |
|
105 apply (simp_all add: alpha_eqvt) |
|
106 apply (rule_tac x="- pi" in exI) |
|
107 apply (erule alpha_gen_compose_sym) |
|
108 apply (simp_all add: alpha_eqvt) |
|
109 apply (rule_tac x="- pic" in exI) |
|
110 apply (erule alpha_gen_compose_sym) |
|
111 apply (simp_all add: alpha_eqvt) |
|
112 done |
76 |
113 |
77 |
114 |
78 abbreviation "WBind \<equiv> WBind_raw" |
115 abbreviation "WBind \<equiv> WBind_raw" |
79 abbreviation "WP \<equiv> WP_raw" |
116 abbreviation "WP \<equiv> WP_raw" |
80 abbreviation "WV \<equiv> WV_raw" |
117 abbreviation "WV \<equiv> WV_raw" |