src/Pure/logic.ML
changeset 32765 3032c0308019
parent 32026 9898880061df
child 32784 1a5dde5079ac
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
   167 fun mk_conjunction_list [] = true_prop
   167 fun mk_conjunction_list [] = true_prop
   168   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   168   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   169 
   169 
   170 (*(A &&& B) &&& (C &&& D) -- balanced*)
   170 (*(A &&& B) &&& (C &&& D) -- balanced*)
   171 fun mk_conjunction_balanced [] = true_prop
   171 fun mk_conjunction_balanced [] = true_prop
   172   | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
   172   | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
   173 
   173 
   174 
   174 
   175 (*A &&& B*)
   175 (*A &&& B*)
   176 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   176 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   177   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   177   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   182     NONE => [t]
   182     NONE => [t]
   183   | SOME (A, B) => A :: dest_conjunction_list B);
   183   | SOME (A, B) => A :: dest_conjunction_list B);
   184 
   184 
   185 (*(A &&& B) &&& (C &&& D) -- balanced*)
   185 (*(A &&& B) &&& (C &&& D) -- balanced*)
   186 fun dest_conjunction_balanced 0 _ = []
   186 fun dest_conjunction_balanced 0 _ = []
   187   | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
   187   | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
   188 
   188 
   189 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
   189 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
   190 fun dest_conjunctions t =
   190 fun dest_conjunctions t =
   191   (case try dest_conjunction t of
   191   (case try dest_conjunction t of
   192     NONE => [t]
   192     NONE => [t]