equal
deleted
inserted
replaced
109 by (fast_tac HOL_cs 1); |
109 by (fast_tac HOL_cs 1); |
110 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
110 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
111 by (lift.induct_tac "x" 1); |
111 by (lift.induct_tac "x" 1); |
112 auto(); |
112 auto(); |
113 qed "refl_per_one"; |
113 qed "refl_per_one"; |
114 |
|
115 (* weq *) |
|
116 val prems = goal thy |
|
117 "[|x~=UU; y~=UU|]==>(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"; |
|
118 by(subgoal_tac"x~=UU&y~=UU-->(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"1); |
|
119 by (cut_facts_tac prems 1); |
|
120 by (fast_tac HOL_cs 1); |
|
121 by (lift.induct_tac "x" 1); |
|
122 by (lift.induct_tac "y" 2); |
|
123 by (lift.induct_tac "y" 1); |
|
124 auto(); |
|
125 br refl_per_one 1; |
|
126 auto(); |
|
127 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
|
128 result(); |
|
129 |
|