72 apply auto |
72 apply auto |
73 defer |
73 defer |
74 apply (case_tac x) |
74 apply (case_tac x) |
75 apply (rule_tac y="a" in lt.exhaust) |
75 apply (rule_tac y="a" in lt.exhaust) |
76 apply auto |
76 apply auto |
|
77 apply blast |
77 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
78 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
78 apply (simp add: Abs1_eq_iff) |
79 apply (simp add: Abs1_eq_iff) |
79 apply blast+ |
80 apply blast+ |
80 apply (rule_tac y="b" in lt.exhaust) |
81 apply (rule_tac y="b" in lt.exhaust) |
81 apply auto |
82 apply auto |
82 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
83 apply (simp add: Abs1_eq_iff) |
|
84 apply blast |
|
85 apply (rule_tac ?'a="name" in obtain_fresh) |
83 apply (rule_tac ?'a="name" in obtain_fresh) |
86 apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh) |
84 apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh) |
87 apply (simp add: fresh_Pair_elim) |
85 apply (simp add: fresh_Pair_elim) |
88 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
86 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
89 apply (simp_all add: fresh_Pair)[4] |
87 apply (simp_all add: fresh_Pair)[4] |
|
88 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
89 apply (simp add: Abs1_eq_iff) |
|
90 apply blast |
90 --"" |
91 --"" |
91 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
92 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
92 apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
93 apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
93 apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
94 apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
94 apply (simp only:) |
95 apply (simp only:) |