138 

   138 

   139 lemma 

   139 lemma 

   140   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"

   140   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"

   141   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"

   141   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"

   142   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"

   142   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"

   144   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"

   144   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"

   145 by (simp_all add: Quot_True_def ext)

   145 by (simp_all add: Quot_True_def ext)

   146 

   146 

   147 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"

   147 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"

   148 by (simp add: Quot_True_def)

   148 by (simp add: Quot_True_def)

   167 method_setup lifting_setup =

   167 method_setup lifting_setup =

   168   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}

   168   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}

   169   {* Sets up the three goals for the lifting procedure. *}

   169   {* Sets up the three goals for the lifting procedure. *}

   170 

   170 

   171 method_setup regularize =

   171 method_setup regularize =

   173   {* Proves automatically the regularization goals from the lifting procedure. *}

   173   {* Proves automatically the regularization goals from the lifting procedure. *}

   174 

   174 

   175 method_setup injection =

   175 method_setup injection =

   176   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}

   176   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}

   177   {* Proves automatically the rep/abs injection goals from the lifting procedure. *}

   177   {* Proves automatically the rep/abs injection goals from the lifting procedure. *}